Technology media outlet Gigazine published a blog post yesterday (August 3), reporting that a Lean formalized proof completed with the help of AI and claiming to disprove the Collatz conjecture was confirmed to be invalid.
Note: The Collatz conjecture (also known as the Syracuse conjecture or the 3n+1 conjecture) was proposed by German mathematician Lothar Collatz in 1937. It is an extremely simple yet still unsolved mathematical problem, asserting that after repeated application of a specific set of rules, every positive integer will eventually return to 1.
The calculation rules for any positive integer n are:
If n is even, divide it by 2 (n ÷ 2).
If n is odd, multiply it by 3 and add 1 (3n + 1).
After obtaining the new number, repeat the above steps until the result becomes 1.
Taking the number 6 as an example:
6 is even; dividing it by 2 gives 3.
3 is odd; multiplying it by 3 and adding 1 gives 10.
10 is even; dividing it by 2 gives 5.
5 is odd; multiplying it by 3 and adding 1 gives 16.
16 successively divided by 2 gives 8, 4, 2, and 1.
The final path is: 6 → 3 → 10 → 5 → 16 → 8 → 4 → 2 → 1.
Formal verification expert Ramana Kumar published a project on GitHub on July 25, initially claiming that he had disproved the Collatz conjecture with the help of AI. The project did not provide a specific counterexample integer; it merely proved in Lean (a theorem-proving assistant system) that “there exists a number that cannot reach 1.”
Lean is a theorem-proving assistant system that allows users to write mathematical formulas and logic as programs, with the computer verifying the accuracy of the proofs. Lean code written by users turns mathematical propositions and proofs into checkable programs, while the kernel verifies type and logical consistency.
However, while subsequently reviewing the refutation, he discovered that the relevant method could even make Lean unconditionally accept “False,” representing a false proposition. Therefore, the current code cannot refute the Collatz conjecture.
Formal verification researcher Kiran Gopinathan reduced the issue to a small reproducer and reported it to the Lean development team on July 28, 2026.
The vulnerability was located in the kernel’s handling of “nested inductive types,” which sometimes caused it to ignore “phantom type parameters,” meaning parameters that do not appear directly in the components of a data structure. As a result, parameters that should originally have been deemed invalid could evade verification. Lean developer Leonardo de Moura said that the issue was caused by the kernel implementation failing to perform the required checks.
The Lean team created a fix pull request about 1 hour after receiving the report and released Lean 4.32.2 on July 28, fixing the issue.