Polyhedra in Lean

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

Workshop announcement

Together with Michael Joswig, Georg Loho and Olivia Röhrig, we are planning a 2-weeks hands-on workshop “Polyhedra in Lean” to take place August 24 – September 4, 2026 at FU Berlin. The goal of the workshop is to bring together experts on Lean and formalization, experts on various aspects of polyhedral theory, and young researchers interested in or curious about formalization, with the intent to steer and accelerate the implementation into mathlib by setting up a long term collaboration.

If you are interested in participating, please contact me. More details will be announced soon.

I am leading this project together with Georg Loho (FU Berlin). We are supported by several PhD students

If you are interested in joining, feel free to contact any member of the project.

You can find the current status of the project in Olivia’s GitHub repository, where we also list the currently open and closed PRs into mathlib. This project happens in close collaboration with the lean/mathlib community (mainly on Zulip), and we are the official assignees of polyhedral mathematics for mathlib. See also the Zulip discussion on the topic.