A proof assistant capable of validating a proof of the Collatz conjecture: that would have sent shockwaves through the world of formal mathematics. Except the proof in question, generated by an AI, exploited a very real soundness bug in Lean’s kernel. The community erupted, and Leo de Moura, the system’s creator, responded with a postmortem of exemplary transparency.
The incident rattled Lean users far beyond academic circles. A question posted on MathOverflow captured the prevailing unease: “Are we stuck with Lean?” In other words, can we still trust a kernel that let a proof of False slip through?
The origins of bug #14576: a flaw in nested inductive types
It all started on July 25, 2026, when Ramana Kumar published a repository containing a “proof” of the Collatz conjecture, built with the help of an artificial intelligence. The proof contained no sorry terms, those placeholders that usually signal an incomplete proof. And yet, it was not valid.
On July 28, Kiran Gopinathan reduced the problem to a minimal kernel: a proof of False fitting in just a few lines. Bug #14576 was opened. An hour later, the Lean team proposed a fix, reviewed by Joachim Breitner, then merged. Patched versions were deployed right after.
The flaw lies in how the kernel handles nested inductive types. When the kernel eliminates a nested occurrence under an inductive type T with parameters Ds, and those parameters are phantom (absent from the constructors’ fields), they disappear from the generated auxiliary type and escape the typing check. The result: a badly typed term can be slipped in at that exact spot, and the kernel accepts a proof of False.
It is important to stress that this soundness bug in Lean’s kernel is only exploitable through metaprogramming, by sending an inductive declaration directly to the kernel. The frontend, for its part, checks the arguments and blocks the badly typed term. Leo de Moura insists: this is an implementation bug, not a flaw in Lean’s meta-theory.
Why nanoda saw nothing
One of the most surprising aspects of this incident concerns nanoda, Lean’s independent external checker developed in Rust by Chris Bailey. The Collatz proof also passed in a week-old version of nanoda. Two distinct bugs, then, in two different implementations.
The official kernel omitted a check in its handling of nested inductive types. Nanoda, for its part, did run that specific check, but failed to verify the type name in a projection node. A bug discovered by Jeremy Chen and fixed one week before the Lean bug. The faulty proof exploited both flaws simultaneously.
Ramana Kumar believes the timing is coincidental, though he does not rule out that the AI model may have been aware of the nanoda bug report. Joachim Breitner offers a broader hypothesis: the recent availability of models powerful enough to sniff out this kind of flaw would explain the unsettling synchronization.
The practical takeaway is reassuring: checking with an independent kernel still works, since two distinct bugs in two implementations were needed. But users who rely on this double-verification approach must keep both tools up to date, no exceptions.
Metaprogramming: cutting off access is not the answer
In the discussions that followed, one suggestion kept coming up: restrict or remove metaprogramming to prevent this type of attack. Leo de Moura dismisses the idea outright.
The elaborator is, by design, an untrusted component. The system’s soundness cannot rest on an untrusted component refusing to build a malicious term. An attacker wanting to submit an invalid proof can also write .olean files directly or tamper with memory, two vectors that bypass the elaborator entirely.
The kernel must reject badly typed declarations on its own, within its own process. This separation of responsibilities is one of the great advantages of proof terms. Trying to plug the hole by shrinking the elaborator’s attack surface would merely shift the problem without solving it.
What the FRO has put in place since
The Lean FRO (Focused Research Organization) has been busy. Regression tests for the exploit, as well as for a related case of non-uniform parameters reported by Arthur Adjedj, have been integrated into the Kernel Arena, the kernel test suite.
A complementary fix (PR #14582) now ensures that the kernel checks that the parameters of a nested occurrence genuinely behave as parameters, rather than simply re-verifying them.
Daniel Selsam, at OpenAI, assisted the FRO with a cybersecurity-specialized AI. The result: additional programming errors were found in the kernel. All have been corrected. All were caught by nanoda. The relevant PRs are #14607, #14608, #14609, #14613, #14615, and #14616. Kernel invariants have also been strengthened (PRs #14621, #14631, #14632).
On the infrastructure side, comparator.live now runs nanoda by default, and nanoda is tracked daily so that lean-eval and comparator stay synchronized with upstream fixes. The FRO is also reaching out to experts capable of finding other bugs, developing new kernels, and working on the theory or on formally verified kernels.
Trust strengthened through transparency
Leo de Moura’s postmortem was praised for its candor. Where a bug of this nature could have durably eroded Lean’s credibility, the team’s swift and well-documented response produced the opposite effect. The community, though shaken, seems to emerge stronger from the episode.
The bug was confined to a feature not covered by Mario Carneiro’s consistency proof in lean4lean, a formalization of Lean’s type theory within Lean itself. That proof, still in progress, does not yet cover inductive types. The bug would have been discovered anyway when that verification was finalized.
The incident illustrates a broader reality: the soundness of proof assistants is a critical concern, and formal verification of the kernel itself remains a goal to pursue. The transparency shown by the Lean team is probably the best asset to get there.
Key takeaways
- Bug #14576 allowed the Lean kernel to accept a proof of
Falsevia a defect in the handling of nested inductive types with phantom parameters. - The flaw was only exploitable through metaprogramming, bypassing the frontend; the bug is an implementation error, not a theoretical flaw.
- Two independent bugs in two implementations (the official kernel and nanoda) were required for the faulty Collatz conjecture proof to pass.
- The Lean team fixed the flaw within an hour, strengthened kernel invariants, and enlisted a cybersecurity AI to uncover other potential errors.
- The transparency of the postmortem and the quality of the technical response strengthened the community’s trust rather than weakening it.
Using Lean in your formalization projects or interested in proof assistant soundness? Feel free to share your thoughts in the comments or reach out to discuss these topics.
Sources
- Postmortem for Kernel Soundness Bug #14576, Official post by Leonardo de Moura, creator of Lean
- Are we stuck with Lean?, Academic discussion on MathOverflow about the bug’s implications
- AI-Generated Lean Proof Exploits Collatz Kernel Bug, Article relayed by Digg illustrating the concrete exploitation of the flaw by an AI