Workshop Information

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.

Google Sites

Report abuse