Project
MDU-5
Connecting Formal Mathematics and Verified Combinatorial Computing in Lean
Project Heads
Sebastian Pokutta, Christoph Spiegel
Project Members
Olivia Röhrig
Project Duration
01.09.2026 – 31.08.2029
Located at
ZIB
Description
Algorithms in combinatorics and polyhedral geometry are used across mathematics, science, and engineering, but their implementations are rarely verified. This project develops a refinement methodology for bridging abstract mathematical types to efficient executable code in Lean 4, validated through verified polyhedral and graph algorithms grounded in the community-maintained mathlib library.
External Website
Related Publications
Related Pictures