AI Exploits Bugs in Lean Math Proof Verifier — SkimNews
Get the Health newsletter
Daily health & science — research, biotech, public health, the studies worth knowing. Free.
- Ramana Kumar announced in July that he had disproved the Collatz conjecture with a Lean formalisation, but it turned out he had used AI to find and exploit two separate bugs in two separate Lean kernels — something Lean's creator Leonardo de Moura described as 'something that we thought was impossible.'
- Leonardo de Moura created Lean at Microsoft Research in the 2010s as a niche tool for human mathematicians; it has since become the leading verification software used by AI companies to back announcements like OpenAI's recent Navier-Stokes proof.
- Lean's roughly 20 full-time developers responded by formalising their own kernel using Lean itself in a self-referential safety check, converting that kernel into a different programming language using AI, and writing a third kernel from scratch; the next version of Lean will ship with four kernels as standard instead of one.
- Google DeepMind maintains the Formal Conjectures list of open math problems explicitly defined in Lean and checked by mathematicians, and when OpenAI solved the Navier-Stokes puzzle earlier this month, the statement provided to Lean was taken directly from that list.
- Working with OpenAI engineers, the Lean team found a bug in the compiler runtime — the compiled code actually executed by a computer — that let them claim a false conjecture was proved, showing the attack surface extends beyond Lean's own code.
- Kevin Buzzard at Imperial College London warned that Lean code can be crafted maliciously to redefine operations and claim false proofs — for example, redefining addition to 'prove' Fermat's last theorem — loopholes that are also now being closed in the tool.
Why it matters: AI companies have used Lean to back headline-grabbing proof announcements, including OpenAI's recent Navier-Stokes solution; now that an engineer has shown AI can hack that verifier, those claims rest on increasingly elaborate but still imperfect defenses — multi-kernel cross-checks that Leonardo de Moura concedes could still be broken by future AI models.
Ask SkimNews
