All Events 

2025 MPS Workshop on Lean

Conference

Mathematics & Physical Sciences

When

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

  • All Day

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.

Agenda
9:30 — 10:30 AM Lecture
11:00 AM — 12:00 PM Group work / projects
1:00 — 2:00 PM Lecture
2:30 — 4:00 PM Group work / projects
4:00 — 5:00 PM Short presentations from participants / debrief

More Events

2026 MPS Annual Meeting

Conference

October 15–16, 2026

2026 Simons Collaboration on Extreme Wave Phenomena Based on Symmetries Annual Meeting

Conference

October 22–23, 2026

2026 Simons Collaboration on Confinement and QCD Strings Annual Meeting

Conference

November 5–6, 2026

Speakers

Ofer Aharony, Aleksey Cherman, Gabriel Cuomo SISSA, Davide Gaiotto, Jaume Gomis, + 3 more