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

[This is a guest post by Thomas Hales. This blog post was initially written in a different file format and converted using AI. — T.] Mathematicians have been weighing in on what they value about mathematics. For me, what matters is the consistency of math and its unparalleled reliability in support of science and civilization. Formalization of Math A formal proof is a mathematical proof that has b...