Monday, June 16th to Friday, June 27th, 2025
This workshop will take place at the Simons Foundation in NYC.
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.
For 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.
Organizers:
The workshop is organized by Antoine Chambert-Loir (Institut de mathématiques de Jussieu – Paris Rive Gauche), Alex Kontorovich (Rutgers University), and Heather Macbeth (Imperial College London).
Applications:
Participation is limited; to apply please Click here
If you have any problems with the application or other practical questions, please write to simonsleanworkshop2025@gmail.com.
Sponsors:
Travel is fully funded for all admitted participants. This workshop gratefully acknowledges support from the Simons Foundation.