Connecting Formal Mathematics and Verified Combinatorial Computing in Lean
This project bridges formal mathematics in the LEAN theorem prover with verified combinatorial computing, creating a unified framework where computational enumeration, optimization-based search, and formal proof verification reinforce each other. The goal is to make computational discoveries in combinatorics certifiably correct while simultaneously expanding LEAN's library of verified combinatorial results.
🧑🎓 IOL Project Members
🪙 Funding
This project is being funded by the Berlin Mathematics Research Center MATH+ (project ID MDU-5), itself funded by the German Research Foundation (DFG) under Germany's Excellence Strategy (EXC-2046/1, project ID 390685689) from October 2026 to September 2029.
🔬 Project Description
Formal proof verification and computational combinatorics have largely developed independently: computational results in combinatorics often rely on ad-hoc enumeration code that is never formally verified, while formal proof systems like LEAN rarely interface with high-performance combinatorial search or optimization solvers.
This project develops tooling and methodology to connect these worlds: (1) Verified combinatorial search: integrating LEAN proofs with computational enumeration and branch-and-bound frameworks, ensuring that search results carry formal certificates; (2) Optimization-driven lemma discovery: using constraint programming and integer optimization to guide LEAN proof search for combinatorial conjectures; (3) Library development: building a rich LEAN library of verified combinatorial results (extremal graph theory, Ramsey-type statements, design theory) that can serve as a foundation for future work; (4) Educational outreach: developing tutorials and workshops that teach combinatorialists how to use LEAN for verifying computational results.