Collatz Conjecture Proof: Why Lean Accepted a Fake

Is the Collatz conjecture solved? What the AI-assisted proof was

The Collatz conjecture remains unsolved, since the AI-assisted "disproof" Lean accepted was not a real proof. It got through by exploiting a bug in the Lean kernel. The kernel is the core of Lean that does the final check on every proof, no matter who or what wrote it.

What the Collatz conjecture claims and what a disproof needs

The conjecture says every starting value eventually reaches 1, so disproving it takes one value that never does. The rule is simple: take a number N, halve it if it is even, replace it with 3N+1 if it is odd, and repeat. Lawrence Paulson notes that the conjecture is nearly a century old and that extensive testing has never found a counterexample.

The repository in question presented itself as a formal, machine-checked disproof. Had it held up, it would have overturned the conjecture, but it did not.

Why a sorry-free Lean proof looked finished

A Lean proof without sorry looks complete, because sorry is the placeholder for a step nobody has proved yet. With none left, the checker has no open gap to report, which is why it mattered that the repository was sorry-free.

That guarantee depends on the checker itself being correct. Here the kernel accepted a term it should have rejected, so passing the check proved nothing about the conjecture.

Three days from publication to the bug report

On July 28, three days after publication, Kiran Gopinathan boiled the repository down to a small proof of False and opened issue #14576. Ramana Kumar had published it on July 25 with AI assistance. A proof of False is the classic sign of a soundness bug, since a system that accepts it can be made to accept anything.

How the Lean kernel bug let a false proof through

The Lean kernel skipped type-checking phantom parameters, which let an ill-typed term slip into a proof of False. Lean works in layers, and the kernel is the last, meant to re-check whatever the layers above it produce.

Phantom parameters in nested inductive types

A phantom parameter is one no constructor field refers to, and those were exactly the ones the kernel lost track of. A nested inductive type contains itself inside another type in its definition. When the kernel unpacks such a nested occurrence, it builds an auxiliary type, and the phantom parameters drop out of it.

After that, nothing checks those parameters. Put an ill-typed argument in that slot and the kernel could be tricked into accepting a proof of False.

Why ordinary Lean code never reaches the bug

Normal Lean code never gets near the bug, because the frontend rejects the ill-typed term first. Only metaprogramming, code that builds Lean declarations, can send an inductive declaration straight to the kernel and bypass that check. Someone writing an ordinary proof never takes that route.

The flaw is in the implementation, not the mathematics behind it. A follow-up postmortem published on August 24 says the same: the theory of Lean's inductive types is well understood, and the faults were coding errors.

A fix one hour after the report

An hour after the report, the Lean team pushed a fix in #14577. Joachim Breitner reviewed it and suggested improvements before it was merged, and new patch releases followed. Both the report and the fix happened in the week of July 27.

The first patch was only the start. A follow-up, #14582, tightened the check itself.

Why the nanoda checker missed the false proof too

The nanoda checker let the proof through because of a separate bug of its own. It looked at the spot the official kernel skipped but never verified a type name in a projection node. Chris Bailey wrote nanoda in Rust as an independent kernel for Lean, and Paulson's post says the proof was checked in Lean and then double-checked with nanoda, and both were fooled.

Two unrelated bugs lined up in one proof

For the repository to pass both checkers, two unrelated bugs in two separate implementations had to line up. It passed a week-old version of nanoda, and the proof was built around an expression the official kernel never examined and the older nanoda build let pass.

Jeremy Chen reported the nanoda bug, which was fixed a week before the Lean bug report. So the build that passed was already out of date when the repository appeared.

Was the timing a coincidence?

No one knows for certain: Ramana Kumar believes the timing was chance but cannot rule out that the model had seen the nanoda report. It comes up because the nanoda fix and the Lean report were only a week apart.

Joachim Breitner offered another explanation: strong models capable of finding this bug are now available. The postmortem gives both views and does not choose between them.

Why lean4lean shared the flaw

The lean4lean port had the same kernel bug because its handling of inductive types is ported from the reference implementation. A port inherits the original's mistakes along with its design, and since Mario Carneiro's project also aims to prove that the kernel implements Lean's type theory, a shared bug weighs more there.

Not every bug carried over. In the later bug hunt, lean4lean matched the main kernel but escaped one bug (#14807), because its isProp already used ensureSortCore.

Why banning metaprogramming would not fix a soundness bug

Restricting metaprogramming would not cure a soundness bug, because the kernel cannot count on an untrusted layer to refuse bad terms. Someone in the discussion proposed restricting metaprogramming so this attack could not be expressed. The postmortem calls that idea misguided.

The elaborator is untrusted by design

The elaborator, which turns what a person writes into Lean's internal form, is untrusted by design. Soundness cannot rely on it behaving well, because if a proof's safety depended on the elaborator refusing to build a bad term, one elaborator bug would break every guarantee.

What the kernel has to reject on its own

The kernel has to reject ill-typed declarations by itself, since a malicious submitter can bypass the elaborator. That person can write .olean files (Lean's compiled output) directly or alter memory. Both routes skip the elaborator, so no limit on metaprogramming would block them.

The postmortem names this separation as one of the main advantages of proof terms. The August 24 follow-up agrees that lake build does not protect against adversarial proofs and that the gold standard is comparator plus external checkers. The Lean FRO, the organization behind Lean, treats AI-generated proofs as a possible source of malicious ones.

What the Lean team changed after the soundness bug

The Lean team added tests and stricter checks, and a bug hunt run with OpenAI's help turned up more soundness bugs, one of which nanoda also accepted. The fixes from that hunt shipped in Lean v4.33.1 on August 21, while the new lake check commands were still only planned as of August 24.

Regression tests and the #14582 check

The Kernel Arena now has regression tests for the exploit and for a related non-uniform-parameter case Arthur Adjedj raised. A regression test is an automated check that fails if the same defect returns.

A follow-up PR, #14582, goes further. It makes the kernel confirm that the parameters of a nested occurrence really behave as parameters, rather than just re-running type checks on them.

Kernel invariants were also tightened, in #14621, #14631 and #14632. Since the pull requests are public, you can compare the code before and after each change.

What the OpenAI-assisted bug hunt found

OpenAI's Daniel Selsam used internal models to search the official Lean kernel and runtime for soundness bugs between July 30 and August 20. The search stopped when the internal AI reported it could find nothing else, and Lean v4.33.1, released on August 21, fixes everything it found.

The model turned four kernel bugs into proofs of False that the official kernel accepted. The “Kernel soundness bugs the model exploited, and what the other checkers did” table shows whether two independent checkers, nanoda and ind-models, rejected each one.

The follow-up postmortem adds a case nanoda missed: it accepted the bogus proof for #14807. Two runtime bugs were exploited too: a reference counter overflow (fixed in #14838) and a known bug in GMP v6.1.2, which the official Linux build used instead of v6.3.0 (fixed in #14833). Like any external checker not built on the Lean runtime, nanoda rejected both.

Four more PRs fixed bugs that were not soundness bugs. Two, #14607 and #14609, came up when the team tried to export the exploit, and the other two, #14608 and #14615, were ordinary bugs, with #14615 fixing the official kernel's rejection of a valid inductive declaration.

Checkers that run nanoda by default

comparator.live now uses nanoda as its default checker. The team also tracks nanoda's releases daily so that lean-eval and comparator pick up upstream fixes quickly, which addresses the problem the week-old build exposed.

More was planned but not yet shipped as of August 24. From Lean v4.35.0, lake check is meant to export a project and recheck it with lean4checker, with lake check nanoda using nanoda and lake check --paranoid using every kernel shipped with Lean. The Lean FRO also plans to bundle nanoda, lean-inductive-models and lean4lean in the official distribution.

Joachim Breitner's lean-inductive-models, listed in the Kernel Arena as ind-models, proves that an inductive type can be modeled from first principles. It catches a large class of bugs in how the kernel handles inductives, and in the “Kernel soundness bugs the model exploited, and what the other checkers did” table above, it rejected all four bogus proofs.

Is the Lean theorem prover still safe to trust?

Lean proofs are still worth trusting when an up-to-date independent kernel checks them as well, but the guarantee depends on the checkers' code. The Collatz proof Lean accepted was fake, yet the lesson is narrower than "machine checking is useless".

Run an independent checker and keep it current

An independent kernel still helps, because sneaking a fake proof past it took two separate bugs in two implementations. Three practices follow.

Run an independent implementation alongside Lean, and keep it current, since the original repository passed a nanoda build that was a week out of date. For a high-stakes claim, also publish the versions of the verification environment with the result, a step the postmortem itself does not list.

The bug hunt points to one more lesson that the postmortem does not spell out. One external checker is not enough: nanoda accepted the bogus proof for #14807 while ind-models rejected it, so different checkers catch different mistakes.

A skeptic's view on proof objects

Lawrence Paulson says he knows of no case where an independent checker caught an error a kernel had let through, and nanoda was fooled here as well. In his view, storing proof objects adds weight, and only the calculi that keep them seem to need everything inside the kernel.

He wrote that on July 30, before the hunt, and the later record cuts the other way in one respect: the two runtime bugs produced proofs of False that the official kernel accepted and nanoda rejected. His objection is still worth weighing, since the Collatz proof itself fooled both checkers.

Verified kernels are unfinished

Verified kernels are not finished yet: lean4lean's consistency proof does not cover inductive types so far. The implementation being verified also had the same bug as the official kernel, which the postmortem says would have come to light when verification of that part was completed.

Verified kernels written in Lean are also exposed to bugs in the Lean runtime, as the reference counter and GMP exploits showed. The Lean FRO adds that lean4lean does not need to mirror the official kernel line by line.

Jacobian conjecture disproved with Claude Fable 5 and OpenAI Astra: ten math proofs, no release date cover other AI-assisted work on open problems in mathematics. The Collatz proof Lean accepted is a reminder that a checked result is only as reliable as its checker.