A Safe Computational Framework for Integer Programming applied to Chv\'atal's Conjecture

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 take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant. As a result, we are able to provide a first machine-assisted proof that Chv\'atal's conjecture holds for all downsets whose union of sets contains seven elements or less.