What mathematicians should know about the Lean Theorem Prover: reliability & AI

Thomas Hales discusses the reliability of formal proofs and the use of software like the Lean Theorem Prover to exhaustively check mathematical proofs. Formalization projects for Navier-Stokes forced blowup, the sphere packing problem in 8 and 24 dimensions, and Fermat’s Last Theorem were completed this year.