GoKawiilLean Theorem Prover highlighted as leading tool for formal math verification
A guest post by mathematician Thomas Hales surveys the state of formal proof verification, noting that major theorems—including Fermat's Last Theorem, the sphere packing problem, and Navier-Stokes forced blowup—have recently been formally verified using computer proof assistants. Hales identifies Lean, created by Leo de Moura at Microsoft in 2013 and later open-sourced, as the proof assistant now most favored by mathematicians among several competing systems like Coq, Isabelle, and HOL Light.