What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI
Summary
Terence Tao and Thomas Hales discuss the Lean Theorem Prover’s reliability, the role of autoformalization in math, and the challenges of AI-assisted formal verification. The piece covers Lean’s type theory (CIC), the size and vetting of mathlib, milestones in autoformalization, a recent period termed the Summer of Soundness Bugs, and three proposed strategies to improve kernel reliability: multiple kernels, formal verification, and deeper metatheory.