TL;DR
This paper introduces a safe computational framework using exact integer programming and formal verification to produce reliable machine-assisted proofs, demonstrated by confirming Chvátal's conjecture for small cases.
Contribution
It presents a novel, verified approach combining exact integer programming with formal proof checking to ensure correctness of computational proofs in mathematics.
Findings
Verified Chvátal's conjecture for all cases with up to seven elements.
Developed a self-contained certificate verification method for integer programming results.
Ensured correctness of input data using the Coq proof assistant.
Abstract
We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems. At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point roundoff errors present in most state-of-the-art solvers for mixed-integer programs. The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate. This acts as a safeguard against programming errors that may be present in complex solver software. The viability of this approach is tested by applying it to finite cases of Chv\'atal's conjecture, a long-standing open question in extremal combinatorics. We…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
