Lean is a piece of software which formally verifies mathematical proofs. The user inputs a theorem statement, and then interacts with the system while providing the proof. At the end of the process, Lean has verified that the proof is valid. What sets Lean apart from other proof assistant is the community effort to build a unified repository of mathematics: mathlib. As a result of this, formalizing modern research-level math is becoming more realistic. Some examples from the past few years:
Formalizing work of Clausen-Scholze on condensed mathematics on Scholze’s request,
Campos, Giffiths, Morris and Sahasrabudhe’s upper bound on Ramsay numbers is formalized before it receives a referee report,
Gowers-Green-Manners-Tao is formalized in three weeks, before it was even submitted
A good first step to test out lean is Kevin Buzzard’s natural number game.
The aim of the study group is for the participants to gain familiarity with the Lean system and perhaps end at a level where they would be able to contribute to mathlib if they choose.
Monday at 2:30PM in C514 starting on 9/5.