AI Exploits Lean Math Tool Bugs, Developers Harden Defenses — SkimNews
Get the Health newsletter
Daily health & science — research, biotech, public health, the studies worth knowing. Free.
- Ramana Kumar used AI in July to find and exploit two separate bugs in two separate Lean kernels, publishing a fake disproof of the Collatz conjecture that initially passed dual-kernel verification.
- Lean creator Leonardo de Moura said the attack "managed to do something that we thought was impossible"; the bugs were fixed an hour after they were officially logged.
- Lean developers formalized their own kernel using Lean itself as a self-referential safety check, used AI to convert it to a second programming language, and verified a third kernel written from scratch.
- The next version of Lean will ship with four different kernels as standard (it currently ships with one), and developers built a "battle arena" website where kernels compete on known true and false proofs.
- While working with OpenAI engineers, the Lean team found a bug in the runtime — the compiled code produced by the compiler — that let them falsely prove a false conjecture; the flaw was in the compiler, not in Lean's code.
- Google DeepMind maintains the Formal Conjectures list of explicitly defined math problems; OpenAI's Navier-Stokes solution announced this month used a statement taken directly from that list.
- Kevin Buzzard at Imperial College London warns that Lean is just a programming language — users can redefine "addition" and falsely "prove" theorems mentioning it — and that fully verifying an entire hardware/software stack remains "the dream."
Why it matters: Tech companies rely on Lean to publicly announce AI-solved math problems; after AI was shown to exploit the tool's verification kernels, developers are deploying four-kernel checks as standard in the next release. The remaining gap: a compiler bug — not a Lean bug — already let researchers falsely prove a false conjecture, and fully verified hardware/software stacks are years away.
Ask SkimNews
