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

Mathematics & Physical Sciences

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

2026 Flatiron Wide Autumn Meeting

Conference

November 11–12, 2026

Mathematics & Physical Sciences

2026 Simons Collaboration on New Frontiers in Superconductivity Annual Meeting

Conference

November 12–13, 2026

Speakers

Daniel Agterberg, Erez Berg, Andrei Bernevig, Laura Classen, Dmitri Efetov, + 3 more