Lean plans four proof-checking kernels to guard against AI exploits

Lean's next version will ship with four different proof-checking kernels instead of one, New Scientist reported. These components check the logic of mathematical proofs, and the change follows an AI-assisted stunt that exploited separate bugs in Lean and another kernel to falsely certify a disproof of the Collatz conjecture. Developers have verified several kernels and built more diverse implementations to reduce the chance that one exploit could defeat every checker. Compiler errors remain a separate risk: work with OpenAI engineers uncovered a runtime bug that allowed a false conjecture to be certified despite the source code checks.