An AI-assisted 'falsification of the Collatz conjecture' was found to be invalid, having exploited a kernel bug in Lean.
A proof disproving
Postmortem for Kernel Soundness Bug #14576 — Leonardo de Moura
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/
The Collatz conjecture states that for any positive integer, if you repeatedly perform the operations 'divide by 2 if even' and 'multiply by 3 and add 1 if odd,' you will eventually reach 1. For example, starting with 6, the sequence would be '6→3→10→5→16→8→4→2→1'. The calculation rules are simple, but as of the time of writing, it remains an unsolved problem with no proof or counterexample found.
To disprove the Collatz conjecture, it is necessary to show that there exists at least one positive integer for which the operation cannot be repeated any number of times and the result will not reach 1. On July 25, 2026, Ramana Kumar, a specialist in formal verification, published a project on GitHub claiming to have 'disproven the Collatz conjecture with the help of AI.'
GitHub - xrchz/CollatzLean: Collatz conjecture in Lean · GitHub
https://github.com/xrchz/CollatzLean
The project in question claimed to have proven, using Lean principles, that 'there exists a number that does not reach 1,' rather than providing a specific integer.
Lean is a theorem proving assistance system that allows you to write mathematical formulas and logic as programs and have a computer verify the accuracy of the proofs. The Lean code written by the user is converted into an internal representation that the kernel can check by an processing system called an 'elaborator,' and finally the core checking program, the 'kernel,' checks for type consistency. Even if there are flaws in the complex automated proving function, the kernel is designed to maintain reliability by rejecting invalid proofs.
This project did not rely on the 'sorry' notation used to temporarily place incomplete proofs, nor on additional axioms, and outwardly appeared to be a formal proof.
However, while Kumar was investigating the content of the counter-argument, he discovered that it was possible to get Lean to accept the proposition 'False,' which represents falsehood, regardless of the Collatz conjecture. Kiran Gopinathan, a researcher specializing in formal verification, put the problem into a small reproduction code and reported it to the Lean development team on July 28.
If it becomes possible to prove false without any preconditions, then logically, any proposition can be proven. In other words, it becomes possible to reach not only the conclusion that 'the Collatz conjecture is false,' but also the opposite conclusion that 'the Collatz conjecture is true,' so the accepted code does not constitute a refutation of the Collatz conjecture.
The problem lay in the part of the kernel that handled complex data structures known as 'nested inductive types.' 'Phantom type parameters,' which don't directly appear in the data structure's components, were sometimes omitted from the generated auxiliary types, allowing arguments that should have been mistyped to escape validation. Providing mistyped arguments made it possible to trick the kernel into accepting contradictory proofs.
When you input normal Lean code, type mismatches are detected in processing before the kernel. To exploit this bug, it was necessary to use metaprogramming features that construct Lean's internal representation and send a crafted declaration directly to the kernel. De Moura explains that the problem wasn't with the Lean logic itself, but rather with a failure in the kernel's implementation checks.
The original project had also passed verification by Nanoda, an independent checker written in Rust, separate from Lean. However, the older version of Nanoda used had another bug that prevented it from validating type names in projection nodes. The proof was constructed in such a way that expressions that were bypassed by the Lean kernel bug were also accepted by this other bug in the older version of Nanoda. In other words, unrelated bugs in two implementations, Lean and Nanoda, were exploited simultaneously.
While Kumar believes it was a coincidence that the two bugs were available at the same time, he says he cannot rule out the possibility that the AI model had previously learned from Nanoda's bug reports. On the other hand, Joachim Breitner, who is involved in the development of Lean, suggests that the availability of a high-performance AI model may have enabled the discovery of more complex bugs.
The Lean development team created a pull request for a fix approximately one hour after the report, adding code to verify within the kernel whether the problematic argument is of the correct type. Lean 4.32.2, which includes the fix, was released on July 28, 2026. Updating to the latest version of Nanoda is also recommended if you are using independent checks.
Lean FRO, the non-profit research organization responsible for developing Lean, is adding preventative tests and working to more rigorously scrutinize the kernel's internal prerequisites. Daniel Selsam of OpenAI, using security-focused AI, assisted Lean FRO in their investigation and found several other implementation errors, all of which have since been fixed as of the time of writing.
While the Collatz conjecture was not disproven, the AI-assisted code ultimately revealed flaws in Lean and Nanoda. De Moura stated that he will continue to support the development of new independent kernels and testers to strengthen proof-checking mechanisms.
Related Posts:
