New Frontiers of Formal Proof Revolution
Date:
Abstract:
Mathematicians have used machines and datasets to aid their research for millennia. In our time, computational tools such as computer algebra systems, SAT/SMT solvers, Reinforcement Learning, and LLMs play an increasingly central role in mathematical discovery. Complementing these, formal verification and proof assistants ensure the correctness of mathematical arguments, providing mathematicians with instant and extremely high confidence in formalized results and enabling large-scale collaboration. This formal proof revolution is transforming how we produce, organize, and interact with mathematical knowledge.
In this talk, I will introduce Lean, a popular proof assistant based on dependent type theory. I will give an overview of Lean’s community-based mathematical library Mathlib. I will survey the state of the art in using Lean in mathematical research. Finally, I will highlight Lean’s powerful metaprogramming framework, and how we are employing it in a new collaborative project to bring Homotopy Type Theory (HoTT) and synthetic homotopical reasoning into Lean4.