Lean Proof Found To Be False

[Hornbein]

From AI. I'm too lazy to check it.

• Publication: On July 25, 2026, Ramana Kumar published an AI-assisted Lean repository containing a sorry-free formal proof purporting to show that the Collatz conjecture was false by exhibiting an orbit that does not return to 1. [1, 2]
• The Kernel Bug (Issue #14576): The proof did not contain a valid mathematical refutation. Instead, it exploited an implementation bug in how the Lean 4 kernel handled nested inductive types with phantom parameters. When eliminating a nested occurrence, these parameters disappeared from the generated auxiliary type, allowing an ill-typed term to bypass checks and prove a contradiction (False). [1]
• Independent Checker Bug: The repository also coincidentally bypassed an independent checker (Nanoda) due to a separate, unrelated bug in Nanoda's projection node verification. [1]
• The Fix: Kiran Gopinathan reduced the exploit to a small proof of False on July 28, 2026, and Lean's creator Leonardo de Moura pushed a patch to fix the kernel bug within an hour. The Collatz conjecture remains completely unresolved. [1, 2]

 

[pbuk]

I'm too lazy to check it.

That's pretty lazy

Verified: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

 

[sbrothy]

It smells a little of AI. But what do I know?

 

[sbrothy]

That's pretty lazy

Verified: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

Oh lazy indeed. It was AI-backed.

 

[FactChecker]

ANYTHING that relies on unfiltered internet "knowledge" is on very shaky ground.

 

[sbrothy]

If you mean that as critique I’ll take it as such, it just looked pretty valid.

Nothing personal.

 

[FactChecker]

If you mean that as critique I’ll take it as such, it just looked pretty valid.

Nothing personal.

Nothing personal. I know nothing about this subject, but I am very skeptical, in general, about the current wave of AI LLM efforts. IMO, any AI LLM results require very careful review.

 

[sbrothy]

The Lean 4 Theorem Prover and Programming Language

The Lean Theorem Prover (System Description)

 

[sbrothy]

But yes. I’m also pretty clueless.