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.