The Polynomial Hirsch ConjectureOpen Problem
## Motivation The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the **polynomial Hirsch conjecture**: is the diameter bounded by a polynomial in $n$ and $d$? ## Timeline - **1957.** Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in *Linear Programming and Extensions* (1963). - **1964–1966.** Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three. - **1967.** Klee and Walkup ([Acta Math.](https://doi.org/10.1007/BF02392971)) refute the *unbounded-polyhedron* version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the **$d$-step conjecture** ($n = 2d$). - **1970.** Larman ([Proc. LMS](https://doi.org/10.1112/plms/s3-20.2.249)) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape. - **1989.** Naddef ([Math. Programming](https://doi.org/10.1007/BF01589418)) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$. - **1992.** Kalai and Kleitman ([Bull. AMS](https://arxiv.org/abs/math/9204233)) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart. - **2010.** Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR](https://doi.org/10.1287/moor.1100.0470)) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches **Polymath 3** on the polynomial version. - **2010–2012.** Santos ([Annals of Math.](https://arxiv.org/abs/1006.2814)) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width. - **2014–2019.** Todd ([SIAM J. Discrete Math.](https://arxiv.org/abs/1402.3579)) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel ([Proc. LMS 2015](https://arxiv.org/abs/1202.4701)) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial. ## Setting Work in $\mathbb{R}^d$. An **H-polytope** is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is $$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$ where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts. A **vertex** of $P$ is an extreme point. Two vertices $u \ne v$ are **adjacent** when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an **edge**. The **combinatorial diameter** of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim. ## Formalization targets ### Goal — the polynomial Hirsch conjecture $$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$ Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents. ### Milestones — the known ladder Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$. ## Significance A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR 2010](https://doi.org/10.1287/moor.1100.0470)) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes. None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge. ## Difficulty The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving *any* polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters *large* is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial. ## Formalization scope The Lean model commits to: ambient space `EuclideanSpace ℝ (Fin d)`; the polytope as `Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i}` for `a : Fin n → EuclideanSpace ℝ (Fin d)`, `b : Fin n → ℝ`, with nonemptiness and `Bornology.IsBounded` as explicit hypotheses (boundedness is essential: Klee–Walkup's *unbounded* counterexample would otherwise trivialize the Santos milestone); vertices as `Set.extremePoints ℝ`; adjacency as `u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v)`; and diameter bounds as the walk predicate `DiamLE`, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through `Real.logb` and the natural floor. In `larman_bound` and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with `todd_bound` requiring full-dimensionality (`(interior P).Nonempty`) as in its source. Welcome contributions: any milestone in any order (`dimension_three_bound` for $d \le 1$ cases and structural lemmas about `Adj` and `DiamLE` are natural entry points, and `kalai_kleitman_bound` is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions. ## Selected references - V. Klee, D. Walkup, *The d-step conjecture for polyhedra of dimension d < 6*, Acta Math. 117 (1967). [doi:10.1007/BF02392971](https://doi.org/10.1007/BF02392971) - D. Larman, *Paths on polytopes*, Proc. London Math. Soc. 20 (1970). [doi:10.1112/plms/s3-20.2.249](https://doi.org/10.1112/plms/s3-20.2.249) - D. Naddef, *The Hirsch conjecture is true for (0,1)-polytopes*, Math. Programming 45 (1989). [doi:10.1007/BF01589418](https://doi.org/10.1007/BF01589418) - G. Kalai, D. Kleitman, *A quasi-polynomial bound for the diameter of graphs of polyhedra*, Bull. AMS 26 (1992). [arXiv:math/9204233](https://arxiv.org/abs/math/9204233) - F. Santos, *A counterexample to the Hirsch conjecture*, Annals of Mathematics 176 (2012). [arXiv:1006.2814](https://arxiv.org/abs/1006.2814) - M. Todd, *An improved Kalai–Kleitman bound for the diameter of a polyhedron*, SIAM J. Discrete Math. 28 (2014). [arXiv:1402.3579](https://arxiv.org/abs/1402.3579) - B. Matschke, F. Santos, C. Weibel, *The width of five-dimensional prismatoids*, Proc. London Math. Soc. 110 (2015). [arXiv:1202.4701](https://arxiv.org/abs/1202.4701) - F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, *Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010). [doi:10.1287/moor.1100.0470](https://doi.org/10.1287/moor.1100.0470) - F. Santos, *Recent progress on the combinatorial diameter of polytopes and simplicial complexes*, TOP 21 (2013) (survey). [arXiv:1307.5900](https://arxiv.org/abs/1307.5900)