A Formal Disproof of the Hirsch Conjecture

TL;DR

This paper presents a fully formal, computational proof in Coq that verifies counterexamples to the Hirsch Conjecture, demonstrating the approach's scalability to high-dimensional polytopes with complex combinatorics.

Contribution

It introduces a novel, certificate-based algorithm for computing polytope diameters within a proof assistant, combining correctness and efficiency for complex cases.

Findings

Successfully verified counterexamples of 20- and 23-dimensional polytopes.

Demonstrated scalability to polytopes with over 73,000 vertices.

Validated the method on well-known classes like cyclic polytopes.

Abstract

The purpose of this paper is the formal verification of a counterexample of Santos et al. to the so-called Hirsch Conjecture on the diameter of polytopes (bounded convex polyhedra). In contrast with the pen-and-paper proof, our approach is entirely computational: we implement in Coq and prove correct an algorithm that explicitly computes, within the proof assistant, vertex-edge graphs of polytopes as well as their diameter. The originality of this certificate-based algorithm is to achieve a tradeoff between simplicity and efficiency. Simplicity is crucial in obtaining the proof of correctness of the algorithm. This proof splits into the correctness of an abstract algorithm stated over proof-oriented data types and the correspondence with a low-level implementation over computation-oriented data types. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g., matrix multiplications, basic routines on sets and graphs), in order to make the derivation of the correctness of the low-level implementation more transparent. Efficiency allows us to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples of Matschke, Santos and Weibel to the Hirsch conjecture, respectively 20- and 23-dimensional polytopes with 36 425 and 73 224 vertices involving rational coefficients with up to 40 digits in their numerator and denominator. We also illustrate the performance of the method by computing the list of vertices or the diameter of well-known classes of polytopes, such as (polars of) cyclic polytopes involved in McMullen's Upper Bound Theorem.