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
TBA
Registration
A registration form will be made available soon. In the meantime, contact an organizer to indicate interest.
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 our project GitHub repository (will be shared here before the workshop)
Funding
We thankfully acknowledge the supporty by MATH+.
