An AI 'Disproof' of Collatz Slipped Past Two Proof Checkers

TL;DR

On July 25, formal-methods researcher Ramana Kumar published CollatzLean, a repository containing a sorry-free, AI-assisted "disproof" of the Collatz conjecture that type-checked on Lean 4. Three days later, Kiran Gopinathan reduced it to an axiom-free proof of False and filed issue #14576; the kernel fix landed one hour after the report. The uncomfortable detail in Leonardo de Moura's postmortem, published August 1: the fake proof also got past nanoda, an independent Rust reimplementation of the checker, by hitting a second, unrelated bug. The Collatz conjecture, for the record, is fine.

A stunt with a completely straight face

The repo does not present itself as an exploit. The README walks through a modular formalization, pins Lean and Mathlib to v4.32.1, and ships a verification script. The exported result is Collatz.not_conjecture, a negation of the conjecture, with the deadpan note that the argument is "witness-free": it claims a Collatz orbit that never reaches 1 exists without naming a single number. The verification script passes, which was of course the entire problem.

Per the postmortem, the proof was "produced with AI assistance," and in the Lean community the Collatz packaging was read as a flashy gimmick rather than a genuine claim; some maintainers grumbled that a plain proof of False would have made a cleaner bug report. That report came on July 28, when Gopinathan boiled the whole construction down to a tiny declaration named boom whose #print axioms output reads "'boom' does not depend on any axioms." A theorem proving False from nothing is the formal-methods equivalent of dividing by zero on live television.

Two checkers, two unrelated bugs

The kernel bug lives in how Lean handles nested inductive types with phantom parameters. In de Moura's words: "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." Think of a customs form that only lists what the traveler wrote down: the phantom parameters never make it onto the form, so they are exactly the thing that sails through uninspected. Gopinathan's repro abuses the gap by feeding the kernel structure projections applied to a value of the wrong type, and the issue title says the rest: "Kernel accepts wrong-structure projections, allowing an axiom-free proof of False."

The standard defense against a kernel bug is to re-check the proof export with an independent implementation. Here that defense also failed, and this is the part worth staring at. The nanoda checker did verify the spot the official kernel missed, but skipped a different one: it "did not verify the type name in a projection node." Two codebases, two authors, two distinct holes, one fake theorem through both. Jeremy Chen had reported the nanoda bug a week before the kernel bug surfaced, and both are now patched. De Moura's takeaway is measured: "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."

Before you delete your Mathlib checkout: no legitimate proof was ever at risk. Triggering the bug requires a metaprogram that hands a malicious inductive declaration directly to the kernel; nothing the ordinary Lean frontend elaborates can produce it. The issue puts it precisely: "an adversarial metaprogram can add declarations that ordinary Lean code then uses to prove False." De Moura is also explicit that this is an implementation bug, not a hole in Lean's meta-theory, and commenters on Hacker News noted the buggy path had been sitting in the kernel for years. The threat model this changes is narrow but real: artifacts you did not write, produced by authors (human or model) with an incentive to pass the check.

The fix took an hour. The audit is still running.

The response is the most instructive part of the postmortem. Beyond the one-hour hotfix and new patch releases, the team added regression tests, then landed a follow-up PR making the kernel check that nested-occurrence parameters actually behave like parameters. Then they went hunting: six further security PRs fixing kernel programming mistakes "discovered with AI cybersecurity assistance," and three more hardening kernel invariants. The comparator service now runs nanoda by default with daily updates, so the independent checker stays current instead of quietly rotting.

The certificate era just got its first fire drill

The timing is almost too on the nose. The postmortem hit the front page in the same news cycle as OpenAI's ten Lean-certified results from its unreleased Astra model: 548,207 lines of Lean, zero sorry placeholders, and an argument that rests entirely on "do not trust the model, trust the certificate." The CollatzLean exploit pins Lean v4.32.1; OpenAI's ten-proofs repo builds on 4.32.0, the adjacent patch release of the same toolchain line. Nothing about #14576 invalidates those proofs, which were not produced by adversarial metaprograms. But it sharpens what a certificate means: a proof is verified modulo the implementation of the verifier, at a specific patch level, and now demonstrably modulo the second verifier too.

Two comments from people who build these systems frame the moment. Lean contributor Joachim Breitner floated the hypothesis that "the timing coincidence is due to the availability of strong models able to find this bug." And Lawrence Paulson, creator of Isabelle, used the incident to needle the whole architecture: "I am not aware of a single instance where an independent proof checker detected a soundness error that had passed through the kernel." This episode did not break his streak. The independent checker missed it too.

If you are building agent pipelines that accept machine-generated Lean artifacts, the operational lessons are concrete. Update your toolchain, because the patch releases are out. Re-verify with an independent checker, but keep it as current as the kernel itself. And treat submitted proof artifacts that include metaprogramming the way you treat any untrusted code, because that is what they are: #print axioms reported the fake Collatz result as depending on nothing at all.

Key Takeaways

• A sorry-free, AI-assisted "disproof" of the Collatz conjecture published July 25 exploited a Lean 4 kernel soundness bug in nested inductive types with phantom parameters.
• Kiran Gopinathan reduced it to an axiom-free proof of False on July 28 (issue #14576); the fix (PR #14577) shipped one hour after the report.
• The artifact also passed nanoda, an independent checker, via a second, unrelated bug, so cross-checking failed until both implementations were patched.
• No legitimate proofs were affected: the exploit requires an adversarial metaprogram feeding declarations directly to the kernel, which the normal frontend cannot produce.
• The Lean team followed up with eleven kernel PRs, six of them from an AI-assisted security audit, and now runs nanoda daily against current builds.
• For AI-generated math, the trust story survives but gets a footnote: a certificate is only as sound as the current, patched checkers, plural, that accept it.

Sources: Leonardo de Moura, Postmortem for Kernel Soundness Bug #14576, leanprover/lean4 issue #14576, CollatzLean repository, Lawrence Paulson, Why is it all in the kernel?, Hacker News discussion