Motivation

How densely can equal disks be packed in the plane? The hexagonal arrangement, with centers on the triangular lattice, covers a fraction $\pi/(2\sqrt3)\approx0.9069$ of the plane, and Thue's theorem says no packing does better. In 2003 Cohn and Elkies introduced a linear programming bound for sphere packing: a single auxiliary function whose values are nonpositive outside a ball and whose Fourier transform is nonnegative certifies an upper bound on packing density. Viazovska (dimension 8) and Cohn, Kumar, Miller, Radchenko and Viazovska (dimension 24) found auxiliary functions for which the bound is sharp, solving sphere packing in those dimensions. Cohn and Elkies conjectured that a sharp function exists also in dimension 2 (Conjecture 7.3 of their paper). The planar packing problem itself is classical; the question here is whether the Fourier method certifies it exactly.

Timeline

• 1890s–1940s. Thue's theorem on optimality of the hexagonal circle packing; an elementary proof based on an idea of Rogers is presented by Hales (2000).
• 2003. Cohn and Elkies introduce the linear programming bound and conjecture sharp auxiliary functions in dimensions 2, 8 and 24 (doi:10.4007/annals.2003.157.689).
• 2017. Viazovska constructs the sharp function in dimension 8 (doi:10.4007/annals.2017.185.3.7); Cohn, Kumar, Miller, Radchenko and Viazovska do so in dimension 24 (doi:10.4007/annals.2017.185.3.8).
• 2019. Radchenko and Viazovska prove Fourier interpolation on the real line (doi:10.1007/s10240-018-0101-z).
• 2021. Sardari shows that values and first derivatives on triangular-lattice shells do not determine a planar radial Schwartz function (arXiv:2102.08753).
• 2022. Cohn, Kumar, Miller, Radchenko and Viazovska prove universal optimality in dimensions 8 and 24 via interpolation formulas (doi:10.4007/annals.2022.196.3.3).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims an explicit sharp planar certificate.

Setting

Scale disks to radius $1/2$, so a packing is a set of centers $\mathcal C\subset\mathbb R^2$ with $|x-y|\ge1$ for distinct centers. The Fourier transform is

$$\widehat f(\xi)=\int_{\mathbb R^2}f(x)\,e^{-2\pi i\,x\cdot\xi}\,dx.$$

A Schwartz function is smooth with all derivatives decaying faster than any inverse power of $|x|$. A function is radial if $f(x)$ depends only on $|x|$; for real radial integrable $f$, $\widehat f$ is real and radial. The Cohn–Elkies theorem says that if $f$ is admissible, $f(x)\le0$ for $|x|\ge1$ and $\widehat f\ge0$, then every packing of radius-$1/2$ disks has density at most $\operatorname{vol}B(0,1/2)\cdot f(0)/\widehat f(0)$.

Formalization targets

Goal: Theorem 1.1 (sharp Fourier certificate)

There is a real radial Schwartz function $f:\mathbb R^2\to\mathbb R$ with

$$\widehat f(0)=1,\qquad f(0)=\frac{2}{\sqrt3},\qquad \widehat f(\xi)\ge0\ \ (\xi\in\mathbb R^2),\qquad f(x)\le0\ \ (|x|\ge1).$$

Lean: OAI.sharp_fourier_certificate, open on the platform.

Significance

With $f(0)/\widehat f(0)=2/\sqrt3$ the Cohn–Elkies bound equals $\frac{\pi}{4}\cdot\frac{2}{\sqrt3}=\frac{\pi}{2\sqrt3}$, the hexagonal density, so the theorem answers the two-dimensional case of Cohn–Elkies Conjecture 7.3 affirmatively and gives a Fourier-analytic proof of Thue's theorem for arbitrary (not only periodic) packings. Its zero structure also recovers uniqueness of the triangular lattice among periodic optimal packings. The certificate does not satisfy the additional zero-set requirement of Cohn–Elkies Conjecture 8.1, which remains a separate question. The construction methods feed into the companion work on universal optimality of the triangular lattice in the same family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. By contrast, Viazovska's dimension-8 theorem has been the subject of formalization efforts, so a planar certificate would be a natural low-dimensional companion.

Difficulty

In dimensions 8 and 24 the magic functions come from modular forms, whose symmetries control a function and its Fourier transform at once. No such modular construction is known to produce the planar certificate, and Sardari's nonuniqueness theorem shows that prescribing values and derivatives on the lattice shells does not pin a function down. Numerical Laguerre–Gaussian searches (Cohn–Elkies) approach the bound but do not attain it. The hard part is an exact construction together with rigorous sign control of both $f$ (for $|x|\ge1$) and $\widehat f$ (everywhere), including between interpolation nodes and in the tails.

Formalization scope

• The plane is EuclideanSpace ℝ (Fin 2); the function is a SchwartzMap Plane ℝ.
• SharpPlanar.fourier f ξ is the Bochner integral of $f(x)\exp(-2\pi i\langle x,\xi\rangle)$; for a Schwartz function it is the usual transform.
• SharpCertificate f: Radial f, fourier f 0 = 1, f 0 = 2 / √3, for every ξ the transform has zero imaginary part and nonnegative real part, and f x ≤ 0 when 1 ≤ ‖x‖.
• The goal is pure existence; any certificate, explicit or not, proves it.

A complete development needs Fourier transforms of radial functions in the plane (Hankel transforms, Gaussian pairings) and rigorous interval or Bernstein-polynomial sign certification. Formalizing the Cohn–Elkies bound itself (certificate implies density bound) would be a valuable reusable companion. Contributions formalizing Proposition 2.2, Proposition 3.4 or Proposition 4.3 are welcome.

Selected references

• OpenAI, A sharp Fourier certificate for planar circle packing, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-sharp-Fourier-certificate-for-planar-circle-packing-September-23-2026/paper.pdf
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math., 2003. https://doi.org/10.4007/annals.2003.157.689
• T. C. Hales, Cannonballs and honeycombs, Notices Amer. Math. Soc., 2000.
• M. S. Viazovska, The sphere packing problem in dimension 8, Ann. of Math., 2017. https://doi.org/10.4007/annals.2017.185.3.7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, The sphere packing problem in dimension 24, Ann. of Math., 2017. https://doi.org/10.4007/annals.2017.185.3.8
• D. Radchenko, M. Viazovska, Fourier interpolation on the real line, Publ. Math. IHÉS, 2019. https://doi.org/10.1007/s10240-018-0101-z
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, Universal optimality of the E8 and Leech lattices and interpolation formulas, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.3.3
• N. Talebizadeh Sardari, Higher Fourier interpolation on the plane, preprint, 2021. https://arxiv.org/abs/2102.08753

Motivation

Which arrangement of points in the plane minimizes interaction energy? For many repulsive interactions the expected answer is the triangular (hexagonal) lattice. Universal optimality, formulated by Cohn and Kumar (2007, doi:10.1090/S0894-0347-06-00546-7), asks for a single configuration that minimizes energy simultaneously for every completely monotone potential of squared distance, which includes all Gaussians and all inverse powers. It was proved in dimensions 8 and 24 for $E_8$ and the Leech lattice; in dimension two it was a conjecture. The question matters in mathematical physics (crystallization, vortex lattices, Coulomb and Riesz gases) and in the theory of Fourier interpolation.

Timeline

• 1953–1964. Rankin, Cassels, Ennola and Diananda show that the triangular lattice minimizes the Epstein zeta function among planar lattices (doi:10.1017/S2040618500035668, doi:10.1017/S2040618500033906).
• 1988. Montgomery proves the Gaussian (theta-function) minimum among planar lattices of fixed covolume for every parameter (doi:10.1017/S0017089500007047).
• 2003. Cohn and Elkies introduce Fourier linear-programming bounds for sphere packing (doi:10.4007/annals.2003.157.689).
• 2007. Cohn and Kumar formulate the Euclidean universal-optimality program (Conjecture 9.4).
• 2018. Cohn and de Courcy-Ireland extend the Fourier comparison to density-based competitor classes (doi:10.1215/00127094-2018-0018).
• 2019. Radchenko and Viazovska develop Fourier interpolation on the line (doi:10.1007/s10240-018-0101-z).
• 2022. Cohn, Kumar, Miller, Radchenko and Viazovska prove universal optimality of $E_8$ and the Leech lattice (doi:10.4007/annals.2022.196.3.3).
• 2024–2025. Partial planar results: comparisons with periodic classes (Faulhuber–Shafkulovska–Zlotnikov, doi:10.1090/bproc/247), small periodic configurations (Hardin–Tenpas, doi:10.19086/da.144978), and local optimality under small displacements (Leblé, arXiv:2511.03353).

The source of this mission, an OpenAI preprint dated September 26, 2026, claims the full planar statement against all locally finite configurations of density one. A companion OpenAI preprint reaches the same energy conclusion by a different (modulo-12) interpolation construction.

Setting

Let $b=\sqrt3/2$ and $A=b^{-1/2}\{m(1,0)+n(1/2,b):m,n\in\mathbb Z\}$, the triangular lattice of covolume one. Let $B_R$ be the closed disk of radius $R$ about the origin. A set $\mathcal C\subset\mathbb R^2$ is locally finite if each $\mathcal C\cap B_R$ is finite, and has centered disk density one if $N_R/(\pi R^2)\to1$, where $N_R=\#(\mathcal C\cap B_R)$.

A smooth $g:(0,\infty)\to[0,\infty)$ is completely monotone if $(-1)^jg^{(j)}(t)\ge0$ for all $j\ge0$, $t>0$. The lower energy per particle is

$$E_g(\mathcal C)=\liminf_{R\to\infty}\frac1{N_R}\sum_{\substack{x,y\in\mathcal C\cap B_R\\ x\ne y}}g(|x-y|^2)\in[0,\infty],$$

summing over ordered pairs. The Fourier transform is $\widehat f(\xi)=\int f(x)e^{-2\pi i x\cdot\xi}\,dx$ and $A^*=\{\xi:\xi\cdot a\in\mathbb Z\ \forall a\in A\}$ is the dual lattice.

Formalization targets

Milestone: Theorem 1.2 (sharp Gaussian minorants)

For every $\alpha>0$ there is a real radial Schwartz $f_\alpha$ with

$$f_\alpha\le e^{-\pi\alpha|x|^2},\quad \widehat f_\alpha\ge0,\quad f_\alpha(a)=e^{-\pi\alpha|a|^2}\ (a\in A\setminus\{0\}),\quad \widehat f_\alpha(w)=0\ (w\in A^*\setminus\{0\}),$$

given for $\alpha\ge1$ by the paper's explicit atomic interpolation construction.

Goal: Theorem 1.1 (universal energy minimum)

For every smooth nonnegative completely monotone $g$ and every locally finite $\mathcal C$ of centered disk density one,

$$E_g(\mathcal C)\ \ge\ \sum_{a\in A\setminus\{0\}}g(|a|^2)\ =\ E_g(A)\qquad\text{in }[0,\infty].$$

Lean: OAI.AtomicTriangular.universal_energy_minimum, open on the platform.

Significance

Theorem 1.1 would settle the planar case of the Cohn–Kumar universal-optimality conjecture in a density-based competitor class with no periodicity or perturbation assumption, for every completely monotone potential including those (such as $t^{-p}$ with $p\le1$) whose lattice sums diverge. By Bernstein's theorem such potentials are mixtures of Gaussians, so the sharp Gaussian certificates of Theorem 1.2 are the analytic core. The theorem identifies the minimum value; it does not classify minimizers. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formalization would also produce reusable Fourier-analytic tools in Lean (Poisson summation for lattices, linear-programming energy bounds).

Difficulty

Lattice-restricted results (Rankin, Montgomery) compare only lattices; a competitor here may be nonperiodic, have arbitrarily close pairs, and have large local clustering. The Fourier linear-programming method handles general competitors but needs, for each Gaussian, an auxiliary function that is simultaneously a pointwise minorant, has nonnegative Fourier transform, and is sharp: it must touch the Gaussian on every lattice shell and its transform must vanish on every dual shell. Constructing such functions for all $\alpha>0$ at once, with rigorous sign control between the interpolation nodes, is the central obstacle. A second issue is passing from the density hypothesis alone (no averaging over translates) to the energy inequality.

Formalization scope

• Points live in EuclideanSpace ℝ (Fin 2); A is Set.range triangularPoint.
• AdmissiblePotential g: ContDiffOn ℝ ⊤ g (Ioi 0), $g\ge0$ and $(-1)^r$ iteratedDeriv r g t $\ge0$ for $t>0$.
• energy g C is the liminf over $R\to\infty$ of diskEnergy, valued in ℝ≥0∞; latticeEnergy g is a tsum in ℝ≥0∞, so divergent sums are allowed and no summability hypothesis is needed.
• The goal returns both the inequality for every admissible C and the equality latticeEnergy g = energy g A.
• For Theorem 1.2, realFourier is Mathlib's 𝓕 (kernel $e^{-2\pi i\langle x,\xi\rangle}$) applied to the complexified function; the $\alpha\ge1$ clause names the paper's explicit coefficients (R, R0, Yf, Uplus, Uminus) and error bounds.

Contributions formalizing Lemma 2.1 (reciprocal Gaussian parameters), Proposition 2.3 (density-only linear programming), Lemma 4.1 (finite certificate) and Proposition 5.1 (exact interpolation and approximation) are welcome.

Selected references

• OpenAI, An atomic certificate for triangular-lattice universal optimality, preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-atomic-certificate-for-triangular-lattice-universal-optimality-September-26-2026/paper.pdf
• H. Cohn, A. Kumar, Universally optimal distribution of points on spheres, J. Amer. Math. Soc., 2007. https://doi.org/10.1090/S0894-0347-06-00546-7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, Universal optimality of the E8 and Leech lattices and interpolation formulas, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.3.3
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math., 2003. https://doi.org/10.4007/annals.2003.157.689
• H. Cohn, M. de Courcy-Ireland, The Gaussian core model in high dimensions, Duke Math. J., 2018. https://doi.org/10.1215/00127094-2018-0018
• H. L. Montgomery, Minimal theta functions, Glasgow Math. J., 1988. https://doi.org/10.1017/S0017089500007047
• R. A. Rankin, A minimum problem for the Epstein zeta-function, 1953. https://doi.org/10.1017/S2040618500035668
• D. Radchenko, M. Viazovska, Fourier interpolation on the real line, Publ. Math. IHÉS, 2019. https://doi.org/10.1007/s10240-018-0101-z
• T. Leblé, The hexagonal lattice is universally locally optimal, preprint, 2025. https://arxiv.org/abs/2511.03353

Motivation: cut metrics, flows and the planar embedding conjecture

A finite metric space embeds into $L_1$ exactly when its metric is a nonnegative combination of cut metrics $\delta_S(x,y)=|\mathbf 1_S(x)-\mathbf 1_S(y)|$. For this reason the least distortion with which a graph metric embeds into $L_1$ governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst $L_1$ distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into $L_1$ with uniformly bounded distortion. The planar case has been the central open instance.

Timeline

• 1981 — Okamura and Seymour: multicommodity flows in planar graphs with all terminals on one face (JCTB 1981), giving isometric $L_1$ representations of one-face metrics.
• 1993 — Klein, Plotkin and Rao: decompositions of graphs excluding a fixed minor (STOC 1993).
• 1999 — Rao: every $n$-vertex planar metric embeds into $L_1$ (via Euclidean space) with distortion $O(\sqrt{\log n})$ (SoCG 1999).
• 2003 — Newman and Rabinovich: series-parallel metrics may need $\Omega(\sqrt{\log n})$ distortion into Euclidean space, so the Euclidean route cannot give a constant (DCG 2003).
• 2004 — Gupta, Newman, Rabinovich and Sinclair: constant distortion for series-parallel graphs, and the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: $k$-outerplanar graphs, with a bound exponential in $k$ (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent: sharp bound $2$ for series-parallel graphs (FOCS 2008); Lee and Raghavendra: matching lower bound (DCG 2010). Lee and Sidiropoulos relate the planar case to the full conjecture (STOC 2009).
• 2013 — Sidiropoulos: constant distortion for planar metrics realized in nonpositively curved simply connected surfaces (FOCS 2013).
• 2019–2025 — Face-cover bounds by Krauthgamer, Lee and Rika (SODA 2019) and Filtser (TALG 2025); Abraham, Filtser, Gupta and Neiman recover Rao's bound via shortest-path decompositions (SICOMP 2022).
• 2026 — An OpenAI preprint, Planar Graph Metrics Embed into $L_1$ with Constant Distortion (OpenAI Math Release, September 23, 2026), claims the planar case of the GNRS conjecture. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite connected simple graph on vertex set $V=\{0,\dots,n-1\}$ with symmetric edge lengths $\ell(u,v)=\ell(v,u)>0$ on edges. The graph metric $d_G(x,y)$ is the infimum of $\sum\ell(e)$ over walks from $x$ to $y$. $G$ is planar if it has a drawing in $\mathbb R^2$: distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.

A map $f:V\to L_1(\Omega,\mu)$ into the real $L_1$ space of some measure space has distortion at most $C$ if $d_G(x,y)\le\|f(x)-f(y)\|_1\le C\,d_G(x,y)$ for all $x,y$.

Formalization targets

Goal: Theorem 1.1 (planar graph metrics in $L_1$)

There is a constant $C\ge1$ such that for every $n$, every connected planar graph $G$ on $n$ vertices and every symmetric positive edge-length function $\ell$, there are a measure space $(\Omega,\mathcal F,\mu)$ and $f:V\to L_1(\Omega,\mathcal F,\mu;\mathbb R)$ with

$$d_G(x,y)\;\le\;\|f(x)-f(y)\|_1\;\le\;C\,d_G(x,y)\qquad(x,y\in V).$$

The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.

Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an $L^1$ space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.

Difficulty

Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show $\Omega(\sqrt{\log n})$ Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.

Formalization scope

• Vertices are Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so $n\ge1$). Singletons are allowed.
• IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.
• Edge lengths are a function Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.
• The target space is MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into $f$).
• Infrastructure needed: plane drawings and their combinatorial consequences (rotation systems, noncrossing column models), cut-metric representations of $L_1$ metrics, and the probabilistic multiscale construction. Plane-drawing and cut-metric infrastructure is reusable.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995). https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An $O(\log k)$ approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica (2004). https://doi.org/10.1007/s00493-004-0015-x
• S. Rao, Small distortion and volume preserving embeddings for planar and Euclidean metrics, SoCG 1999. https://doi.org/10.1145/304893.304983
• I. Newman, Y. Rabinovich, A lower bound on the distortion of embedding planar metrics into Euclidean space, Discrete Comput. Geom. (2003). https://doi.org/10.1007/s00454-002-2813-5
• C. Chekuri, A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Embedding $k$-outerplanar graphs into $\ell_1$, SIAM J. Discrete Math. (2006). https://doi.org/10.1137/S0895480102417379
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, A. Sidiropoulos, On the geometry of graphs with a forbidden minor, STOC 2009. https://doi.org/10.1145/1536414.1536450
• A. Sidiropoulos, Non-positive curvature and the planar embedding conjecture, FOCS 2013. https://doi.org/10.1109/FOCS.2013.27
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. (2022). https://doi.org/10.1137/19M1296021
• A. Filtser, A face cover perspective to $\ell_1$ embeddings of planar graphs, ACM Trans. Algorithms (2025). https://doi.org/10.1145/3686800
• OpenAI, Planar Graph Metrics Embed into $L_1$ with Constant Distortion, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf

Motivation

The volume product of a convex body measures how large a body and its polar can simultaneously be. For a body without a distinguished centre, the polar is taken about the point that makes it smallest, the Santaló point, so the product is invariant under all invertible affine maps. The Blaschke–Santaló inequality identifies ellipsoids as the maximizers. Mahler's conjecture for general convex bodies asks for the minimizers and predicts simplices, with minimum value $(n+1)^{n+1}/(n!)^2$. The question arose from Mahler's work on polarity and the geometry of numbers, and it is the sharp form of the Bourgain–Milman reverse Santaló inequality.

This mission asks for a formal proof of the general Mahler conjecture with its equality case, as stated in an OpenAI preprint dated September 22, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

• 1938–1939 — Mahler proves the planar inequality among polygons with triangles as equality cases (Ein Minimalproblem für konvexe Polygone, Mathematica (Zutphen) B, 1938) and formulates the higher-dimensional problem (Časopis 1939).
• 1949 — Santaló's affine invariant and the centre now named after him (Portugaliae Math., 1949).
• 1987 — Bourgain and Milman prove an inverse Santaló inequality with an exponential constant (Invent. Math. 1987).
• 1991 — Meyer completes the planar case for arbitrary convex bodies: triangles are exactly the minimizers (Monatsh. Math. 1991).
• 2006 — Meyer and Reisner use shadow systems to prove the sharp inequality for polytopes with at most $n+3$ vertices (Mathematika 2006).
• 2008–2012 — Kuperberg's explicit lower bounds via Gauss linking integrals (GAFA 2008); Nazarov's complex-analytic proof of Bourgain–Milman (GAFA seminar 2012).
• 2011 — Kim and Reisner prove strict local minimality at every simplex (Mathematika 2011).
• 2018 — Klartag's cone/Laplace-transform formulation of Mahler volumes (Adv. Math. 2018).
• 2024 — Mastrantonis and Rubinstein extend Nazarov's method to nonsymmetric bodies (arXiv:2206.06188).
• 2026 — Chen, Li, Xi and Xu prove the three-dimensional general case with tetrahedra as minimizers (arXiv:2605.09334).
• September 2026 — The OpenAI preprint claims the general conjecture in every dimension (Theorem 1.1, p. 1).

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior; $|\cdot|$ is Lebesgue measure and $\langle\cdot,\cdot\rangle$ the Euclidean inner product. For an interior point $z$, the polar of $K$ about $z$ is

$$(K-z)^\circ=\{y\in\mathbb R^n:\ \langle y,x-z\rangle\le1\ \text{for all }x\in K\},$$

and the volume product is

$$P(K)=\inf_{z\in\operatorname{int}K}|K|\,|(K-z)^\circ|.$$

The infimum is attained at the unique Santaló point $s(K)$. A simplex is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: the general Mahler conjecture (Theorem 1.1, p. 1)

For every $n\ge1$ and every convex body $K\subset\mathbb R^n$,

$$P(K)\ \ge\ \frac{(n+1)^{n+1}}{(n!)^2},$$

with equality if and only if $K$ is a simplex.

Significance

The result itself. It is the exact form of a problem open since the 1930s and previously settled only in dimensions $2$ and $3$ and for polytopes with few vertices. Because the infimum over centres is taken, it gives the same lower bound for $|K||(K-z)^\circ|$ at every interior point $z$. Via the known geometric-to-functional implication, the preprint derives the sharp functional Mahler inequality for log-concave functions and an entropy–transport inequality (Corollary 1.2, p. 4; Corollary 8.1, p. 41). The symmetric conjecture, with the larger constant $4^n/n!$, is a different statement treated in a companion preprint.

Formalizing it. The proof combines convex cones and their Laplace transforms, Gaussian Sobolev calculus, Moreau's decomposition, matrix divided differences, and certified one-variable inequalities. A formal proof would provide checked versions of these tools and of the Santaló point's existence and uniqueness. No machine-checked proof of the conjecture in any dimension $n\ge2$ is known.

Difficulty

Symmetrization does not apply, the volume product is not convex along natural deformations except in restricted families (shadow systems), and local minimality at simplices says nothing about distant bodies. In the preprint's route the main obstacle (Introduction, pp. 2–3) is that the Jacobian matrices $P_z=D\Pi_C(Z+\xi_z)$ of the Gaussian-averaged cone projections neither commute nor increase in $z$: bounding them separately loses both the sharp constant and the equality case. Controlling them jointly requires comparing the whole family with spectral thresholds of a linear Gaussian matrix (Sections 5–7), and equality must then force the cone to split into half-lines.

Formalization scope

• Bodies are subsets of EuclideanSpace ℝ (Fin n) with IsCompact, Convex ℝ and nonempty interior, and $n\ge1$.
• polarAt K z is the polar about $z$; volumeProduct K is the sInf over interior K of (volume K).toReal * (volume (polarAt K z)).toReal. For an interior $z$ the polar is bounded, so toReal reads the true volume; the index set is nonempty because the interior is.
• The goal is a conjunction: the inequality, and volumeProduct K = (n+1)^(n+1)/(n!)^2 iff K = convexHull ℝ (range v) for some affinely independent v : Fin (n+1) → _.
• The Santaló point is not named in Lean; using the infimum over interior points is equivalent to evaluating at $s(K)$ because the infimum is attained there (Section 2 of the preprint).

Welcome contributions: polar bodies and their volumes in Mathlib, the Santaló point, Laplace transforms of convex cones, and Gaussian integration by parts.

Selected references

• OpenAI, The Mahler Conjecture for General Convex Bodies, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Mahler-Conjecture-for-General-Convex-Bodies-September-22-2026/paper.pdf
• OpenAI, The symmetric Mahler conjecture and its equality cases, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-symmetric-Mahler-conjecture-and-its-equality-cases-September-22-2026/paper.pdf
• K. Mahler, Ein Übertragungsprinzip für konvexe Körper, Časopis Pěst. Mat. Fys. 68 (1939). https://doi.org/10.21136/CPMF.1939.109441
• M. Meyer, Convex bodies with minimal volume product in $\mathbb R^2$, Monatsh. Math. (1991). https://doi.org/10.1007/BF01351770
• J. Bourgain, V. Milman, New volume ratio properties for convex symmetric bodies in $\mathbb R^n$, Invent. Math. (1987). https://doi.org/10.1007/BF01388911
• G. Kuperberg, From the Mahler conjecture to Gauss linking integrals, GAFA (2008). https://doi.org/10.1007/s00039-008-0669-4
• M. Meyer, S. Reisner, Shadow systems and volumes of polar convex bodies, Mathematika (2006). https://doi.org/10.1112/S0025579300000061
• J. Kim, S. Reisner, Local minimality of the volume-product at the simplex, Mathematika (2011). https://doi.org/10.1112/S0025579310001555
• B. Klartag, Isotropic constants and Mahler volumes, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.03.009
• V. Mastrantonis, Y. A. Rubinstein, The Nazarov proof of the non-symmetric Bourgain–Milman inequality, Indiana Univ. Math. J. (2024). https://arxiv.org/abs/2206.06188
• S. Chen, Y. Li, D. Xi, Z. Xu, The Mahler Conjecture in Three Dimensions, preprint (2026). https://arxiv.org/abs/2605.09334v3

Motivation

The learning with errors (LWE) problem underlies much of post-quantum public-key cryptography, and its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). Every step of that reduction is calibrated by the smoothing parameter $\eta_\epsilon(L)$ of Micciancio and Regev (SIAM J. Comput. 2007): the Gaussian width above which a discrete Gaussian on a lattice behaves like a continuous one. The approximation factors of the reduction are stated in terms of $\eta_\epsilon(L)$, and they are converted into factors for the standard lattice problems (GapSVP, SIVP) by comparing $\eta_\epsilon(L)$ with the successive minima of $L$ and of its dual.

Upper bounds on $\eta_\epsilon(L)$ (Lemmas 2.11 and 2.12 of the paper, from Micciancio–Regev) say the smoothing parameter is not too large. Claim 2.13 is the matching lower bound: the smoothing parameter cannot be much smaller than $1/\lambda_1(L^*)$, and hence than $\lambda_n(L)/n$. The second comparison goes through Banaszczyk's transference theorem (Banaszczyk, Math. Ann. 296 (1993)), $1 \le \lambda_1(L)\lambda_n(L^*) \le n$, which relates the geometry of a lattice to that of its dual.

This mission formalizes Claim 2.13 from the published J. ACM article (Article 34, 2009), together with the steps of its proof and the transference theorem it cites. The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms; it is outside this series of missions.

Setting

Work in $\mathbb{R}^n$, $n \ge 1$, with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$. A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is

$$L^* = \{y \in \mathbb{R}^n : \langle x, y\rangle \in \mathbb{Z} \text{ for all } x \in L\},$$

again a lattice, with $(L^*)^* = L$.

The successive minima used here are $\lambda_1(L)$, the length of a shortest nonzero vector of $L$, and $\lambda_n(L)$, the least $r$ such that $L$ contains $n$ linearly independent vectors of length at most $r$.

For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$ (Eq. (4)), and for a countable set $A$, $\rho_s(A) = \sum_{x\in A}\rho_s(x)$. In particular $\rho_{1/s}(y) = \exp(-\pi s^2\|y\|^2)$.

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ such that $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

Formalization targets

Goal: Claim 2.13 (p. 34:20)

For any lattice $L$ and any $\epsilon > 0$,

$$\eta_\epsilon(L) \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{1}{\lambda_1(L^*)} \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{\lambda_n(L)}{n}.$$

Both inequalities of the chain are part of the goal. The asymptotic "In particular" sentence of the claim ($\epsilon(n) = o(1)$, large enough $n$) is not.

Milestones, in attack order

1. The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$, tends to $\infty$ as $s \to 0$ and to $0$ as $s \to \infty$, and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse; in particular $\rho_{1/\eta_\epsilon(L)}(L^*\setminus\{0\}) = \epsilon$.
2. The display of the proof of Claim 2.13 (p. 34:20). For $s = \eta_\epsilon(L)$ and $v \in L^*$ of length $\lambda_1(L^*)$,

$$\epsilon = \rho_{1/s}(L^*\setminus\{0\}) \ge \rho_{1/s}(v) = \exp\bigl(-\pi(s\lambda_1(L^*))^2\bigr).$$

3. Lemma 2.3, Banaszczyk's transference theorem (p. 34:18). For any $n$-dimensional lattice $L$,

$$1 \le \lambda_1(L)\cdot\lambda_n(L^*) \le n .$$

Significance

The result. Claim 2.13 shows that the smoothing parameter for a negligible $\epsilon$ exceeds every constant multiple of $1/\lambda_1(L^*)$ and of $\lambda_n(L)/n$. Together with the upper bound $\eta_\epsilon(L) \le \sqrt{\ln(2n(1+1/\epsilon))/\pi}\,\lambda_n(L)$ of Lemma 2.12, it locates $\eta_\epsilon(L)$ within a polynomial factor of $\lambda_n(L)$. This is what lets the reduction's guarantees, phrased in $\eta_\epsilon(L)$, be read as approximation factors for SIVP and GapSVP. The transference theorem is used throughout the geometry of numbers and in lattice-based cryptography to pass between a lattice and its dual.

Formalizing it. The claim and its proof are classical and short, but neither is machine-checked. The mission produces formal definitions of the dual lattice, the successive minima $\lambda_1$, $\lambda_n$ and the smoothing parameter on EuclideanSpace ℝ (Fin n), a proof that Definition 2.10 is well posed, and a statement of Banaszczyk's transference theorem. The upper bound of the transference theorem is a substantial result in its own right (the paper cites it without proof), and a formal proof of it would be reusable well beyond this mission.

Difficulty

The first inequality of the goal is elementary once the smoothing parameter is known to be attained, with $\rho_{1/\eta}(L^*\setminus\{0\}) = \epsilon$ exactly. That step is not a formality: it needs the continuity and strict monotonicity of an infinite lattice sum in the scale parameter, and the fact that a shortest nonzero dual vector exists, both of which rest on the discreteness of $L^*$.

The second inequality is a single line in the paper, "by Lemma 2.3", but it uses the upper bound of Banaszczyk's theorem, applied to the dual lattice. The easy lower bound $1 \le \lambda_1(L)\lambda_n(L^*)$ does not suffice, and a Minkowski-type argument gives a bound worse than linear in $n$. Applying the lemma to $L^*$ also needs $L^*$ to be a lattice with dual $L$.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n). A lattice is L : Submodule ℤ _ with [DiscreteTopology L] [IsZLattice ℝ L]. The dual is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
• Every theorem assumes $0 < n$: the paper's lattices are $n$-dimensional with $n \ge 1$. This is the only added hypothesis.
• Gaussian sums are real tsums. They are summable over discrete subgroups, so no summability hypotheses are added.
• $\eta_\epsilon(L)$, $\lambda_1$ and $\lambda_n$ are infima (sInf). The paper's "smallest" is the attainment proved in milestones 1 and 2, not built into the definition. $\lambda_1$ and $\lambda_n$ are defined for every $\mathbb{Z}$-submodule, so they apply to $L^*$ without extra instances.
• For $\epsilon \ge 1$ the paper's $\sqrt{\ln(1/\epsilon)/\pi}$ is the square root of a non-positive number; Lean's Real.sqrt gives $0$ there and the goal reduces to true statements. No hypothesis $\epsilon < 1$ is added, since the page says "any $\epsilon > 0$".
• The goal is a conjunction of both inequalities of the chain, not only the outer comparison $\eta_\epsilon(L) \ge \sqrt{\ln(1/\epsilon)/\pi}\,\lambda_n(L)/n$, which would be weaker. Lemma 2.3 states both bounds; stating only the easy lower bound would leave the goal's second inequality without its milestone.
• No printed statement needed correction.

Contributions welcome: the attainment of $\lambda_1$ and $\lambda_n$ for IsZLattice (and for the dual), the identity $(L^*)^* = L$ in this setting, continuity and monotonicity of Gaussian lattice sums, and above all Banaszczyk's transference theorem.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, J. ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• W. Banaszczyk, New bounds in some transference theorems in the geometry of numbers, Math. Ann. 296, 625–635, 1993. https://doi.org/10.1007/BF01445125
• D. Micciancio, O. Regev, Worst-case to average-case reductions based on Gaussian measures, SIAM J. Comput. 37(1), 267–302, 2007. https://doi.org/10.1137/S0097539705447360

Motivation

Nearest neighbor searching asks for a data structure that stores $n$ points $S\subset\mathbb R^d$ and, given a query point $q$, returns a point of $S$ closest to $q$. It underlies classification, vector quantization, data compression, pattern recognition and similarity search in databases. In dimension $d\ge 3$, exact methods either use space growing like $n^{\lceil d/2\rceil}$ or answer queries in time close to linear in $n$, so practical systems settle for an approximate answer: a point whose distance to $q$ is within a factor $1+\varepsilon$ of the true nearest distance.

Arya, Mount, Netanyahu, Silverman and Wu (J. ACM 45 (1998), 891–923) gave the first structure for this problem that is simultaneously of linear size, built in $O(dn\log n)$ time, and answers $(1+\varepsilon)$-approximate queries in $O(c_{d,\varepsilon}\log n)$ time for any fixed $d$, with $c_{d,\varepsilon}\le d\lceil 1+6d/\varepsilon\rceil^d$. The structure, the balanced box-decomposition tree (BBD-tree), and the priority search on it became the basis of the ANN library of Mount and Arya.

Timeline. Arya and Mount (SODA 1993) studied approximate nearest neighbor queries in fixed dimensions; the conference version of this paper (SODA 1994) gave an optimal algorithm; the journal version (1998), which the paper itself describes as differing from the conference version by a single balanced structure without auxiliary data structures (p. 897), is the one formalized here. Later work, for example by Har-Peled, Indyk and Motwani (2012), addressed the exponential dependence on $d$.

Setting

Points are vectors in $\mathbb R^d$. For an integer $m\ge1$ the $L_m$ distance is $\operatorname{dist}_m(x,y)=(\sum_i|x_i-y_i|^m)^{1/m}$, and for $m=\infty$ it is $\max_i|x_i-y_i|$. A rectangle is a product $\prod_i[\ell_i,h_i]$ of closed intervals; its size is the length of its longest side. A box is a rectangle with positive sides whose aspect ratio, longest over shortest side, is at most $3$.

A cell consists of an outer box $b_O$ and an optional inner box $b_I$; as a point set it is $b_O$, or the closure of $b_O\setminus b_I$. Its size is the size of $b_O$. The inner box must be sticky for the outer one: in every coordinate, each of the two gaps between the inner and the outer interval is either $0$ or at least the width of the inner interval.

A BBD-tree subdivides a root box by two operations. A fair split cuts a cell by a hyperplane $x_i=t$ into a low and a high child; a shrink cuts it by a shrinking box $b$ into an inner child (outer box $b$) and an outer child (outer box unchanged, inner box $b$). Throughout, every box has aspect ratio at most $3$, a parent's inner box lies entirely within one child (within the inner child of a shrink), and inner boxes are sticky. The cells at the leaves are the leaf cells; they cover the root box and have disjoint interiors.

The distance from $q$ to a cell $c$ is $\operatorname{dist}_m(q,c)=\inf_{x\in c}\operatorname{dist}_m(q,x)$. Each leaf cell $c_j$ carries an associated data point $p_j$ in its outer box. The search enumerates the leaf cells $c_0,c_1,\dots$ in nondecreasing order of distance from $q$, processes each by comparing its point with the closest point $p$ seen so far, and terminates at the first cell whose distance from $q$ exceeds $\operatorname{dist}_m(q,p)/(1+\varepsilon)$. The goal bounds $N$, the number of cells that did not cause termination, which is the count the paper's proof bounds ("the number of cells visited up until termination", p. 912).

Formalization targets

Goal: Lemma 5 (p. 911)

For every valid BBD-tree, every Minkowski metric $1\le m\le\infty$, every $\varepsilon>0$, every query point and every sorted enumeration of the leaf cells,

$$N\le\Big\lceil 1+\frac{6d}{\varepsilon}\Big\rceil^d.$$

Milestones

The packing constraint (Lemma 4, p. 908): for $r,s>0$, the number of leaf cells of size at least $s$ meeting an open $L_m$ ball of radius $r$ is at most

$$\Big\lceil 1+\frac{6r}{s}\Big\rceil^d.$$

Its proof has three stated steps, each a milestone: an $L_m$ ball of radius $r$ lies in an axis-parallel cube of side $2r$; at most $\lceil1+6r/s\rceil^d$ interior-disjoint boxes of side at least $s/3$ meet such a ball; and the leaf cells of size at least $s$ meeting the ball can be replaced by as many interior-disjoint boxes of size at least $s$ meeting it. The proof of Lemma 5 contributes two more: the $L_m$ diameter of a rectangle is at most $d$ (indeed $d^{1/m}$) times its longest side, and every visited cell has size at least $r\varepsilon/d$, where $r$ is the distance to the last cell that did not cause termination.

A companion statement records the correctness of the termination rule: the closest point processed is a $(1+\varepsilon)$-approximate nearest neighbor.

Significance

Lemma 5 is the explicit content of the query bound of Theorem 1(i): each visited cell costs $O(d\log n)$ time to enumerate and process, so the query takes $O(d\lceil1+6d/\varepsilon\rceil^d\log n)$ time, with no dependence on $n$ beyond the logarithm. Lemma 4 is the property of the subdivision on which this rests, and it is used again for the $k$-nearest-neighbor variant (Lemma 6) and for approximate range searching with the same tree.

The results are proved on paper and widely cited; none has a machine-checked proof. The mission produces checked versions of the packing constraint and of the cell-count bound for an abstract BBD-tree, defined by its invariants rather than by a particular construction algorithm, so that any construction meeting the invariants inherits the bound. It also exposes two places where the printed argument needs care: the open versus closed ball in Lemma 4, and the step in Lemma 5 that applies Lemma 4 to cells within distance $r$ of $q$, which touch the closed ball of radius $r$.

Difficulty

The counting step of Lemma 4 is asserted on the page ("the densest packing of axis-aligned rectangles of side length at least $s/3$ is realized by a regular grid"), and a formal argument must replace that sentence with a genuine counting argument. The replacement step is the geometric core: the outer box of a leaf cell with an inner box overlaps every leaf cell inside that inner box, so outer boxes cannot be counted directly, and without stickiness many nested inner boxes could crowd against one face of a cell. Applying Lemma 4 inside Lemma 5 is not immediate either: the visited cells lie within distance $r$ of $q$, so they meet the closed ball, while Lemma 4 concerns the open ball, and a naive enlargement of the radius changes the ceiling exactly when $6d/\varepsilon$ is an integer.

Formalization scope

Points are Fin d → ℝ, the metric index $m$ is an element of ℕ∞ with $1\le m$, and the $L_m$ distance is defined explicitly by the formula above. Rectangles are pairs of corner vectors; boxes have positive sides and aspect ratio at most $3$. A cell's point set is the closure of the outer box minus the inner box, as the paper's "cells are considered to be closed" requires; an inner box equal to its outer box is excluded. A BBD-tree is an inductive tree of splits and shrinks with a validity predicate expressing the §2.1 invariants relative to the root cell; the root may be any box rather than the paper's hypercube, and the construction algorithms of §2.2–§2.5 are not formalized.

The enumeration is a list of (leaf cell, associated point) pairs that is a permutation of the leaf cells, sorted by distance from $q$, with each point in its cell's outer box. A cell is processed before its own termination test, and $N$ counts the cells processed before the cell whose test fires (all cells if none fires). Lemma 4 and its counting step use the open ball of property (d). Theorem 1's $O(\cdot)$ time and space claims, Lemmas 1–3 on the construction, and the $k$-nearest-neighbor Lemma 6 are out of scope.

This convention follows the proof of Lemma 5, which takes $r$ to be the distance to "the last leaf cell that did not cause the algorithm to terminate" and bounds the cells up to that one. If the cell whose test fires is also counted, the printed bound can be exceeded by one: a valid one-dimensional tree with $\varepsilon=6$ needs three processed cells against $\lceil 1+6d/\varepsilon\rceil^d=2$. The formal goal therefore states the bound for the cells that did not cause termination, which is what the proof establishes; consequently at most $\lceil 1+6d/\varepsilon\rceil^d+1$ cells are processed in total.

The goal must not be trivialized: the enumeration must contain every leaf cell (an empty enumeration would give $N=0$), it must be sorted, cells must be closed sets rather than outer boxes minus open inner boxes (which leaves isolated boundary points and makes the goal false), and no size bound or packing fact may be assumed in the goal.

Contributions welcome: proofs of the milestones in any order, general lemmas on $L_m$ distances and interior-disjoint boxes (reusable beyond this mission), and a construction of valid BBD-trees from the paper's midpoint or middle-interval rules.

Selected references

• S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, J. ACM 45(6):891–923, 1998. https://doi.org/10.1145/293347.293348
• S. Arya, D. M. Mount, Approximate nearest neighbor queries in fixed dimensions, Proc. 4th ACM-SIAM SODA, 271–280, 1993 (reference [Arya and Mount 1993b] of the main paper, https://doi.org/10.1145/293347.293348).
• S. Arya, D. M. Mount, N. S. Netanyahu, R. Silverman, A. Y. Wu, An optimal algorithm for approximate nearest neighbor searching in fixed dimensions, Proc. 5th ACM-SIAM SODA, 573–582, 1994 (reference [Arya et al. 1994] of the main paper).
• D. M. Mount, S. Arya, ANN: A library for approximate nearest neighbor searching. https://www.cs.umd.edu/~mount/ANN/
• S. Har-Peled, P. Indyk, R. Motwani, Approximate nearest neighbor: towards removing the curse of dimensionality, Theory of Computing 8:321–350, 2012. https://doi.org/10.4086/toc.2012.v008a014

Motivation

In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.

The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor $3/2$. When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio $2n^{3/2}$.

Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on $K$. Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio $n$, but not by a polynomial algorithm for varying $n$; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.

Setting

Work in $\mathbb R^n$ with the Euclidean length $|\cdot|$, and write $B(p, \rho) = \{x \in \mathbb R^n : |x - p| \le \rho\}$ for the closed ball. For points $w_0, \dots, w_n \in \mathbb R^n$, the simplex volume is

$$\mathrm{vol}(w_0, \dots, w_n) = \frac{|\det M|}{n!},$$

where $M$ has column vectors $w_1 - w_0, \dots, w_n - w_0$.

Let $K \subseteq \mathbb R^n$ be convex, and let $v_0, \dots, v_n \in K$ with $v_1 - v_0, \dots, v_n - v_0$ linearly independent. Choose linear functions $g_0, \dots, g_n : \mathbb R^n \to \mathbb R$ with

$$g_i \text{ constant on } \{v_j : j \ne i\}, \qquad g_i(v_i) \ne g_i(v_j) \ (j \ne i). \tag{15}$$

Thus $g_i$ measures the height above the facet opposite $v_i$. The stopping condition of the second stage is

$$|g_i(x - v_j)| \le \tfrac32\, |g_i(v_i - v_j)| \quad \text{for all } x \in K \text{ and all } i \ne j. \tag{16}$$

The ratio $|g_i(x - v_j)|/|g_i(v_i - v_j)|$ is the factor by which the volume changes when $v_i$ is replaced by $x$, so (16) says that no such swap enlarges the simplex by more than $3/2$.

Let $\tau$ be a nonsingular linear map of $\mathbb R^n$ such that $z_j = \tau(v_j)$ span a regular simplex, meaning that all distances $|z_i - z_j|$, $i \ne j$, are equal. Let $p = (n+1)^{-1}\sum_j z_j$ be its centroid and $S$ its convex hull. For $c \ge 1$, the paper defines

$$T_c = \{x \in \mathbb R^n : \mathrm{vol}(z_0, \dots, z_{i-1}, x, z_{i+1}, \dots, z_n) \le c\cdot \mathrm{vol}(z_0, \dots, z_n) \text{ for all } i\}.$$

The proof of the LEMMA works in model coordinates. There $\mathbb R^n$ is the hyperplane $\sum_{j=0}^n r_j = 1$ of $\mathbb R^{n+1}$, the $z_j$ are the standard basis vectors, $p = (\tfrac1{n+1}, \dots, \tfrac1{n+1})$, and $T_c = \{r : |r_j| \le c \text{ for all } j,\ \sum_j r_j = 1\}$.

Formalization targets

Goal (§2, p. 543)

Under (15) and (16), with $\tau$ making the simplex regular and $p$ its centroid, there are positive reals $r, R$ with

$$B(p, r) \subseteq \tau K \subseteq B(p, R), \qquad \frac{R}{r} \le 2n^{3/2}.$$

These are conditions (3)–(4) of §1 with $c_1 = 2n^{3/2}$.

Milestones, in the order the proof uses them

1. (16) is a statement about $T_{3/2}$ (p. 543). Condition (16), for all $x \in K$ and $i \ne j$, holds exactly when $\tau K \subseteq T_{3/2}$.
2. Vertices of $T_c$ (pp. 543–544). In the model, $T_c$ is the convex hull of the coordinate permutations of $e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m$), or of $(1-c)e_0 - c\sum_{j=1}^m e_j + c\sum_{j=m+1}^n e_j$ ($n = 2m+1$).
3. Outer radius (p. 544). $T_c \subseteq B(p, R)$ with $R^2 = nc^2 + \tfrac{n}{n+1}$ ($n$ even) or $(n+1)c^2 - 2c + \tfrac{n}{n+1}$ ($n$ odd).
4. Inner radius (p. 544). $B(p, r) \subseteq S$ inside the hyperplane, with $r^2 = \tfrac{1}{n(n+1)}$.
5. LEMMA (p. 543). For $c \ge 1$ and any regular simplex, $B(p, r) \subseteq S \subseteq T_c \subseteq B(p, R)$ for positive $r, R$ with

$$\Big(\frac Rr\Big)^2 = \begin{cases} c^2n^3 + (c^2+1)n^2 & n \text{ even},\\ c^2n^3 + (2c^2 - 2c + 1)n^2 + (c^2 - 2c)n & n \text{ odd}.\end{cases}$$

The paper's own proof derives the goal from milestone 1 and the LEMMA at $c = 3/2$. At $n = 1$ the constant $2n^{3/2}$ cannot be improved by this argument.

Significance

The result. The theorem is the only place in the paper where the roundness constant $c_1$ is computed, and $c_1$ enters the bound $1 + c_1c_2\sqrt n$ on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of $c$ to obtain $c_1 = ((1+\epsilon)(n^3 + 2n^2))^{1/2}$ ($n$ even) and $((1+\epsilon)(n^3+n^2-n))^{1/2}$ ($n$ odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume-$c$ neighbourhood" $T_c$ of a regular simplex extends.

The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor $n$, by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.

Difficulty

There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map $\tau$. The second is the transfer to the model. The paper's "similarity transformation" identifies $\mathbb R^n$ with a hyperplane of $\mathbb R^{n+1}$ and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and $T_c$ must all be carried across this isometry up to scaling. The LEMMA is stated in $\mathbb R^n$, not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and the model $\mathbb R^{n+1}$ is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching $0, \dots, n$.
• The volume keeps the paper's normalisation $|\det M|/n!$. $T_c$ is defined from volumes exactly as on p. 543, not from barycentric coordinates.
• Readings of loose phrases. "Nonsingular endomorphism" is a linear equivalence. "Span a regular $n$-simplex" means all pairwise distances are equal and positive. "Certain/two positive real numbers $r, R$" is an existential with $0 < r$ and $0 < R$ in the conclusion; without them, $R/r$ with $r = 0$ would be $0$ in Lean. The LEMMA keeps the printed equality for $(R/r)^2$. (15) is two hypotheses on $g$, and (16) is quantified over all $x \in K$ and all pairs $i \ne j$.
• Generalizations, all harmless. The paper's $K$ is a bounded polyhedron and the $v_j$ are vertices; the claim is stated for any convex $K$ and any points $v_j \in K$, and boundedness of $K$ follows from (16). Milestone 1 holds for any set $K$. The LEMMA is stated for any regular simplex, since $\tau$ plays no role in it.
• $n \ge 1$ throughout. In the model, the ball of milestone 4 is intersected with the hyperplane $\sum_j x_j = 1$, the paper's $\mathbb R^n$. The full ball of $\mathbb R^{n+1}$ is not inside $S$.
• No trivializing formalization is possible: the hypotheses are satisfiable (checked at $n = 1$, $K = [0,1]$), the radii are positive, and the sets are computed from the data rather than assumed.
• Useful infrastructure, reusable beyond this mission: the volume of a simplex with one vertex replaced, as a multiple of a barycentric coordinate; existence and properties of regular simplices in $\mathbb R^n$; the isometric embedding of a regular simplex onto the standard simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• H. W. Lenstra, Jr., Integer programming with a fixed number of variables, Mathematics of Operations Research 8(4) (1983) 538–548. https://doi.org/10.1287/moor.8.4.538
• A. K. Lenstra, H. W. Lenstra, Jr., L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
• L. G. Khachiyan, A polynomial algorithm in linear programming, Soviet Math. Doklady 20 (1979) 191–194.
• R. Kannan, Minkowski's convex body theorem and integer programming, Mathematics of Operations Research 12(3) (1987) 415–440. https://doi.org/10.1287/moor.12.3.415
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

Whether the diameter of a polyhedron is bounded by a polynomial in its number of facets is one of the central open questions of convex geometry, and it bears directly on linear programming: the diameter of the graph of a polyhedron is a lower bound on the number of pivots of any simplex method that moves along edges. Write $\triangle_u(d,n)$ for the largest diameter of a $d$-dimensional polyhedron with $n$ facets. The best known bounds are

$$n - d + \lfloor d/5 \rfloor \;\le\; \triangle_u(d,n) \;\le\; n^{1+\log d},$$

due to Klee and Walkup (1967) and Kalai and Kleitman (1992), and the gap between them has stood for decades.

A recurring approach is to isolate a few purely combinatorial properties of polyhedra and to prove bounds for every object having them. Eisenbrand, Hähnle, Razborov and Rothvoß (2010) proposed a base abstraction defined by a single property, shared by all abstractions from which earlier bounds were derived. They showed that the known upper bounds survive in it, and, as their main result, that it admits almost-quadratic diameter. This mission formalizes that lower bound.

Timeline.

• 1967: Klee and Walkup, lower bound $n-d+\lfloor d/5\rfloor$ for unbounded polyhedra.
• 1970: Larman, $\triangle_u(d,n) \le 2^{d-1} n$ (linear in fixed dimension).
• 1974: Adler, Dantzig and Murty study abstract polytopes and their diameters.
• 1992: Kalai and Kleitman, the quasi-polynomial bound $n^{1+\log d}$.
• 2010: Eisenbrand, Hähnle, Razborov and Rothvoß, the base abstraction; both upper bounds hold in it, and its diameter is $\Omega(n^2/\log n)$ in dimension $n/4$.
• 2012: Santos disproves the Hirsch conjecture for polytopes; the polynomial question remains open.

Setting

Let $[n] = \{1,\dots,n\}$ and let $\binom{[n]}{d}$ be the family of its $d$-element subsets. Consider a graph $G$ whose vertex set $V$ is a nonempty subfamily of $\binom{[n]}{d}$. The graph satisfies condition i) if

for each $u, v \in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u \cap v$.

The base abstraction $\mathcal B_{d,n}$ is the class of all such graphs; $d$ is called the dimension and $n$ the number of facets. Write $\mathrm{dist}_G(u,v)$ for the length of a shortest $u$–$v$ path, and

$$D(d,n) = \max\{\mathrm{dist}_G(u,v) : G \in \mathcal B_{d,n},\ u, v \in V(G)\}.$$

The geometry behind the definition: in a non-degenerate polyhedron every vertex lies on exactly $d$ facets, so labelling vertices by their facets gives distinct $d$-subsets of $[n]$; and two vertices can be joined without leaving the smallest face containing both, i.e. through vertices lying on every facet common to $u$ and $v$. Hence $\triangle_u(d,n) \le D(d,n)$ (the subject of a separate mission of this series).

In the Lean development, EHRR10.LowerBound.CondI V G is condition i), and EHRR10.LowerBound.InB d n V G says that $V$ is nonempty, all its members have $d$ elements, and condition i) holds.

Formalization targets

Goal: almost-quadratic diameter in dimension $n/4$

$$D(n/4,\, n) = \Omega\!\left(\frac{n^2}{\log n}\right).$$

Explicitly, there are $c > 0$ and $N$ such that for every $n \ge N$ with $4 \mid n$ there is a graph $G \in \mathcal B_{n/4,\,n}$ and two vertices $u, v$ of $G$ with $\mathrm{dist}_G(u,v) \ge c\, n^2/\log n$. The constants $c$ and $N$ are left unfixed, so the goal survives any improvement in the constant.

There are no milestones: the source is an extended abstract that states the result without a proof and names no intermediate lemma.

Significance

The result. Since $\triangle_u(d,n) \le D(d,n)$, any proof of a bound on $D$ bounds the diameter of all non-degenerate polyhedra. The paper shows that the Kalai–Kleitman and Larman bounds are of this kind. The lower bound shows the limits of the approach: an argument that uses only condition i) cannot prove a linear (Hirsch-type) bound, because $D(n/4,n)$ grows almost quadratically in $n$. Any proof of a linear bound must use further geometric properties of polyhedra. A polynomial, even quadratic, upper bound for $D$ is not excluded by the result.

Formalizing it. The result is proved in the literature (Math. Oper. Res. 35 (2010) 786–794); it has no machine-checked proof. A formal proof requires an explicit combinatorial construction of graphs in the base abstraction with large diameter and a probabilistic existence argument, neither of which is currently on the platform. The platform's Hirsch campaign has the same abstraction in its layer-family form (Hirsch_clf, whose description mentions the $\Omega(n^2/\log n)$ families in prose) and the proved upper bound Hirsch.clf_saturated_quadratic_bound, $L \le d(n-d)$, on a subclass that contains the constructions of this paper; neither states the lower bound.

Difficulty

A long path through all of $\binom{[n]}{d}$ has exponential length but violates condition i): two vertices of the path generally share elements that some intermediate vertex lacks. Condition i) must hold for every pair of vertices simultaneously, which forces the vertices containing any fixed set to induce a connected subgraph. Building a long graph means arranging many $d$-sets so that each of these exponentially many connectivity constraints holds at once while the graph distance between two vertices stays large. The authors announce that their construction relies on disjoint covering designs, and that the existence of such designs with the required parameters is obtained from the Lovász Local Lemma.

Formalization scope

• $[n]$ is Fin n; vertices are the $d$-sets themselves, V : Finset (Finset (Fin n)) and G : SimpleGraph V. Distinct vertices carry distinct labels.
• Condition i) is stated with walks, and requires every vertex of the walk (endpoints included, which is automatic) to contain $u \cap v$. A walk contains a path on a subset of its vertices, so this is the page's condition.
• "Connected" is encoded as $V \ne \emptyset$; connectivity follows from condition i).
• The page writes $D(n/4,n)$ without rounding; the goal is read literally: $4 \mid n$ and dimension exactly $n/4$.
• $\Omega(\cdot)$ is made explicit as $\exists c > 0, \exists N, \forall n \ge N$. The logarithm is natural (Real.log); the base only rescales $c$.
• "$D(n/4,n) \ge B$" is stated as the existence of one graph in the class with two vertices at SimpleGraph.dist at least $B$; $D$ is not defined as a supremum, so no junk value enters. SimpleGraph.dist returns $0$ for unreachable pairs, which could only make the statement harder.
• Only the lower half of $\Omega$ is claimed, as on the page.

The goal cannot be trivialized by a non-injective labelling (vertices are the sets), by checking condition i) only on adjacent pairs (it is required for all pairs, with $u\cap v$ kept along the whole walk), or by a zero constant ($c > 0$ is required).

Infrastructure that a solution needs and that is reusable beyond this mission: covering designs and disjoint covering designs over Finset (Fin n), the Lovász Local Lemma (posed on the platform as AppliedComb.ManyFaces.local_lemma_symmetric), and a toolkit for proving condition i) for graphs assembled from blocks. Contributions of any of these as separate theorems are welcome.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010 (the extended abstract this mission cites). http://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010 (full proofs). https://doi.org/10.1287/moor.1100.0470
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26(2), 315–316, 1992. https://doi.org/10.1090/S0273-0979-1992-00285-9
• D. G. Larman, Paths on polytopes, Proc. London Math. Soc. 20(3), 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161
• V. Klee, D. W. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117, 53–78, 1967. https://doi.org/10.1007/BF02395040
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176(1), 383–412, 2012. https://doi.org/10.4007/annals.2012.176.1.7
• N. Alon, J. Spencer, The Probabilistic Method, 3rd ed., Wiley, 2008 (Lovász Local Lemma).

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$, which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

• 1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
• 1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$.
• 1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
• 1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
• Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$, where $1\le k\le\min(m,n)$, keeps $k$ rows and $k$ columns of $A$. The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$. So $\Delta(0)=0$, and $\Delta(A)\ge 1$ whenever $A\ne 0$. Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$.

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$. An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$. For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$. A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$, $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$.

If $ay\le\beta$ for all $y\in P$, with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$. The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$. Then $P_I\subseteq P^{(i)}$ for all $i$. The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$. The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$.

Formalization targets

Goal: Theorem 10 (p. 260)

$$\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.$$

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$.

Milestones, in attack order

1. Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$-distance $n\Delta(A)$, and every IP optimum has an LP optimum within the same distance.
2. Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$.
3. Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$. This result is off the goal's path.
4. Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$-distance $n\Delta(A)$.
5. Theorem 7 (p. 257). A single integral matrix $M$, with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
6. Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$.
7. Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$.

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$. They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$: polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$. That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$. Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$, and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

• Rationality. Everything is over $\mathbb{Q}$, following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$, and a polyhedron is a finite system of rational inequalities.
• $\Delta(A)$. Only nonempty submatrices count, so $\Delta(0)=0$.
• Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
• Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$, using all integral $a$ and rational $\beta$. The rank is valued in $\mathbb{N}\cup\{\infty\}$, with $\infty$ if no iterate equals $P_I$. A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$, as printed.
• Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$. For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
• Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$.

A complete development needs the following:

• cone generation with Cramer bounds and Carathéodory's theorem;
• LP duality and Farkas' lemma over $\mathbb{Q}$;
• the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
• Schrijver's face lemma and unimodular invariance;
• a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

• W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
• V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
• A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
• W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
• F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322