Lean

What is Lean?

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.

What are we doing?

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.  For at least the first two thirds of the semester we will be following Mathematics in Lean by  Avigad and Massot which comes with many exercises.  Due to the nature of the subject matter, our learning will primarily be based on exercises rather than presentations.  Towards the end of the semester we may move on to Lean projects in small groups based on participants progress and interests.

When and where?

Fridays at 3PM  in C514 starting on 9/5.  This is an organizational meeting where we will discuss the plan for the semester in more detail, and anyone who might be interested should feel free to attend with no commitment.  Make sure to bring your laptop so that we can troubleshoot installation issues together.  If you would like to join a mailing list to receive future updates, please sign up here.

Schedule

The plan, subject to change, is to begin each topic in the corresponding meeting and then finish the exercises at home, discussing any difficulties at the start of the next meeting.  References are to "Mathematics in Lean" by Avigad and Massot (Lean 4 version).