Lean Bugs Let AI Fake Proof

BonnAn AI exploited 2 Lean kernel bugs to fake a disproof.

Every Lean-verified proof rests on the kernel, the small code that checks the mathematics.

Ramana Kumar’s July claimed Collatz disproof passed both the standard kernel and Nanoda, each carrying a different bug.

“[The AI] managed to do something that we thought was impossible,” said Leonardo de Moura, Lean’s creator.

The next Lean version ships with 4 different kernels as standard.

How each outlet framed it

New Scientist: reveals exploitable bugs in Lean formalisation tool allowing AI to fake proof correctness