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
Organisers
Schedule
A detailed schedule will be announced later.
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 capacities are limited. If you are interested in participating, please register until July 16, 2026 by filling 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”.
