This workshop will take place August 24 – September 4, 2026 at FU Berlin.
We bring together experts on Lean and formalization, experts on the various aspects of polyhedral geometry and combinatorics, and researchers interested in or curious about these topics. Our goal is to plan and accelerate the formalization of the foundations of polyhedral theory in the Lean language and their integration into mathlib, aiming for long term collaboration.
Invited Experts
- Xavier Allamigeon
- Jesús De Loera
- Yaël Dillies
- Moritz Firsching
- Michael Rothgang
- Justus Springer
- Kim Völlinger
Organisers
Schedule
The main part of the workshop will consist of group work, formalizing selected topics around polytopes/polyhedra in Lean. On some days we will have a talk on the topics of Lean, formalization, AI and/or polyhedral geometry and combinatorics.
Opening day Monday, 24 August
- Registration
- Welcome, introduction, technical setup,
repository overview, and project discussion - Lunch (options here)
- Michael Rothgang: Introduction to Mathlib
- Group formation
- Start of group work
Typical group-work day
| Soft start (meet directly in groups) | |
| Lunch (options here) | |
| Talk, information session, etc | |
| All-groups status update |
Talks and special sessions
Unless listed here, the day follows the group-work schedule above.
| Date | Additional program |
|---|---|
| Xavier Allamigeon: TBA | |
| Moritz Firsching: TBA | |
| |
| Kim Völlinger: TBA | |
| Jesús de Loera: AI and the future of Polyhedral Research | |
|
Venue
- Registration: Arnimallee 2 (Villa)
- Group meetings: Arnimallee 6 (Pi Building) SR 031
For a map of the FU campus Dahlen click here.
Registration
The registration is now closed. We extended the format so as to accommodate everyone previously on the waiting list. If you registered on or before July 16, we are pleased to confirm your place in the workshop.
We offer limited travel funds for young researchers. The application is close. All applicants have been contacted about the status of their application.
What you need to participate
There will be a setup session on the first day, but ideally you already come with the following:
- your own computer
- a working Lean installation (note that this also works with the freely licensed vscodium editor)
- VSCode, vscodium or some other Lean capable IDE. You already have this if you followed the guide linked in the line above.
- a git installation
- a typechecked clone of the workshop fork GitHub repository (will be shared here before the workshop)
- an account at the Lean Zulip instance
Funding
We thankfully acknowledge the supporty by MATH+ and the SPP 2458 “Combinatorial Synergies”.
