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
12:00Lunch (options here)
14:30Group formation
15:00Justus Springer: Introduction to Lean
16:00Michael Rothgang: Introduction to Mathlib

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.

Talks and sessions that supplement or replace the typical group-work programme
Date	Additional program
Wed, 26 August	Workshop photo (week 1) Xavier Allamigeon: Formalizing and Computing with Polyhedra in Rocq Social evening
Thu, 27 August	Moritz Firsching: The Formal Conjectures project
Fri, 28 August	Recap of the week Recreational activity (start ca 15:00)
Mon, 31 August	Kim Völlinger: Polyhedra at Work: Neural Network Verification in Rocq
Tue, 1 September	Yaël Dillies: Using AI for writing Lean
Wed, 2 September	Workshop photo (week 2) Jesús de Loera: AI and the future of Polyhedral Research Social evening
Fri, 4 September	Recap of the week Discussion of the future of the project Official end: 15:00

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
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.

Funding

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