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 have implemented in Coq and proved 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 datatypes and the correspondence with a low-level implementation over computation-oriented datatypes. A special effort has been made to reduce the algorithm to a small sequence of elementary operations (e.g., matrix-vector multiplication, basic routines on graphs), in order to make the derivation of the correctness of the low-level implementation more transparent.

Efficiency allows to scale up to polytopes with a challenging combinatorics. For instance, we formally check the two counterexamples to Hirsch conjecture due to Matschke, Santos and Weibel, respectively $20$- and $23$-dimensional polytopes with $36425$ and $73224$ vertices involving rational coefficients with up to $20$ digits. 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.