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

Lean is a popular open-source theorem prover that allows mathematicians to create exhaustively checked formal proofs at the foundation level of mathematics and logic. The Lean mathematical library (mathlib) has grown to contain nearly 300,000 formalized theorems and over 2.5 million lines of code, enabling mathematicians to build upon previously verified results. Recent high-profile formalizations including Fermat's Last Theorem, the Navier-Stokes forced blowup, and sphere packing problems have demonstrated the potential of computer-assisted proof verification.