2025 MPS Workshop on Lean

Meeting Goals

Week 1 (June 16-20th) is devoted to training PhD students and postdocs on formalization via three courses teaching mathematics in a fashion that is bilingual with Lean:

• one in Analysis (sequences and series, limits of real-valued functions, continuity, etc),
• one in Geometry/Topology (group actions on affine space, Euclidean space, etc), and
• one in Algebra/Number Theory (rings, unique factorization domains, congruence, finite fields, quadratic reciprocity, etc).

The goal is to formalize solutions of exercises at an undergraduate level. This would bring the participants to a serious Lean proficiency and also serve as a “real life” test and demonstration of the Mathlib library.

Week 2 (June 23-27th), participants from week 1 are joined by senior researchers for talks and projects at a more advanced level, including:

• Learning basics of metaprogramming and tactic writing,
• Working with git and “blueprint” technology,
• Concerted efforts to make progress on ongoing large collaborative projects in Lean, such as the FLT or PNT+ projects, among other more traditional projects.

All lectures will be recorded and posted to YouTube, where they can potentially be useful to a much larger audience.