Workshop — Polyhedra in Lean

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

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

9:00Registration
10:00Welcome, introduction, technical setup,
repository overview, and project discussion (slides)
12:00Lunch (options here)
14:30Group formation
15:00Justus Springer: Introduction to Lean (slides)
16:00Michael Rothgang: Introduction to Mathlib I (slides)

Typical group-work day

Standard daily schedule for group-work days
10:00	Soft start (meet directly in groups)
12:00	Lunch (options here)
14:00	Talk, information session, etc
17:00	All-groups status update

Talks and special sessions

Unless listed here, the day follows the group-work schedule above.

Week I

Date	Additional program
Tue, 25 August	10:30Michael Rothgang: Introduction to Mathlib II (slides) 11:00A short walk through the Polyhedral Repository
Wed, 26 August	Workshop photo (week 1) 14:00Xavier Allamigeon: Formalizing and Computing with Polyhedra in Rocq (slides) Social evening
Thu, 27 August	11:00Discussion: polytope vs. V-polytope vs. H-polytope (Villa) 13:55Workshop photo (week 1) 14:00Moritz Firsching: The Formal Conjectures project
Fri, 28 August	Recap of the week 15:00Recreational activity: Walk around Krumme Lanke

Week II

Date	Additional program
Mon, 31 August	11:00Kick-off meeting for week II 14:00Kim Völlinger: Polyhedra at Work: Neural Network Verification in Rocq (slides)
Tue, 1 September	14:00Yaël Dillies: The Convexity Refactor
Wed, 2 September	14:00Jesús de Loera: AI and the future of Polyhedral Research (slides) Social evening
Thu, 3 September	Workshop photo (week 2) 14:00Yaël Dillies: What Lean tasks are LLMs good at on the 3rd of September 2026?
Fri, 4 September	14:00Recap of the week & future of the project 15:00Official end

Venue

Registration:

Arnimallee 2 (Villa)

All-groups meetings:

Arnimallee 6 (Pi Building) SR 031

Rooms for group work:

Arnimallee 2 (Villa): seminar room, 002, K007
Arnimallee 3: 115, 119, 120
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
VSCode (Microsoft), vscodium (freely licensed) or some other Lean capable IDE. You already have this if you followed the guide linked in the line above.
a git installation
an account at the Lean Zulip instance
a typechecked clone of the workshop fork GitHub repository. You can get it by running the following commands in a command line:
```
  git clone https://github.com/Workshop-Polyhedra-In-Lean/Polyhedral.git
  cd Polyhedral
```
Then download the pre-compiled binaries, otherwise building can take several hours:
```
  lake exe cache get
```
This might take up to 10GB of disk memory and several minutes for downloading depending on your internet connection and computer. Verify that it builds by running
```
  lake build
```
There will be some warnings, most of which come from remaining sorry-s or deprecations. You can ignore them.

Lean resources

To get started with writing Lean, we list here some of the most important learning resources:

Lean learning games
Freely available e-books:
Introduction to Formal Mathematics with Lean 4
Mathlib Phrasebook
Paperproof, a Lean theorem-proving interface designed to feel like pen-and-paper proofs.

For looking up theorems, try Loogle, leansearch or the mathlib documentation.

Group Photo

Week 1

Week 2

Funding

We thankfully acknowledge the supporty by MATH+ and the SPP 2458 “Combinatorial Synergies”.