What happened with the AI "disproof" of Collatz
The Collatz conjecture states that starting from any positive integer and repeatedly halving if even or tripling and adding one if odd, you always reach 1. Disproving it means exhibiting a number that never reaches 1.
July 25–28, 2026
sorry-free "disproof" of the Collatz conjecture, produced with AI assistanceA soundness bug in the Lean kernel ( #14576 ) was reported and fixed during the week of July 27. ／ On July 25, Ramana Kumar published a repository containing a sorry -free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576 . We pushed a fix one hour after the report ( #14577 ). Joachim Breitner reviewed it and suggested improvements, and it was merged. New patch releases are out. — From the account of what happened and how quickly it was fixed
"No sorry" did not hold
When writing a proof in Lean, unfinished steps are marked with sorry. A repository with no sorry anywhere presents as having passed the checker with nothing left open. That is why it mattered that what was published was sorry-free. The postmortem makes that point and then states it is not a valid proof.
But the check itself had a gap. Passing the checker did not guarantee the proof was correct. That is the heart of it. Machine checking exists to eliminate human oversight, but if the machine's implementation has a bug, the guarantee does not hold.
Spotted in three days, closed in an hour
The speed of the response is also worth recording. Three days after publication, another researcher extracted the core of the problem, reduced it to a minimal example proving False, and filed a bug report. A fix was out one hour after the report, reviewed, merged, and shipped as patch releases.
Measured from anomaly to closure, the verification culture in this field turns over quickly.
Where the bug in the Lean kernel was
Into the technical substance. It looks difficult, but only one point really matters: something that should have been type-checked disappeared from the set of things being checked.
The essentials of bug #14576
The bug: when the kernel eliminates a nested occurrence under an inductive type T with parameters Ds , and these parameters are phantom (not mentioned in constructor fields), they disappear from the generated auxiliary type and thus escape type checking. An ill-typed argument in that position could be used to make the kernel accept a proof of False . The bug is only reachable through metaprogramming, by sending the inductive declaration to the kernel directly. The frontend checks the arguments and catches the ill-typed term. This is an implementation bug, not a hole in Lean's meta-theory. — From the technical description of the bug, how it is reached, and how it is classified
It does not reach people writing ordinary Lean
The scope needs stating correctly. The bug is only reachable by using metaprogramming — writing programs that build programs — to send an inductive declaration straight to the kernel. Written as ordinary Lean code, the frontend checks the arguments first and catches the ill-typed term there.
So this is not existing proofs collapsing across the board. It was a hole that opened only when a deliberately crafted declaration was submitted. No wave of already-formalised proofs became invalid.
Banning metaprogramming would not fix it
One suggestion in the discussion was to restrict metaprogramming so the attack could not be expressed. The postmortem rejects this as misguided.
The reason is architectural. The elaborator, the layer converting written expressions into internal representation, is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker can write compiled .olean files directly or modify memory, either of which bypasses the elaborator entirely. So the kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns, the postmortem says, is one of the main advantages of proof terms.
One suggestion in the discussion is to remove or restrict metaprogramming so that this attack is not expressible. This is misguided. The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker who wants to submit a malicious proof can also write .olean files directly or modify memory, both of which bypass the elaborator entirely. The kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns is one of the main advantages of proof terms. — From the response to the proposal of restricting metaprogramming
The independent checker missed it at the same time
The heaviest part of this episode is not the kernel bug itself. It is that nanoda, the independent checker used as a backstop, also let the same proof through.
Two implementations, two unrelated bugs
| Checker | Implementation | What happened here |
|---|---|---|
| Official Lean kernel | Reference implementation | Missing check in nested inductive type support |
| nanoda | Independent Rust implementation by Chris Bailey | Checked that spot, but did not verify the type name in a projection node |
| lean4lean | Port of the reference implementation | Affected by the same kernel bug |
The original Collatz repository also passed a week-old version of nanoda , the main external checker. nanoda is an independent kernel (aka proof/type checker) for Lean implemented in Rust by Chris Bailey . The surprising part is that there are two unrelated bugs involved. The official kernel had a missing check in the nested inductive type support, as explained above. nanoda did check that spot, but did not verify the type name in a projection node. The nanoda bug was reported by Jeremy Chen and fixed a week before the Lean bug was reported. ／ The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both. ／ lean4lean is affected by the kernel bug, since its handling of inductives is a port of the reference implementation. — From why nanoda missed it, why independent-kernel checking still works, and the effect on lean4lean
Double-checking has not been invalidated
Checking with an independent kernel still works. What slipped through did so because two unrelated bugs happened to line up; either one alone would not have sufficed. That it took a distinct defect in each of two implementations is, if anything, evidence for the value of double-checking.
There is a condition attached: keep both current. The nanoda bug was reported by Jeremy Chen and fixed a week before the Lean bug was reported. What let this through was verifying against a week-old build. If your workflow puts proofs through a checker, version management of the checker is part of the guarantee.
Was the timing against nanoda's hole a coincidence?
The unsettling detail is that the spot targeted was an expression the old nanoda would accept. Ramana Kumar believes the timing was coincidental but cannot rule out that the model had seen the nanoda report. Joachim Breitner offers a different hypothesis: that the timing coincidence is due to the availability of models strong enough to find this bug.
The proof was built so that the expression the kernel never inspects is one that the old nanoda accepted. ／ Ramana believes the timing was coincidental, but cannot rule out that the model had seen the nanoda report. Joachim proposed the hypothesis that the timing coincidence is due to the availability of strong models able to find this bug. — From what the proof was built to target and the participants' views on the timing
What the Lean side changed afterwards
The postmortem does not stop at reflection; it lists what has already been done. The episode pushed the defences up.
Regression tests and additional kernel checks
First, regression tests — automated checks that catch the same defect recurring — for the exploit and for a related non-uniform-parameter case raised by Arthur Adjedj are now in the Kernel Arena. If the same hole opens again, a machine notices.
A follow-up PR (#14582) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them. Kernel invariants have been hardened as well. The actual changes are public, so you can put before and after side by side.
Regression tests for the exploit, and for a related non-uniform-parameter case raised by Arthur Adjedj, are in the Kernel Arena . ／ A follow-up PR ( #14582 ) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them. ／ We have also hardened kernel invariants. PRs: #14621 , #14631 , #14632 . — From the regression tests, the additional check, and the hardening of kernel invariants
OpenAI's help turned up several more bugs
This part should not be missed. Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialised in cybersecurity and found other programming mistakes in the Lean kernel. All have been fixed, across six changes.
There is a sequel to that result. Every one of the newly found bugs was caught by nanoda. And all of them are likewise only reachable through metaprogramming. The pattern from the previous section — that two implementations missing the same thing at once is unlikely — holds here as well.
AI made the bug; AI found the bugs. Set side by side in the same week, it is clear the technology cuts both ways. The use of AI in mathematical proof is accelerating regardless, as in Fable 5's work on the Jacobian conjecture.
And this same nanoda appears in OpenAI Astra's ten open problems, published the same week, because nanoda is built into the instructions for third parties to check those published proofs. A checker in which a hole was just found is being used to verify the next result. Which is exactly why the earlier condition — keep both current — matters in practice.
Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed. All of them were caught by nanoda. These bugs are also only reachable through metaprogramming. PRs: #14607 , #14608 , #14609 , #14613 , #14615 , #14616 . ／ comparator.live now runs nanoda by default, and nanoda is tracked daily so lean-eval and comparator stay current after upstream fixes. — From the additional bugs found with OpenAI's help and the updates to the checking environment
The verified-kernel effort is still in progress
One more fact for an accurate picture. Mario Carneiro's lean4lean is a Lean formalisation of Lean's type theory together with a proof that the kernel implements it.
The work is ongoing, though: the proof of consistency does not cover inductive types yet, and the to-be-verified implementation suffered from the same bug as the official kernel. The postmortem notes the bug would have been found when attempting to conclude the verification of this part. The plan to secure this with formal methods is not finished — that is where things stand.
Mario Carneiro's lean4lean is a Lean formalization of Lean's type theory together with a proof that the kernel implements it. The work is ongoing, the proof of consistency does not cover inductive types yet, and the to-be-verified implementation suffered from the same bug as the official kernel. The bug would have been found when attempting to conclude the verification of this part. — From the progress of the lean4lean verification effort
Conclusion: how much to trust machine checking
What this episode shows is not that machine checking is pointless. It is the obvious fact that the guarantee rides on the quality of the checker's implementation. No sorry means every step passed the check; that the check itself is correct is a separate requirement.
Three practical stances follow. First, run an independent implementation alongside. Given that slipping through took two distinct bugs, this defence is working. Second, keep that checker current. Verifying against an old build was the direct cause here. Third, for heavy claims, state the versions of the verification environment along with the result.
And one more thing. The bug was exploited by AI, and the other bugs were found by AI. That the same tool works on both the proving side and the hardening side says a lot about where this field sits for now. When reading a published fix, going through line by line to see which check was added is what brings the shape into focus.
