On July 25, a repository appeared on GitHub containing what looked like an axiom-free Lean 4 disproof of the Collatz conjecture — one of those problems that sits unsolved for eighty years while looking deceptively simple. No sorry. No admitted gaps. The proof checked.

It wasn’t a disproof. It was a kernel exploit.

Leonardo de Moura’s postmortem published August 1 explains what actually happened. When Lean’s kernel eliminates nested inductive types whose parameters are “phantom” — declared but never appearing in constructor fields — those parameters vanish from the generated auxiliary type before type checking runs. An adversarial metaprogram can hand the kernel an inductive declaration that slips an ill-typed argument through this gap and produce a proof of False. With False provable, you can derive anything, including a Collatz disproof. The #print axioms command reports nothing suspicious, because the exploit operates below the layer that command inspects.

Kiran Gopinathan reduced it to a minimal False proof and opened issue #14576 on July 28. The fix landed within the hour.

That would be an interesting but tidy story — bug found, bug fixed — except for one detail. The proof object was built to pass not just Lean’s official kernel, but also Nanoda, an independent Rust-based kernel reimplementation that exists precisely to cross-check proof objects against a completely separate codebase. It passed both because it hit two entirely different bugs, each in the right place for the other to miss. The official kernel had the phantom-parameter logic error. Nanoda had a separate issue with projection node type name validation. The proof was threaded through both gaps simultaneously.

Whether this was intentional design or a lucky coincidence of whatever AI produced it, de Moura’s read is unambiguous: “This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.”

That’s the part worth sitting with. Proof assistants operate on a small-kernel trust model: the entire security argument rests on the kernel being correct, because everything above it — elaboration, tactics, the macro system — can be wrong as long as the kernel catches it. The kernel is supposed to be small enough to audit, and the Lean 4 kernel is intentionally kept compact. It has had prior soundness bugs; this is not the first. But the threat model until recently was mostly human mathematicians doing clever things with metaprogramming. The new threat model is AI systems that can rapidly probe thousands of edge cases in kernel logic, finding the combinations that slip through.

Lawrence Paulson’s commentary, written the day before the postmortem, makes the architectural argument: HOL-style systems that derive complex features (recursion schemes, inductive definitions, pattern matching) from a minimal axiom set rather than building them into the kernel have a structurally smaller attack surface. Lean chose expressiveness and ergonomics, which means a larger kernel. There are real tradeoffs either way — HOL Light is not how most people want to write proofs — but the kernel bug validates Paulson’s concern about what happens when the system gets adversarial inputs.

The Lean Foundation’s response went beyond the immediate patch: five additional bugs identified by AI security specialists were fixed in PRs #14607-#14616, Nanoda was integrated into a daily comparison pipeline, and regression tests now live in a Kernel Arena. That’s the kind of institutional hardening that actually changes the security posture over time. But de Moura’s prediction frames where this is going: the proof community has spent years worrying about whether AI-generated proofs are mathematically sound. Now it has to worry about whether AI-generated proofs are weaponized.

The Collatz conjecture is still open.