Lean patches kernel bug that let an AI "disprove" the Collatz conjecture

On July 25, Ramana Kumar published a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It was not a valid proof: it exploited a soundness bug in the kernel of the Lean theorem prover. On July 28, Kiran Gopinathan reduced the exploit to a minimal proof of False and opened kernel issue #14576. The FRO pushed a fix, pull request #14577, one hour after the report; Joachim Breitner reviewed it, suggested improvements, and it was merged, with new patch releases following.

The bug sat in how the kernel checks nested inductive types. When the kernel eliminates a nested occurrence under an inductive type whose parameters are "phantom" (not mentioned in any constructor field), those parameters vanish from the generated auxiliary type and escape type checking. An ill-typed argument placed there could make the kernel accept a proof of False. The flaw was reachable only through metaprogramming, by sending an inductive declaration to the kernel directly; Lean's normal frontend still catches ill-typed terms, so the postmortem stresses this is an implementation bug, not a hole in Lean's underlying logic.

The same Collatz repository also passed nanoda, the independent Lean kernel checker written in Rust by Chris Bailey, because nanoda carried a separate, unrelated bug: it checked the spot the official kernel missed but did not verify a type name in a projection node. That nanoda bug had been reported by Jeremy Chen and fixed a week before the kernel issue was opened, so the fake proof worked only by hitting an expression the kernel never inspected while relying on the version of nanoda that predated its own fix. Ramana Kumar says the timing looks coincidental but cannot rule out that the model had seen the nanoda report; Breitner instead proposes that the coincidence reflects strong models now being capable of finding this class of bug at all.

Mario Carneiro's lean4lean, a from-scratch formalization of Lean's type theory together with a proof that the kernel implements it, turned out to share the same bug, since its handling of inductive types ports the reference implementation; its ongoing consistency proof does not yet cover inductive types, so the flaw would have surfaced once that part was verified. After the incident, Daniel Selsam at OpenAI assisted the FRO with an AI specialized in cybersecurity, which found six more programming mistakes in the kernel, all reachable only through metaprogramming and all caught by nanoda; all six were fixed (pull requests #14607, #14608, #14609, #14613, #14615, #14616). The FRO also merged three pull requests hardening kernel invariants (#14621, #14631, #14632), added regression tests in the Kernel Arena for the exploit and for a related non-uniform-parameter case raised by Arthur Adjedj, and put comparator.live on a version of nanoda tracked daily so it and lean-eval stay current with upstream fixes.

One suggestion raised in the discussion was to remove or restrict metaprogramming so the attack could not be expressed. The postmortem rejects this: Lean's elaborator is untrusted by design, so soundness cannot depend on an untrusted component simply refusing to build a bad term; an attacker able to submit a malicious proof could also write .olean files directly or modify memory, bypassing the elaborator entirely. The kernel has to reject ill-typed declarations on its own. Checking with an independent kernel still works in principle, since exploiting the incident required two distinct bugs in two separate implementations, but only for users who keep both current.

Key facts

Ramana Kumar's AI-assisted "disproof" of the Collatz conjecture, published July 25, exploited a Lean kernel soundness bug rather than proving anything.
Kiran Gopinathan reduced it to a proof of False and opened issue #14576 on July 28; the FRO shipped a fix, pull request #14577, one hour later.
The flaw let phantom parameters of a nested inductive type escape type checking, reachable only through metaprogramming that bypasses Lean's frontend.
The independent nanoda checker missed the same exploit only because of its own separate bug, already fixed a week earlier after a report by Jeremy Chen.
An OpenAI cybersecurity-specialized AI, run with Daniel Selsam's help, then found six more metaprogramming-only kernel bugs, all fixed, plus three further invariant-hardening pull requests.

Why it matters

A soundness bug in a proof assistant's kernel is close to a worst case for formal verification: it lets the system accept a "proof" of a false statement, undermining the guarantee that makes Lean useful for checked mathematics and software. This one surfaced through an AI-assisted attempt to disprove the Collatz conjecture, a case where a model produced something that exploited a subtle kernel flaw rather than a genuine proof. The response also doubles as a case study in defense in depth: an independent checker, nanoda, was supposed to catch exactly this class of error and initially did not, because it carried its own separate, already-fixed bug; the fake proof worked only by threading the gap between the two.

Who it affects

Anyone using Lean for verified mathematics or software needs the patched kernel. Mario Carneiro's lean4lean project is directly affected, since its inductive-type handling ports the same reference implementation and shared the bug. Users of nanoda as an independent double-check need its patched version too, since the Collatz exploit depended on both the kernel bug and the now-fixed nanoda bug being present at once. More broadly, anyone treating an AI-produced Lean proof as trustworthy without checking it against a current, independent kernel is exposed to the same class of exploit.

How to use it

There is no product or price here: the fix ships as new Lean patch releases plus a set of merged pull requests, the original kernel fix (#14577), six further metaprogramming-bug fixes (#14607, #14608, #14609, #14613, #14615, #14616), and three invariant-hardening pull requests (#14621, #14631, #14632). Projects should update both Lean and nanoda to current versions. Regression tests for the original exploit and for a related non-uniform-parameter case raised by Arthur Adjedj now live in the Kernel Arena, and comparator.live runs a daily-tracked nanoda so lean-eval and comparator stay in sync with upstream fixes.

How solid is it

This is a first-party postmortem published on the FRO's own blog, reviewed by Joachim Breitner and Sebastian Ullrich, and it names specific issue and pull request numbers throughout (#14576, #14577, #14607 through #14616, #14621, #14631, #14632) rather than describing the fix in the abstract. The technical explanation of the phantom-parameter mechanism is precise enough to be checked against the actual patch. The one soft spot is attribution of intent: nobody, including Ramana Kumar, can say for certain whether the AI model saw the prior nanoda bug report or found the exploit independently.

Risks and caveats

The postmortem is explicit that this was an implementation bug, not a hole in Lean's underlying logic, but it also concedes that an independent kernel is not an automatic safety net: nanoda missed the same fake proof because it had its own unrelated bug, and would have caught it only if patched in time. Ramana Kumar says the timing relative to the nanoda fix looks coincidental but cannot rule it out; Breitner's competing explanation is that sufficiently strong models can now find this kind of bug as a matter of course, which if true means more such reports should be expected rather than treated as one-off. The FRO also pushes back on removing metaprogramming as a fix, arguing the kernel, not the untrusted elaborator, has to be the thing that rejects bad proofs.

“The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term.”

— the postmortem