Polyhedra in Lean

Workshop announcement

Together with Georg Loho and Olivia Röhrig, we are organizing a 2-weeks hands-on workshop “Polyhedra in Lean” to take place August 24 – September 4, 2026 at FU Berlin.

Together with Georg Loho (FU Berlin) we are leading the formalization project Polyhedra in Lean which has the goal of developing a robust, general and easy to use implementation of polyhedral geometry and combinatorics in the Lean proof assistant, aiming for integration into mathlib.

We are supported by

• Olivia Röhrig (leading PhD student, Zuse Institute Berlin)
• John Maar (PhD student at TU Berlin)
• Kilian Rueß (PhD student at UT Nürnberg)
• Mara Gruß (student at FU Berlin)
• Valentina Taylor Cerra (student at FU Berlin)

If you are interested in joining, feel free to contact us.

You can find the current status of the project in Olivia’s GitHub repository. This project happens in close collaboration with the lean/mathlib community (organized on Zulip), and we are the official assignees of polyhedral mathematics for mathlib. See also the Zulip discussion on the topic and the thread on open PRs for what we are pushing to mathlib right now.