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
A detailed schedule will be announced in July.
The main part of the workshop will consist of group work, formalizing selected topics around polytopes/polyhedra in Lean. We also plan to have one talk per day on the topics of Lean, formalization, AI and/or polyhedral geometry and combinatorics.
Registration
The capacity of the workshop has been reached and the official registration is now closed. If you are still interested in participating, and would like to be added to the waiting list, please fill in the form here.
There are limited travel funds available for young researchers. If you would like to apply for them, please send us a short motivation letter (max 1 page) and the name and email address of one reference we may contact. The deadline is July 1, 2026.
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
- VSCode or some other Lean capable IDE
- a git installation and some experience with using GitHub
- a typechecked clone of the workshop GitHub repository (will be shared here before the workshop)
Funding
We thankfully acknowledge the supporty by MATH+ and the SPP 2458 “Combinatorial Synergies”.
