Thomas Hales: What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI (guest post on Terence Tao’s blog)

Hales recounts that “several soundness bugs in Lean were uncovered in July and August” 2026. One gave an illicit Collatz disproof and another a short illicit Kepler proof. All were repaired quickly, and mathlib was re-verified. He recommends cross-checking with many of the ~25 independent kernels, formally verified kernels (Candle; Joachim Breitner’s Con-Leche, whose code and proofs were generated by Claude), and better metatheory. He also says no proof should be accepted without “a human audit … to ensure statement fidelity”.