August 1, 2026
Proof? More like proof-ish
Postmortem for Kernel Soundness Bug #14576
AI ‘disproved’ Collatz, then the comments section had a field day
TLDR: An AI-assisted fake “disproof” of Collatz exposed a real bug in Lean’s proof checker, and the fix landed fast. The comments turned it into a bigger drama about whether AI-generated proofs can be trusted at all — with plenty of jokes, doom, and “we saw this coming” energy.
The real spectacle here wasn’t just a bug in Lean, a proof-checking system used to verify math and code — it was the instant community pile-on after an AI-assisted repo appeared to “disprove” the famous Collatz conjecture. For a hot minute, it looked like a machine had pulled off the impossible. Then came the twist: the proof only worked because it slipped through a bug in Lean’s core checker. Developers patched it within an hour of the report, but not before the internet got exactly what it loves: a fake math apocalypse, followed by extremely online forensic drama.
The strongest reaction was basically, “Yep, called it.” One commenter compared AI to water finding cracks in a pipe, with Lean as the pipe and Collatz as the clog — a delightfully chaotic metaphor for “of course the model found the weak spot.” Others turned the moment into a broader trust issue: if an AI can produce something that looks like a formal proof, does “computer-verified” still feel comforting? One blunt takeaway from the thread: you can’t blindly trust LLM output, even when it seems to pass the verifier.
There was pushback too. Some commenters argued this isn’t the end of formal verification — bugs happen even in serious tools, and the whole point of independent checkers is to catch them. And then there was the comedy relief: one person innocently asked whether disproving Collatz shouldn’t just mean finding a counterexample, which perfectly captured the vibe of everyone wandering into the discourse mid-firestorm.
Key Points
- •A Lean kernel soundness bug, tracked as #14576, allowed an ill-typed construction to be accepted as a proof of `False` through nested inductive type handling.
- •The issue came to light after Ramana Kumar published an AI-assisted, sorry-free supposed disproof of the Collatz conjecture on July 25, and Kiran Gopinathan reduced it to a minimal exploit on July 28.
- •Lean maintainers pushed a fix about one hour after the report, merged it after review, and released new patch versions.
- •An older version of the independent checker nanoda also accepted the exploit, but for a separate bug involving projection node type-name verification; that bug had already been fixed a week earlier.
- •The article argues that restricting metaprogramming would not solve soundness because the kernel must reject ill-typed declarations independently of untrusted components such as the elaborator.