Hirsch猜想的一个形式反证
A Formal Disproof of the Hirsch Conjecture
摘要：
本文对Santos等人关于多面体（有界凸多面体）直径的Hirsch猜想的一个反例进行了形式化验证。与纸笔证明相比，我们的方法是完全计算：我们实现在Coq和证明正确的算法，明确计算，在证明助手，顶点边缘图的多面体以及它们的直径。这种基于证书的算法的独创性是实现简单性和效率之间的权衡。简单性是获得算法正确性证明的关键。这种证明分为面向证明的数据类型上的抽象算法的正确性和面向计算的数据类型上的低级实现的对应性。已经做出了特别的努力来将算法减少到小的基本操作序列（例如，矩阵乘法，集合和图形上的基本例程），以便使低级实现的正确性的推导更加透明。效率使我们能够扩展到具有挑战性的组合多面体。例如，我们正式检查的两个反例的Matschke，桑托斯和韦伯的赫希猜想，分别为20和23维多面体与36 425和73 224顶点涉及有理系数高达40位数的分子和分母。我们还说明了该方法的性能，通过计算的顶点或直径的著名类的多面体，如（极）循环多面体中涉及的McMullen的上限定理。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
