Discrete Geometry

Motivation

A continuously varying family of line segments suggests a low-cost cylinder cover, but a finite approximation must control both gaps and accumulated base area. The source manuscript presents the surrounding research claim.

Setting

A ruled set consists of segments (s,p+sv(p)) with p in a compact planar label set D and |s|≤L. The basic weighted projection cost is ∫_D(1+|v(p)|²)^(-1/2)dp. The source also defines physical rescalings, square intercept tiles and singular slope fields.

Formalization target

Prove the published FullMain conjunction. Its central finite-approximation clause gives

$$\sum_i |B_i|\le\int_D\frac{dp}{\sqrt{1+|v(p)|^2}}+\varepsilon$$

for every ε>0 under its C¹ hyperbolicity hypotheses. The package additionally contains physical-rescaling, logarithmic, product-cell, orthogonal-grid, smooth nilpotent and singular-tetrahedron assertions.

The selected formal target is OAI.RuledApproximation.fullMain.

Significance and status

The chosen goal supplies a package of finite-cover results with explicit regularity and base-shape requirements. The broad fourPaperMain reference also contains a C¹ nilpotent variant. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Freezing directions can create gaps and a persistent area loss. The final family must be finite and cover every point while the area error is arbitrarily small.

Formalization scope

FullMain uses Euclidean planes and three-space. Some clauses require null-measure boundary or C² regularity; its NilpotentStatement requires smoothness and a square-zero derivative. The singular clause includes its stated p,γ ranges and strict tetrahedron cost below √2/2. These are the selected published clauses; the manuscript’s latest C¹ formulation is not silently substituted for them. Independent definition groups remain separate references.

Selected references

• OpenAI, Finite cylinder approximation of ruled sets, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Cylinder covers measure coverage cost by perpendicular base area. For a regular tetrahedron, the familiar half-minimum-shadow threshold is tested by a finite family of tilted triangular cylinders. The source manuscript presents the surrounding research claim.

Setting

The reference tetrahedron K has coordinates (x,y,√2t) with 0≤t≤1, |x|≤1−t and |y|≤t. Let H=√2 and A_min be its least unit-direction projection area. A triangular cylinder has a compact nondegenerate triangle in the plane perpendicular to its unit axis.

Formalization target

Prove A_min=H and construct, for every sufficiently small ε>0, 2⌈2/ε²⌉ cylinders covering K with

$$\frac{\sum_i|B_i|}{H}=\frac12-\frac{13}{6000}\varepsilon^2+O(\varepsilon^4),\qquad\sum_i|B_i|<\frac{A_{\min}}2.$$

Also prove existence of a finite cover with Σᵢ|Bᵢ|/shadowArea(uᵢ)<1/2.

The selected formal target is OAI.TriangularCovering.main.

Significance and status

The asymptotic estimate retains its explicit quadratic coefficient and uniform fourth-order error. Both absolute area and directionwise normalized cost are formal conclusions. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Tilting may reduce projected area but leave uncovered gaps. The target requires exact finite coverage and valid triangular bases together with the strict cost saving.

Formalization scope

Base area is two-dimensional Euclidean Hausdorff measure converted to ℝ. MainAsymptotic has fixed positive δ,C before all small ε. The broad fourPaperMain is retained as a related published reference; the selected goal remains TriangularCovering.main. Repeated definitions in independent source groups are kept separate.

Selected references

• OpenAI, Finite angular cylinder covers below the half-area bound, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Erdős's distinct-distance problems ask how few different distances $n$ points in the plane can determine. The global version, which counts all distances between all pairs, was essentially settled by Guth and Katz, who proved that every $n$-point planar set determines at least $cn/\log n$ distinct distances (Annals 2015), matching the square lattice up to a $\sqrt{\log n}$ factor. The pinned version asks for many distances measured from a single point: given $P$, is there a pin $x\in P$ from which almost $n$ distinct distances are visible? The weak pinned Erdős conjecture asserts that for every $\varepsilon>0$ some pin sees at least $n^{1-\varepsilon}$ distinct distances. Erdős stated the question in 1957 (Michigan Math. J. 1957, Problem 16). Pinned bounds are a standard test for incidence-geometric methods, since Guth–Katz controls only the union of distances over all pins.

This mission formalizes the main theorem of an OpenAI preprint dated September 23, 2026 (source), which claims that large repeated-distance fibres are rare at almost every pin and deduces the weak pinned conjecture. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open (stated, not yet proved).

Background

• 1946 — Erdős introduces the distinct-distance problem and the $\sqrt{\log n}$ lattice example (Amer. Math. Monthly 1946).
• 1957 — Erdős asks the pinned question (Michigan Math. J. 1957).
• 2001 — Solymosi and Tóth prove a pinned lower bound of order $n^{6/7}$ (DCG 2001).
• 2003–2004 — Tardos improves the exponent with entropy inequalities (Adv. Math. 2003); Katz and Tardos reach every exponent below $\frac{48-14e}{55-16e}=0.8641\ldots$ (Contemp. Math. 342, 2004).
• 2015 — Guth and Katz prove the global bound $cn/\log n$ (Annals 2015).
• September 2026 — The OpenAI preprint claims the weak pinned conjecture (Theorem 1.1 and Corollary 1.2, p. 2).

Setting

Let $P\subset\mathbb R^2$ be a finite set with $|P|=n\ge2$. For distinct $x,y\in P$, the distance fibre size is

$$k_P(x,y)=\#\{z\in P\setminus\{x\}:\ \|z-x\|=\|y-x\|\},$$

the number of points of $P$ at the same distance from the pin $x$ as $y$ (it counts $y$ itself). Each pair uses its own pin; pairs sharing a numerical distance but with different pins are not pooled. For $s>0$ define

$$F_n(s)=\sup_{P\subset\mathbb R^2,\ |P|=n}\ \frac{\#\{(x,y)\in P^2:\ x\ne y,\ k_P(x,y)\ge n^s\}}{n(n-1)},$$

the largest possible fraction of ordered distinct pairs that lie in a distance fibre of size at least $n^s$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every fixed $s>0$,

$$F_n(s)\longrightarrow0\qquad(n\to\infty).$$

The convergence is uniform over all configurations; no separation, general-position or coordinate hypothesis is imposed, and no rate is claimed.

Significance

The result itself. Corollary 1.2 (p. 2) follows in a few lines: for every $\varepsilon>0$, the fraction of pins $x\in P$ with fewer than $n^{1-\varepsilon}$ distinct distances tends to $0$ uniformly in $P$, so all but $o(n)$ points see at least $n^{1-\varepsilon}$ distances. This settles the weak pinned conjecture, improving the previous best exponent $0.8641\ldots$ to $1-\varepsilon$. An exceptional set is unavoidable: the centre of a circle carrying the other points sees one distance. The sharper conjecture of order $n/\sqrt{\log n}$ at a pin is not addressed.

Formalizing it. The proof combines transfer for real closed fields (to move a configuration into a number field), the product formula over all places of a number field, random nested grids, and weak compactness of probability measures. A formal proof would exercise Mathlib's number-field and measure-theory libraries in combination, and the statement itself is elementary enough to audit easily. No machine-checked pinned-distance bound is known.

Difficulty

Incidence bounds (Szemerédi–Trotter type) and entropy inequalities give pinned exponents strictly below $1$, and the obstruction is structural: they count incidences globally, while the pinned problem needs control at individual pins. The preprint (pp. 3–4) proceeds by contradiction and uses that squared distance factors as $(Z_1(y)-Z_1(x))(Z_2(y)-Z_2(x))$ with $Z_{1,2}=u\pm iv$, so on a fibre one coordinate is a fractional linear function of the other. Turning the product formula into usable information requires an exact additive overlap identity for nested partitions at every absolute value (Section 3), with the field and its degree unbounded along the sequence, and then a limiting argument that rules out non-atomic fibre maps (Lemma 7.1, p. 25).

Formalization scope

• Points are in EuclideanSpace ℝ (Fin 2); configurations are Finsets. k P x y counts (P.erase x).filter (dist z x = dist y x).
• richPairs P s is the set of ordered pairs $(x,y)\in P\times P$ with $x\ne y$ and $n^s\le k_P(x,y)$; pairFraction divides by $n(n-1)$ as a real.
• F n s is the sSup over all $n$-point sets of pairFraction for $n\ge2$ and is defined as 0 for $n<2$. For $n\ge2$ the set of values is nonempty and contained in $[0,1]$, so sSup is the true supremum.
• The goal is Tendsto (fun n => F n s) atTop (𝓝 0) for each fixed s > 0; it is not vacuous, since $F_n(s)$ is a genuine supremum over all configurations.
• Corollary 1.2 (the counting statement about pins) is not part of the goal; it is an elementary consequence.

Selected references

• OpenAI, The weak pinned planar distance theorem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-weak-pinned-planar-distance-theorem-September-23-2026/paper.pdf
• P. Erdős, On sets of distances of n points, Amer. Math. Monthly 53 (1946), 248–250. https://doi.org/10.1080/00029890.1946.11991674
• P. Erdős, Some unsolved problems, Michigan Math. J. 4 (1957), 291–300. https://doi.org/10.1307/mmj/1028997963
• J. Solymosi, C. D. Tóth, Distinct distances in the plane, Discrete Comput. Geom. 25 (2001), 629–634. https://doi.org/10.1007/s00454-001-0009-z
• G. Tardos, On distinct sums and distinct distances, Adv. Math. 180 (2003), 275–289. https://doi.org/10.1016/S0001-8708(03)00004-5
• N. H. Katz, G. Tardos, A new entropy inequality for the Erdős distance problem, Contemp. Math. 342 (2004). https://doi.org/10.1090/conm/342/06136
• L. Guth, N. H. Katz, On the Erdős distinct distances problem in the plane, Ann. of Math. 181 (2015), 155–190. https://doi.org/10.4007/annals.2015.181.1.2
• B. Lund, G. Petridis, Bisectors and pinned distances, Discrete Comput. Geom. 64 (2020), 995–1012. https://doi.org/10.1007/s00454-019-00122-w

Motivation

Sparsest cut asks for a partition of a weighted graph whose crossing capacity is small compared with the demand it separates. It is a basic graph-partitioning primitive (used for divide-and-conquer algorithms, clustering and expansion testing), and its relaxations are the main bridge between approximation algorithms and the geometry of finite metric spaces. In the uniform version every pair of vertices has demand one. The best known polynomial-time approximation, due to Arora, Rao and Vazirani, uses the Goemans–Linial semidefinite relaxation and achieves ratio $O(\sqrt{\log n})$. How good this relaxation can be, i.e. its integrality gap on uniform instances, has been a long-standing question.

Timeline

• 1995. Linial, London and Rabinovich develop the metric approach to cuts: $\ell_1$ metrics are combinations of cut metrics, so embeddings into $\ell_1$ round to cuts (doi:10.1007/BF01200757).
• 1997 and 2002. Goemans and Linial propose the semidefinite relaxation with triangle inequalities and the conjecture that negative-type metrics embed into $\ell_1$ with constant distortion (doi:10.1007/BF02614315).
• 2003 and 2008. Rabinovich relates uniform sparsest cut to average distortion of embeddings into the line and into $L_1$ (doi:10.1145/780542.780609, doi:10.1007/s00454-007-9047-5).
• 2004/2009. Arora, Rao and Vazirani prove the $O(\sqrt{\log n})$ upper bound for uniform demands (doi:10.1145/1502793.1502794).
• 2005/2015. Khot and Vishnoi disprove the Goemans–Linial conjecture for general demands (doi:10.1145/2629614).
• 2006. Devanur, Khot, Saket and Vishnoi give an $\Omega(\log\log n)$ uniform integrality gap (doi:10.1145/1132516.1132594). Lee and Naor propose the Heisenberg-group approach for general demands (doi:10.1109/FOCS.2006.47).
• 2009–2011. Cheeger, Kleiner and Naor prove a $(\log n)^{\Omega(1)}$ general-demand gap (arXiv:0910.2024) and note that their examples cannot give a diverging uniform gap.
• 2013. Kane and Meka improve the uniform gap to $\exp(\Omega(\sqrt{\log\log n}))$ (doi:10.1145/2488608.2488610).
• 2018 and 2025. Naor and Young obtain the sharp general-demand lower bound $\Omega(\sqrt{\log n})$ (doi:10.4007/annals.2018.188.1.4); Chang, Naor and Ren prove the matching upper bound (doi:10.1145/3717823.3718285).

For uniform demands the gap between the lower bound $\exp(\Omega(\sqrt{\log\log n}))$ and the upper bound $O(\sqrt{\log n})$ remained. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a lower bound matching the upper bound up to a power of $\log\log n$.

Setting

Let $C=(c_{ij})$ be symmetric nonnegative capacities on pairs of distinct vertices of $[n]$. The uniform sparsest-cut value is

$$\mathrm{OPT}(C)=\min_{\varnothing\ne B\subsetneq[n]}\frac{\sum_{i\in B,\,j\notin B}c_{ij}}{|B|\,(n-|B|)}.$$

A negative-type semimetric is $d(i,j)=\|x_i-x_j\|^2$ for vectors $x_i$ in a real Hilbert space, satisfying all triangle inequalities $d(i,k)\le d(i,j)+d(j,k)$; distinct points may have distance zero. The Goemans–Linial value is

$$\mathrm{GL}(C)=\min\Bigl\{\sum_{i<j}c_{ij}\,d(i,j)\ :\ \sum_{i<j}d(i,j)=1,\ d\ \text{negative type}\Bigr\}.$$

Normalized cut metrics are feasible, so $\mathrm{GL}(C)\le\mathrm{OPT}(C)$. The integrality gap of $C$ is $\mathrm{OPT}(C)/\mathrm{GL}(C)$.

Formalization targets

Goal: Theorem 1.1

There are an absolute $c>0$ and instances $C^{(j)}$ on $n_j\to\infty$ vertices with $\mathrm{GL}(C^{(j)})>0$ such that, for all large $j$,

$$\frac{\mathrm{OPT}(C^{(j)})}{\mathrm{GL}(C^{(j)})}\ \ge\ c\,\frac{\sqrt{\log n_j}}{(\log\log n_j)^3}.$$

The Lean statement OAI.UniformSparsestCut.mainGap is open on the platform.

Significance

The bound reaches the exponent $1/2$ in $\log n$, so the Arora–Rao–Vazirani analysis of the Goemans–Linial SDP is tight for uniform demands up to the factor $(\log\log n)^3$. It strengthens the Devanur–Khot–Saket–Vishnoi and Kane–Meka refutations of the uniform constant-gap conjecture. Geometrically, it gives a finite negative-type metric for which every $1$-Lipschitz map into $\ell_1$ preserves only a $(\log\log n)^3/\sqrt{\log n}$ fraction of the average distance. The theorem concerns the basic Goemans–Linial SDP only, not strengthened hierarchies.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.

Difficulty

The sharp general-demand lower bounds (Heisenberg group, Naor–Young) control worst-pair distortion, and Cheeger–Kleiner–Naor note that those examples have constant average distortion into a line, so they cannot give a diverging uniform gap. A uniform-demand example must force every $\ell_1$ contraction to lose most of the average distance over all pairs, not merely on a few pairs. At the same time the constructed distance must remain of negative type and satisfy all triangle inequalities exactly, and the passage from a probability measure on points to an exactly uniform demand with positive SDP value must be carried out without losing the bound.

Formalization scope

• Capacity n stores cap : Fin n → Fin n → ℝ, nonnegative, symmetric, zero on the diagonal.
• cutRatio C B is the crossing capacity of $B$ divided by $|B|(n-|B|)$; OPT C is the sInf over nonempty proper Finsets $B$.
• NegativeType d requires points x : Fin n → EuclideanSpace ℝ (Fin n) with $d=\|x_i-x_j\|^2$ and all triangle inequalities; Feasible d adds $\sum_{i<j}d(i,j)=1$; glValue C is the sInf of $\sum_{i<j}c_{ij}d(i,j)$ over feasible $d$.
• The goal asks for a sequence $n_j\ge2$, $n_j\to\infty$, with $\mathrm{GL}>0$ for every $j$ (ruling out a gap that is trivial because of division by zero) and the bound eventually.

A complete development needs cut-cone duality, a Hilbert-space kernel construction with rounded charts, Gaussian direction families, and contraction estimates for maps into $\ell_1$. Cut-cone duality and the reduction to exactly uniform demands are reusable. Contributions formalizing Lemma 6.1 (cut-cone duality) or the weak duality $\mathrm{GL}\le\mathrm{OPT}$ are welcome first steps.

Selected references

• OpenAI, Near-square-root logarithmic integrality gaps for uniform sparsest cut, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026.pdf
• S. Arora, S. Rao, U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM, 2009. https://doi.org/10.1145/1502793.1502794
• N. R. Devanur, S. A. Khot, R. Saket, N. K. Vishnoi, Integrality gaps for sparsest cut and minimum linear arrangement problems, STOC 2006. https://doi.org/10.1145/1132516.1132594
• D. M. Kane, R. Meka, A PRG for Lipschitz functions of polynomials with applications to sparsest cut, STOC 2013. https://doi.org/10.1145/2488608.2488610
• S. A. Khot, N. K. Vishnoi, The Unique Games Conjecture, integrality gap for cut problems and embeddability of negative type metrics into $\ell_1$, J. ACM, 2015. https://doi.org/10.1145/2629614
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica, 1995. https://doi.org/10.1007/BF01200757
• Y. Rabinovich, On average distortion of embedding metrics into the line, Discrete Comput. Geom., 2008. https://doi.org/10.1007/s00454-007-9047-5
• J. Cheeger, B. Kleiner, A. Naor, A $(\log n)^{\Omega(1)}$ integrality gap for the Sparsest Cut SDP, FOCS 2009. https://arxiv.org/abs/0910.2024
• A. Naor, R. Young, Vertical perimeter versus horizontal perimeter, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.188.1.4

Motivation

A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some $\mathbb R^k$. Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.

Timeline

• 1983. Assouad proves that every doubling metric space embeds bi-Lipschitzly into some $\mathbb R^k$ after snowflaking, i.e. after replacing the distance $d$ by $d^\alpha$ with $0<\alpha<1$ (doi:10.24033/bsmf.1997).
• 2001. Lang and Plaut ask whether every doubling subset of Hilbert space admits a bi-Lipschitz embedding into a finite-dimensional Euclidean space (Question 2.4) (doi:10.1023/A:1012093209450).
• 2003. Gupta, Krauthgamer and Lee independently pose the question for algorithmic dimension reduction (doi:10.1109/SFCS.2003.1238226).
• 2012. Naor and Neiman bound the target dimension in Assouad's theorem independently of the snowflake exponent near $1$ (doi:10.4171/RMI/706).
• 2014. Lafforgue and Naor construct, for $p>2$, a doubling subset of $L_p$ with no bi-Lipschitz embedding into any $\mathbb R^k$ (doi:10.1007/s10711-013-9924-4).
• 2015. Bartal, Gottlieb and Neiman obtain obstructions for doubling subsets of $\ell_p$ via Laakso-type configurations (doi:10.1137/140977655); Gottlieb and Krauthgamer embed snowflakes of finite Hilbert subsets with distortion close to one (doi:10.1007/s00454-015-9707-9).
• 2017. Schioppa announces a negative answer for $\ell_2$ and later withdraws the preprint (arXiv:1703.10265).
• 2021. Baudier, Świȩcicki and Swift give an elementary proof of the fixed-set theorem for $\ell_q$, $q>2$ (doi:10.1016/j.jmaa.2021.125407).

The Hilbert case ($p=2$) remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.

Setting

A metric space $(X,d)$ is doubling with constant at most $\lambda$ if for every $x\in X$ and $r>0$, the ball of radius $r$ about $x$ is covered by at most $\lambda$ balls of radius $r/2$ with centers in $X$. A map $f:X\to\mathbb R^k$ is a bi-Lipschitz embedding with distortion at most $D$ if some scale $a>0$ satisfies

$$a\,d(x,y)\ \le\ \|f(x)-f(y)\|\ \le\ D\,a\,d(x,y)\qquad(x,y\in X).$$

Real $\ell_2$ is the Hilbert space of square-summable real sequences indexed by $\mathbb N$; subsets carry the induced distance.

Formalization targets

Corollary 6 (milestone)

There is a universal $\Lambda$ such that every infinite-dimensional real Banach space $B$ contains a compact set $K_B$ with doubling constant at most $\Lambda$ that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.

Goal: Theorem 1

$$\exists\, S\subset\ell_2:\quad S\ \text{is doubling with constant}\ \le 76800,\ \text{and}\ \forall k\ge1,\ S\ \text{admits no bi-Lipschitz embedding into}\ \mathbb R^k.$$

The set is fixed once, independently of $k$ and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant $76800=300\cdot16^2$ comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.

Significance

The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from $p>2$ to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every $L_p[0,1]$, $1\le p<\infty$ (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.

Difficulty

Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The $p>2$ constructions rely on uniform convexity estimates of $L_p$ that degenerate at $p=2$, and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every $k$ and every $D$ simultaneously.

Formalization scope

• The ambient space is RealL2 := lp (fun _ : ℕ => ℝ) 2; $S$ is a Set RealL2 with the subspace metric.
• DoublingAtMost S bound: for each $x\in S$ and $r>0$ there is a Finset of at most bound centers in $S$ such that every $y\in S$ with $d(y,x)<r$ satisfies $d(y,c)<r/2$ for some center (open balls; centers in $S$).
• AdmitsBiLipschitzEmbedding S k: there are $f:S\to$ EuclideanSpace ℝ (Fin k), $a>0$ and $D\ge1$ with the two-sided bound above.
• For Corollary 6, CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant $\Lambda$ chosen before $B$.

A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of $\mathbb R^2$ (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.

Selected references

• OpenAI, A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf
• U. Lang, C. Plaut, Bilipschitz embeddings of metric spaces into space forms, Geom. Dedicata, 2001. https://doi.org/10.1023/A:1012093209450
• P. Assouad, Plongements lipschitziens dans $\mathbb R^n$, Bull. Soc. Math. France, 1983. https://doi.org/10.24033/bsmf.1997
• A. Gupta, R. Krauthgamer, J. R. Lee, Bounded geometries, fractals, and low-distortion embeddings, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238226
• A. Naor, O. Neiman, Assouad's theorem with dimension independent of the snowflaking, Rev. Mat. Iberoam., 2012. https://doi.org/10.4171/RMI/706
• V. Lafforgue, A. Naor, A doubling subset of $L_p$ for $p>2$ that is inherently infinite dimensional, Geom. Dedicata, 2014. https://doi.org/10.1007/s10711-013-9924-4
• Y. Bartal, L.-A. Gottlieb, O. Neiman, On the impossibility of dimension reduction for doubling subsets of $\ell_p$, SIAM J. Discrete Math., 2015. https://doi.org/10.1137/140977655
• F. P. Baudier, K. Świȩcicki, A. Swift, No dimension reduction for doubling subsets of $\ell_q$ when $q>2$ revisited, J. Math. Anal. Appl., 2021. https://doi.org/10.1016/j.jmaa.2021.125407

Motivation

The Johnson–Lindenstrauss lemma (1984) says that any $n$ points of a Hilbert space can be placed in $O_D(\log n)$-dimensional Euclidean space with distortion at most any prescribed $D>1$. This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces $L_p$ with $p\ne2$ the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space $\ell_p^d$ with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates $d$ are needed so that every $n$-point subset of $L_p$ embeds into $\ell_p^d$ with distortion at most $D$?

Timeline

• 1958. Lamperti characterizes equality in the $p$-parallelogram inequality, the tool behind exact-embedding lower bounds (doi:10.2140/pjm.1958.8.459).
• 1984. Johnson and Lindenstrauss prove the Hilbert-space lemma and ask for analogues in other spaces (doi:10.1090/conm/026/737400).
• 1987 and 2011. Schechtman's finite-set estimates for $p<2$ improve from $O_D(n\log n)$ coordinates to $O_{p,D}(n)$ (numdam, arXiv:1110.2148).
• 1989 and 1995. Bourgain–Lindenstrauss–Milman and Talagrand discretize whole $r$-dimensional subspaces of $L_p$ by linear maps (doi:10.1007/BF02392835, doi:10.1007/978-3-0348-9090-8_26); applied to $n$ points this gives dimension polynomial in $n$.
• 1990. Ball proves that exact embeddings need at most $\binom n2$ coordinates and that quadratic order is necessary for $1\le p<2$ (doi:10.1016/S0195-6698(13)80131-X).
• 2004–2005. Brinkman–Charikar and Lee–Naor show that dimension reduction fails in $\ell_1$ even for nonlinear maps (doi:10.1145/1089023.1089026, doi:10.1007/s00039-004-0473-8); Lee–Mendel–Naor show that linear maps can require dimension linear in $n$ when $p\ne2$ (doi:10.1016/j.ejc.2004.07.002).
• 2018. Naor surveys metric dimension reduction and the coordinate-target question (arXiv:1809.02376).
• 2026. Naor and Ren show that for $p>2$ the dimension cannot be $O_{p,D}(\log n)$ (arXiv:2609.01079).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed $1<p<\infty$, $p\ne2$, and $D>1$ the dimension is $n^{o(1)}$.

Setting

All spaces are real. Fix $1<p<\infty$, an integer $n\ge2$ and $D\ge1$. Let $d_p(n,D)$ be the least integer $d$ such that for every measure space and every $n$ distinct points $x_1,\dots,x_n\in L_p$ there are $y_1,\dots,y_n\in\mathbb R^d$ and a scale $s>0$ with

$$s\,\|x_i-x_j\|_p\ \le\ \|y_i-y_j\|_{\ell_p^d}\ \le\ D\,s\,\|x_i-x_j\|_p\qquad(1\le i,j\le n).$$

The map $x_i\mapsto y_i$ is arbitrary, not required to be linear. Put

$$\gamma(p)=\begin{cases}2-p,&1<p<2,\\ 1-2/p,&2<p<\infty.\end{cases}$$

Formalization targets

Goal: Theorem 1.1

For fixed $1<p<\infty$, $p\ne2$:

$$\forall D>1\ \exists C_{p,D}\ \forall n\ge2:\quad \frac{\log n}{\log(1+2D)}\ \le\ d_p(n,D)\ \le\ \exp\bigl(C_{p,D}(\log n)^{\gamma(p)}\bigr);$$ $$\Bigl\lfloor\tfrac{n-1}{4}\Bigr\rfloor^2\ \le\ d_p(n,1)\ \le\ \binom n2\qquad(n\ge9);$$ $$\lim_{n\to\infty}\frac{\log d_p(n,D)}{\log n}=\begin{cases}0,&D>1,\\ 2,&D=1.\end{cases}$$

Since $\gamma(p)<1$, the upper bound is $n^{o(1)}$. The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.

Significance

For $p\ne2$ the best previous finite-set bounds were polynomial in $n$ (linear for $p<2$), and for $p>2$ logarithmic dimension is impossible. The theorem places $d_p(n,D)$ at $n^{o(1)}$ for every fixed $D>1$, in contrast with exact embeddings, where the dimension is of order $n^2$. Thus the exponent $\lim \log d_p/\log n$ jumps from $2$ at $D=1$ to $0$ for every $D>1$. The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.

The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.

Difficulty

Linear maps cannot work: fixed-distortion linear maps on some $L_p$ configurations need dimension proportional to $n$ when $p\ne2$. Subspace discretization theorems apply to the span of the points, which has dimension up to $n-1$, so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in $L_p$. One needs a single random scalar map whose increments have nearly equal normalized $p$-th moments simultaneously for all $\binom n2$ pairs, with relative (not additive) error control.

Formalization scope

• coordinateDistance p y z is $(\sum_a |y_a-z_a|^p)^{1/p}$ on Fin d → ℝ.
• GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the $\ell_p$ distance and a scale $s>0$.
• dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.
• gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.
• The limit is a Tendsto statement along n : ℕ for each $D\ge1$.

A complete development needs $L_p$ spaces, $p$-stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.

Selected references

• OpenAI, Subpolynomial dimension reduction in $L_p$, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Subpolynomial-dimension-reduction-in-Lp-September-23-2026/paper.pdf
• W. B. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26, 1984. https://doi.org/10.1090/conm/026/737400
• K. Ball, Isometric embedding in $l_p$-spaces, European J. Combin., 1990. https://doi.org/10.1016/S0195-6698(13)80131-X
• G. Schechtman, Dimension reduction in $L_p$, $0<p<2$, preprint, 2011. https://arxiv.org/abs/1110.2148
• B. Brinkman, M. Charikar, On the impossibility of dimension reduction in $\ell_1$, J. ACM, 2005. https://doi.org/10.1145/1089023.1089026
• J. R. Lee, M. Mendel, A. Naor, Metric structures in $L_1$: dimension, snowflakes, and average distortion, European J. Combin., 2005. https://doi.org/10.1016/j.ejc.2004.07.002
• A. Naor, Metric dimension reduction: a snapshot of the Ribe program, Proc. ICM 2018. https://arxiv.org/abs/1809.02376
• A. Naor, K. Ren, A threshold phenomenon for embeddings of Euclidean snowflakes and impossibility of dimension reduction, preprint, 2026. https://arxiv.org/abs/2609.01079
• O. Gurel-Gurevich, A. Nachmias, S. Sachdeva, A tight bound on localization of electrical flows, preprint, 2026. https://arxiv.org/abs/2605.24130

Motivation: $L_1$ embeddings, sparsest cut and the GNRS conjecture

A finite metric embeds into $L_1$ exactly when it is a nonnegative combination of cut metrics $\delta_S(u,v)=|\mathbf 1_S(u)-\mathbf 1_S(v)|$. This makes $L_1$ distortion the right measure for the flow–cut gap: given edge capacities and pairwise demands, the ratio between the sparsest cut value $\phi_*$ and the maximum concurrent flow $\lambda_*$. Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) developed this connection, 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 that every proper minor-closed family embeds into $L_1$ with uniformly bounded distortion (the GNRS conjecture). Graphs of bounded treewidth form one of its basic cases.

Timeline

• 1986 — Robertson and Seymour: excluding a fixed planar graph as a minor bounds the treewidth (JCTB 1986).
• 2004 — Gupta, Newman, Rabinovich and Sinclair prove the treewidth-two (series-parallel) case, show that some series-parallel metrics need expected tree distortion $\Omega(\log n)$, and state the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: bounded distortion for $k$-outerplanar graphs (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent obtain the optimal bound $2$ for treewidth two (FOCS 2008), matched by Lee and Raghavendra (DCG 2010).
• 2010 — Chlamtáč, Krauthgamer and Raghavendra: bounded distortion for bounded treewidth under a local-consistency assumption on small vertex sets (APPROX/RANDOM 2010).
• 2013 — Lee and Sidiropoulos settle bounded pathwidth via stochastic tree embeddings (Combinatorica 2013); Lee and Poore treat 2-sums of a fixed finite family (SoCG 2013).
• 2022 — Abraham, Filtser, Gupta and Neiman: $O(\sqrt p)$ distortion for pathwidth $p$ (SICOMP 2022).
• 2025 — Filtser et al.: optimal padded decompositions for bounded treewidth and an $O(\sqrt{\log(2+t)\log n})$ bound (TheoretiCS 2025).
• 2026 — An OpenAI preprint, $L_1$ Embeddings of Graphs of Bounded Treewidth (OpenAI Math Release, September 23, 2026), claims a uniform bound for every fixed treewidth. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G=(V,E)$ be a finite connected graph with edge lengths $\ell:E\to(0,\infty)$. The shortest-path metric $d_{G,\ell}(u,v)$ is the least total length of a path from $u$ to $v$.

A tree decomposition of $G$ is a finite tree $T$ with bags $B_t\subseteq V$ ($t\in V(T)$) such that the bags cover $V$, each edge has both endpoints in some bag, and for each vertex $v$ the nodes whose bag contains $v$ induce a connected subtree. In this mission, as in the source, $k$ bounds the bag cardinality $|B_t|\le k$, so the treewidth bound is $k-1$.

A map $F:V\to\ell_1^m$ has distortion at most $C$ if $d_{G,\ell}(u,v)\le\|F(u)-F(v)\|_1\le C\,d_{G,\ell}(u,v)$.

Formalization targets

Goal: Theorem 1.1 (bounded-treewidth graph metrics in $L_1$)

For every integer $k\ge2$ there is a constant $C_k\ge1$ such that for every nonempty finite connected graph $G$ with a tree decomposition of bag size at most $k$ and every $\ell:E\to(0,\infty)$, there are $m$ and $F:V\to\ell_1^m$ with

$$d_{G,\ell}(u,v)\;\le\;\|F(u)-F(v)\|_1\;\le\;C_k\,d_{G,\ell}(u,v)\qquad(u,v\in V).$$

$C_k$ is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. 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 bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives $\lambda_*\le\phi_*\le C_k\lambda_*$ for every multicommodity instance on graphs of treewidth less than $k$. By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum $L_1$ distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion $(2+\varepsilon)C_k$. With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.

Formalizing it. The proof constructs cut measures directly on a tree decomposition and combines them with padded random partitions from the literature. A formal proof would certify that the constants depend only on $k$, the point at which earlier approaches lost uniformity.

Difficulty

The successful pathwidth approach embeds the graph stochastically into dominating trees, but that route cannot work here: some series-parallel metrics require expected tree distortion $\Omega(\log n)$ (GNRS 2004, Theorem 5.6). Local-consistency approaches assume that small vertex sets admit compatible isometric cut representations, which a general bounded-treewidth metric need not provide. Multiscale constructions from padded partitions give good separation at each scale, but summing their contributions loses a factor growing with the number of scales. The construction must handle arbitrary branching of the decomposition tree and arbitrary edge-length ratios without such accumulation.

Formalization scope

• The vertex type V is any nonempty Fintype with decidable equality; G : SimpleGraph V is connected.
• HasTreeDecomposition G k: a tree T on Fin n, bags Fin n → Finset V covering all vertices and all edges, with the bags containing each vertex inducing a connected subgraph of T, and all bags of cardinality at most k.
• Edge lengths are ℓ : G.edgeSet → ℝ, strictly positive. shortestPathDistance is the sInf of lengths of paths (IsPath) from $u$ to $v$; this set is finite and nonempty for a connected finite graph, so the infimum is the true distance.
• The target is the finite-dimensional space PiLp 1 (Fin m → ℝ) with $m$ chosen per graph; this is the source's remark (p. 2) that the target can be taken to be finite-dimensional $\ell_1$, and it is at least as strong as an $L_1(\mu)$ target.
• The constant C depends only on k and is quantified before the graph.
• Infrastructure needed: tree decompositions, cut-measure representations of $\ell_1$ metrics, Markov flows on layered graphs, padded decompositions. Tree-decomposition and cut-metric infrastructure is reusable.

Selected references

• N. Robertson, P. D. Seymour, Graph minors. V. Excluding a planar graph, J. Combin. Theory Ser. B 41 (1986), 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995), 215–245. 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. 27 (1998), 291–301. https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica 24 (2004), 233–269. https://doi.org/10.1007/s00493-004-0015-x
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008, 761–770. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, P. Raghavendra, Coarse differentiation and multi-flows in planar graphs, Discrete Comput. Geom. 43 (2010), 346–362. https://doi.org/10.1007/s00454-009-9172-4
• E. Chlamtáč, R. Krauthgamer, P. Raghavendra, Approximating sparsest cut in graphs of bounded treewidth, APPROX/RANDOM 2010, LNCS 6302, 124–137. https://doi.org/10.1007/978-3-642-15369-3_10
• J. R. Lee, A. Sidiropoulos, Pathwidth, trees, and random embeddings, Combinatorica 33 (2013), 349–374. https://doi.org/10.1007/s00493-013-2685-8
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. 51 (2022), 290–314. https://doi.org/10.1137/19M1296021
• A. Filtser, T. Friedrich, D. Issac, N. Kumar, H. Le, N. Mallek, Z. Zeif, Optimal padded decomposition for bounded treewidth graphs, TheoretiCS 4 (2025), Article 22. https://doi.org/10.46298/theoretics.25.22
• OpenAI, $L_1$ Embeddings of Graphs of Bounded Treewidth, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026/paper.pdf

Motivation

The projection body $\Pi K$ of a convex body $K\subset\mathbb R^d$ is the convex body whose support function in a unit direction $u$ is the $(d-1)$-dimensional volume of the shadow of $K$ on $u^\perp$. Petty showed that $K\mapsto\Pi K$ is affinely covariant, so the normalized volume

$$R_d(K)=\frac{|\Pi K|}{|K|^{d-1}}$$

is invariant under invertible affine maps, and its extremal values are natural affine isoperimetric questions. Petty's conjecture concerns the minimum (ellipsoids). For the maximum, Brannen conjectured in 1996 that simplices maximize $R_d$ among all convex bodies (Mathematika 1996); the simplex value is $c_d=(d+1)d^d/d!$.

This mission asks for a formal proof of an explicit counterexample in dimension $20$, as stated in an OpenAI preprint dated September 24, 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.

Background

• 1967 — Petty, Projection bodies, establishes the affine covariance of the projection-body operator (Proc. Colloq. Convexity, Copenhagen 1965).
• 1996 — Brannen conjectures that simplices maximize $R_d$ (Mathematika 1996).
• 2002 — Ludwig characterizes the projection-body operator by valuations (Adv. Math. 2002).
• 2025 — Henk gives the lower bound $2^d(9/8)^{\lfloor d/3\rfloor}$ for the optimal upper constant among centrally symmetric bodies (Acta Math. Sci. 2025).
• 2026 — Chen, Feng, Li, Xi and Xu prove $R_3(K)\le18=c_3$, with tetrahedra as maximizers (preprint); Feng, Hu, Liu and Xu give counterexamples to Brannen's bound in every dimension $d\ge9$ using polytopes with at most $d+2$ facets (preprint).
• September 2026 — The OpenAI preprint gives a direct product counterexample with exact value in dimension $20$ (Theorem 1, p. 2).

Setting

A convex body in $\mathbb R^d$ is compact and convex with nonempty interior, and $|\cdot|$ is $d$-dimensional volume. For $u\in\mathbb R^d$ the brightness is $h_{\Pi K}(u)=\|u\|\operatorname{vol}_{d-1}(\operatorname{proj}_{u^\perp}K)$, and

$$\Pi K=\{y:\ \langle u,y\rangle\le h_{\Pi K}(u)\ \text{for all }u\}.$$

Let $T_{10}=\operatorname{conv}(0,e_1,\dots,e_{10})\subset\mathbb R^{10}$ be the standard simplex and

$$K=T_{10}\times T_{10}=\{x\in\mathbb R^{20}:\ (x_1,\dots,x_{10})\in T_{10},\ (x_{11},\dots,x_{20})\in T_{10}\}.$$

The benchmark constant is $c_d=(d+1)d^d/d!$, which equals $R_d$ of every $d$-simplex (Proposition 5, p. 4).

Formalization targets

Milestone: failure of the simplex bound in dimension 20 (Theorem 1, p. 2, last sentence, with Proposition 5)

It is not true that $R_{20}(P)\le R_{20}(T_{20})$ for every convex body $P\subset\mathbb R^{20}$.

Goal: Theorem 1 (p. 2)

$K=T_{10}\times T_{10}$ is a convex body and

$$\frac{R_{20}(K)}{c_{20}}=\frac{121\binom{20}{10}}{21\cdot 2^{20}}=\frac{22\,355\,476}{22\,020\,096}>1,\qquad\text{so}\qquad |\Pi K|>c_{20}|K|^{19}.$$

Significance

The result itself. Brannen's conjecture fails: in dimension $20$ the simplex is not the maximizer of normalized projection-body volume. The mechanism is the product identity $R_{r+s}(A\times B)=R_r(A)R_s(B)$ for polytopes (Proposition 3, p. 3), which shows that $c_rc_s$ is a lower bound for any universal upper constant in dimension $r+s$; iterating it gives an exponential excess $R_n(K_n)\ge\lambda^nR_n(T_n)$ for all large $n$ (Corollary 6, p. 6). The counterexample in dimensions $d\ge9$ was obtained independently by Feng, Hu, Liu and Xu; the contribution here is an explicit product witness with an exact rational value. The optimal upper constant and its maximizers remain separate questions.

Formalizing it. Every ingredient is elementary: the facet formula for projection bodies of polytopes (Cauchy's formula, Lemma 2, p. 2), the facet structure of a Cartesian product, affine covariance (Lemma 4, p. 3), and a fiber computation of $|\Pi T_d|$. A formal proof would supply Mathlib with projection bodies of polytopes and Cauchy's projection formula, both reusable. The final comparison is an exact rational identity.

Difficulty

There is no shortcut through general inequalities: the statement is a strict comparison of two explicit volumes in dimension $20$, so both $|\Pi K|$ and $|\Pi T_{20}|$ must be computed exactly. Computing $\Pi$ of a product directly from shadow volumes is unwieldy; the efficient route goes through facet area-normal vectors, which requires proving that, up to a null set, each point of a shadow lies over exactly two facet interiors, and that the facets of $A\times B$ are exactly $F\times B$ and $A\times G$. The simplex value needs the volume of a cube plus a segment.

Formalization scope

• Space is EuclideanSpace ℝ (Fin 20). In the goal, projectionVolume is the induced Lebesgue measure on the submodule $(\operatorname{span}\{u\})^\perp$ of the orthogonal projection of $K$; brightness u = ‖u‖ * projectionVolume, so the support-function inequality is imposed for all $u$ (the homogeneous extension).
• productWitness is the set of $x$ whose first and last ten coordinates both lie in standardSimplex 10; the goal includes that it is compact, convex, with nonempty interior.
• simplexConstant 20 is the explicit number $c_{20}$, not $R_{20}(T_{20})$; the goal states the exact ratio, its reduced fraction, the strict inequality, and $|\Pi K|>c_{20}|K|^{19}$.
• The milestone uses a separate definition file: shadow volumes via euclideanHausdorffMeasure (d-1) of the image under the orthogonal projection, and compares with ratio (simplex 20), so it implicitly needs Proposition 5.
• Volumes are read with toReal; all bodies involved are bounded, so no infinite value is hidden.

Selected references

• OpenAI, A product counterexample to the simplex maximum for projection-body volume, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026/paper.pdf
• N. S. Brannen, Volumes of projection bodies, Mathematika 43 (1996), 255–264. https://doi.org/10.1112/S002557930001175X
• C. M. Petty, Projection bodies, Proc. Colloq. Convexity (Copenhagen, 1965), 1967, 234–241.
• M. Ludwig, Projection bodies and valuations, Adv. Math. 172 (2002), 158–168. https://doi.org/10.1016/S0001-8708(02)00021-X
• M. Henk, Note on projection bodies of zonotopes with n+1 generators, Acta Math. Sci. 45 (2025), 96–103. https://doi.org/10.1007/s10473-025-0107-9
• S. Chen, Y. Feng, Y. Li, D. Xi, L. Xu, Petty's conjectured projection inequality in dimension three, preprint (2026). https://archive.ymsc.tsinghua.edu.cn/pacm_download/741/12780-pettyinequality.pdf
• Y. Feng, S. Hu, W. Liu, L. Xu, On the reverse projection inequality, preprint (2026). https://archive.ymsc.tsinghua.edu.cn/pacm_download/743/12781--2026.8.26.pdf
• C. Saroglou, On the shape of a convex body with respect to its second projection body, Adv. Appl. Math. 67 (2015), 55–74. https://doi.org/10.1016/j.aam.2015.03.004

Motivation

The projection body $\Pi K$ of a convex body $K\subset\mathbb R^n$ packages the areas of all shadows of $K$ into a single convex body: its support function in direction $u$ is the $(n-1)$-dimensional volume of the orthogonal projection of $K$ onto $u^\perp$. The normalized volume $|\Pi K|/|K|^{n-1}$ is invariant under translations and invertible linear maps, so asking for its extremizers is an affine isoperimetric problem. Petty's projection-volume conjecture (Petty, 1971) predicts that this ratio is minimized exactly by ellipsoids. It is related to, but distinct from, Petty's projection inequality for the polar body $\Pi^\circ K$, which is a classical theorem; inequalities in this family underlie affine Sobolev inequalities and isoperimetric inequalities in normed spaces.

This mission asks for a formal proof of the conjecture in every dimension $n\ge4$, as stated in an OpenAI preprint dated September 24, 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.

Background

• 1971 — Petty formulates the conjecture (Isoperimetric problems, Proc. Conf. Convexity and Combinatorial Geometry, Univ. of Oklahoma, 1971).
• 1990 — Lutwak reformulates it as a lower bound for a two-body integral with kernel $|u\cdot v|$ against surface-area measures (Contemp. Math. 113, 1990) and derives lower-degree consequences (Geom. Dedicata 1990).
• 2015–2018 — Saroglou's class-reduction results for the second projection body (Adv. Appl. Math. 2015); Saroglou–Zvavitch local minimality near the ball in $L^\infty$ (JFA 2017); Ivaki's local rigidity for $C^2$ solutions of $\Pi^2K=cK$ (Mathematika 2018).
• 2026 — Mielke-Sulz proves the conjecture for bodies of revolution (arXiv:2609.13517); Chen, Feng, Li, Xi and Xu prove the unrestricted three-dimensional case with ellipsoid equality (preprint, August 2026).
• September 2026 — The OpenAI preprint claims all dimensions $n\ge4$ (Theorem 1.1, p. 1).

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior, and $|\cdot|$ denotes $n$-dimensional Lebesgue volume. For a unit vector $u$, let $\operatorname{proj}_{u^\perp}K$ be the orthogonal projection of $K$ onto the hyperplane $u^\perp$ and $\operatorname{vol}_{n-1}$ the Lebesgue measure on that hyperplane. The projection body is

$$\Pi K=\{x\in\mathbb R^n:\ \langle u,x\rangle\le \operatorname{vol}_{n-1}(\operatorname{proj}_{u^\perp}K)\ \text{for every unit }u\},$$

the convex body with support function $h_{\Pi K}(u)=\operatorname{vol}_{n-1}(\operatorname{proj}_{u^\perp}K)$. Write $\kappa_m$ for the volume of the Euclidean unit ball $B_2^m$. An ellipsoid is a set $a+TB_2^n$ with $a\in\mathbb R^n$ and $T$ an invertible linear map. Since $\Pi B_2^n=\kappa_{n-1}B_2^n$, the ball has ratio $\kappa_{n-1}^n\kappa_n^{2-n}$.

Formalization targets

Goal: Theorem 1.1 (p. 1)

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

$$\frac{|\Pi K|}{|K|^{n-1}}\ \ge\ \kappa_{n-1}^{\,n}\,\kappa_n^{\,2-n},$$

with equality if and only if $K$ is an ellipsoid.

Significance

The result itself. Together with the separately proved three-dimensional case, it settles Petty's conjecture for all $n\ge3$ (in dimension $2$ the ratio is constant up to the standard identification). The preprint derives from it the Lutwak–Petty lower-degree inequalities, a mixed determinant-gradient inequality strengthening the Sobolev–Zhang affine $L^1$ inequality, and the sharp Holmes–Thompson isoperimetric inequality in normed spaces (Corollaries 7.1–7.3, pp. 27–29). Those corollaries for $n=3$ rely on the external three-dimensional theorem.

Formalizing it. The proof uses the first variation of volume, spherical harmonics with explicit cosine and Funk transform multipliers, a strict harmonic estimate for arbitrary norms, a variational representation of support functionals, and Brouwer's fixed-point theorem. Mathlib has Brouwer-type results only in limited forms and has no spherical-harmonic decomposition of $L^2(S^{n-1})$; these would be reusable. No machine-checked proof of any case $n\ge2$ of the conjecture is known.

Difficulty

Previous results are local: they require the body, after a linear change of variables, to be close to the ball, because the harmonic analysis of the projection operator only controls perturbations of the ball. A global argument must handle arbitrary bodies without symmetry or regularity. In the preprint (pp. 2–3) the degree-two spherical harmonic component is not a zero mode of the relevant sign-test operator and has to be removed by choosing affine coordinates; this needs a continuous family of variational minimizers extended to singular matrices and a fixed-point argument (Proposition 5.5, p. 23). Harmonics of degree at least four are controlled by a strict norm estimate valid for every norm (Theorem 4.1, p. 12). The equality case must come out of the same estimates.

Formalization scope

• Space n is EuclideanSpace ℝ (Fin n); IsConvexBody K is compact, convex, nonempty interior; $n\ge4$.
• shadowVolume K u is the measure, in the induced Euclidean volume on the submodule $(\operatorname{span}\{u\})^\perp$, of the image of $K$ under orthogonalProjectionOnto. projectionBody K is the intersection of half-spaces over unit vectors, which has support function shadowVolume K because that function is itself a support function.
• projectionRatio K = volume.real (projectionBody K) / volume.real K ^ (n - 1); for a convex body both volumes are finite and the denominator is positive.
• pettyConstant n = kappa (n-1) ^ n * kappa n ^ (2 - n) with an integer exponent, $\kappa_m$ the volume of the closed unit ball.
• IsEllipsoid K: $K = a + T(\text{closed unit ball})$ for a linear equivalence $T$.
• The goal is the conjunction of the inequality and the iff equality characterization; neither part is vacuous for $n\ge4$.

Selected references

• OpenAI, Petty's projection-volume conjecture in dimensions at least four, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026/paper.pdf
• C. M. Petty, Isoperimetric problems, Proc. Conf. Convexity and Combinatorial Geometry, Univ. of Oklahoma, 1971, 26–41.
• E. Lutwak, On a conjectured projection inequality of Petty, Contemp. Math. 113 (1990), 171–182.
• E. Lutwak, On quermassintegrals of mixed projection bodies, Geom. Dedicata 33 (1990), 51–58. https://doi.org/10.1007/BF00147600
• C. Saroglou, A. Zvavitch, Iterations of the projection body operator and a remark on Petty's conjectured projection inequality, J. Funct. Anal. 272 (2017), 613–630. https://doi.org/10.1016/j.jfa.2016.08.015
• M. N. Ivaki, A local uniqueness theorem for minimizers of Petty's conjectured projection inequality, Mathematika 64 (2018), 1–19. https://doi.org/10.1112/S0025579317000444
• S. Chen, Y. Feng, Y. Li, D. Xi, L. Xu, Petty's conjectured projection inequality in dimension three, preprint (2026). https://archive.ymsc.tsinghua.edu.cn/pacm_download/741/12780-pettyinequality.pdf
• F. Mielke-Sulz, The Petty conjecture for convex bodies of revolution, arXiv:2609.13517 (2026). https://arxiv.org/abs/2609.13517v1
• G. Zhang, The affine Sobolev inequality, J. Differential Geom. 53 (1999), 183–202.
• R. J. Gardner, The Brunn–Minkowski inequality, Bull. AMS 39 (2002), 355–405. https://doi.org/10.1090/S0273-0979-02-00941-2

Motivation

Place a convex body $K\subset\mathbb R^n$ in the position coordinates and its polar $K^\circ$ in the momentum coordinates of the standard symplectic space $(\mathbb R^n_q\times\mathbb R^n_p,\omega_0)$. The resulting Lagrangian product $K\times K^\circ$ links two problems. Its volume is the Mahler volume product $|K||K^\circ|$, and its symplectic capacities measure how large a round ball can be squeezed into it by a symplectic map. Since symplectic maps preserve volume, a ball of capacity $c$ inside $\operatorname{int}K\times\operatorname{int}K^\circ$ forces $|K||K^\circ|\ge c^n/n!$. Artstein-Avidan, Karasev and Ostrover showed that the Hofer–Zehnder capacity of $K\times K^\circ$ equals $4$ for every origin-symmetric $K$ and connected Viterbo's volume–capacity conjecture to Mahler's conjecture (Duke 2014). Whether actual balls of capacity close to $4$ fit, i.e. whether the Gromov width also equals $4$, was open.

This mission asks for a formal proof that it does, as claimed 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

• 1939 — Mahler formulates the symmetric volume-product problem (Časopis 1939).
• 1985 — Gromov's nonsqueezing theorem shows that ball embeddings detect symplectic rigidity beyond volume (Invent. Math. 1985).
• 1987 — Bourgain–Milman reverse Santaló inequality (Invent. Math. 1987); Reisner's sharp inequality for unconditional bodies (J. LMS 1987).
• 1994 — Hofer and Zehnder introduce their capacity (book, 1994).
• 2000 — Viterbo proposes the volume–capacity inequality for convex domains (JAMS 2000).
• 2013 — Latschev, McDuff and Schlenk compute Gromov widths of four-dimensional tori with area-preserving constructions (G&T 2013).
• 2014 — Artstein-Avidan, Karasev and Ostrover prove $c_{HZ}(K\times K^\circ)=4$ for symmetric $K$ (Duke 2014).
• 2019–2021 — Ramos and Sepe identify the cube–cross-polytope product with a ball of capacity $4$ (J. Symplectic Geom. 2019); Karasev treats $\ell_p$ balls (Israel J. Math. 2021).
• 2020 — Iriyeh and Shibata prove the three-dimensional symmetric Mahler conjecture (Duke 2020).
• 2024–2026 — Haim-Kislev and Ostrover disprove the general Viterbo conjecture with a non-symmetric four-dimensional example (Annals 2026); Vicente studies functional-dual products and records the width question (arXiv:2505.07572).
• September 2026 — The OpenAI preprint claims Gromov width $4$ for every symmetric polar product, $n\ge2$ (Theorem 1.1, p. 1).

Setting

An origin-symmetric convex body $K\subset\mathbb R^n$ is compact, convex, has nonempty interior, and satisfies $x\in K\iff -x\in K$. Its polar is $K^\circ=\{p:\langle q,p\rangle\le1\ \forall q\in K\}$. On $\mathbb R^n\times\mathbb R^n$ put $\omega_0((q,p),(q',p'))=\langle q,p'\rangle-\langle q',p\rangle$, and let

$$U_K=\operatorname{int}K\times\operatorname{int}K^\circ,\qquad B^{2n}(c)=\{(q,p):\pi(|q|^2+|p|^2)<c\}.$$

A symplectic embedding of an open set $U$ into $V$ is a $C^\infty$ map on $U$ that is a topological embedding, maps $U$ into $V$, and whose derivative preserves $\omega_0$ at every point. The Gromov width $c_G(V)$ is the supremum of capacities $c>0$ for which $B^{2n}(c)$ embeds symplectically into $V$.

Formalization targets

Milestone: the symmetric Mahler inequality (Corollary 5.3, p. 16)

For every $n\ge1$ and origin-symmetric convex body $K\subset\mathbb R^n$, $\ |K|\,|K^\circ|\ge 4^n/n!$.

Goal: Theorem 1.1 (p. 1)

For every $n\ge2$ and every origin-symmetric convex body $K\subset\mathbb R^n$,

$$c_G(U_K)=4,$$

and for every $0<c<4$ there is a symplectic embedding $B^{2n}(c)\hookrightarrow U_K$. No embedding at capacity exactly $4$ is asserted.

Significance

The result itself. It answers the symmetric-polar-product width question with no smoothness, strict convexity or unconditionality assumptions, and through volume preservation it implies the symmetric Mahler inequality in every dimension (Corollary 5.3). For $n\ge3$ it also transports finite ball packings satisfying strict volume and pairwise-capacity conditions into $U_K$ (Corollary 5.5, p. 17). It is specific to symmetric polar products: the general Viterbo conjecture is false.

Formalizing it. Mathlib has smooth manifolds and differential forms but no symplectic capacities, nonsqueezing, or Moser's deformation method. A formal proof would need these, together with a conformal map of the disk with explicit boundary estimates. These components are reusable across symplectic geometry. No machine-checked computation of a Gromov width of a non-trivial domain is known.

Difficulty

The upper bound $c_G\le4$ follows from Gromov nonsqueezing and a supporting-cylinder argument (or from the Hofer–Zehnder computation). The lower bound is the hard direction: knowing $c_{HZ}=4$ does not produce any ball, and explicit embeddings were previously known only for special families ($\ell_p$ balls, the cube). The preprint's route (Sections 2–4) needs balls of capacity close to $\pi k$ from holomorphic maps vanishing to order $k$, and a momentum scale $S_k=(1+o(1))\pi k/4$ that is uniform up to the tips of a conformal lens, where slice heights approach $\pm1$ as $k$ grows; a non-uniform estimate does not suffice.

Formalization scope

• Position and momentum spaces are EuclideanSpace ℝ (Fin n); phase space is their product. polar uses the real inner product; polarProduct K is interior K ×ˢ interior (polar K).
• capacityBall n c is the open ball $\pi(|q|^2+|p|^2)<c$, so a ball of radius $r$ has capacity $\pi r^2$.
• HasSymplecticEmbedding U V: some e with ContDiffOn ℝ ∞ e U, IsEmbedding on the subtype U, MapsTo e U V, and $\omega_0(De\,v,De\,w)=\omega_0(v,w)$ for all $z\in U$.
• gromovWidth is an sSup in ℝ≥0∞ of the admissible capacities, so an unbounded set would give ⊤; the goal asserts the value 4 and separately every capacity below $4$.
• The hypothesis is $n\ge2$, as in the source; the milestone allows $n\ge1$.

Welcome contributions: a Lean notion of symplectic embedding between open subsets of $\mathbb R^{2n}$, Gromov nonsqueezing (as an axiom-free target in its own right), and volume preservation for symplectic maps.

Selected references

• OpenAI, Symplectic Balls in Symmetric Polar Products, OpenAI Math Release preprint, September 22, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symplectic-Balls-in-Symmetric-Polar-Products-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
• S. Artstein-Avidan, R. Karasev, Y. Ostrover, From symplectic measurements to the Mahler conjecture, Duke Math. J. (2014). https://doi.org/10.1215/00127094-2794999
• M. Gromov, Pseudo holomorphic curves in symplectic manifolds, Invent. Math. (1985). https://doi.org/10.1007/BF01388806
• C. Viterbo, Metric and isoperimetric problems in symplectic geometry, J. Amer. Math. Soc. (2000). https://doi.org/10.1090/S0894-0347-00-00328-3
• H. Hofer, E. Zehnder, Symplectic Invariants and Hamiltonian Dynamics, Birkhäuser (1994). https://doi.org/10.1007/978-3-0348-8540-9
• P. Haim-Kislev, Y. Ostrover, A counterexample to Viterbo's conjecture, Ann. of Math. (2026). https://doi.org/10.4007/annals.2026.203.2.5
• R. Karasev, Mahler's conjecture for some hyperplane sections, Israel J. Math. (2021). https://doi.org/10.1007/s11856-021-2114-4
• V. G. B. Ramos, D. Sepe, On the rigidity of Lagrangian products, J. Symplectic Geom. (2019). https://doi.org/10.4310/JSG.2019.v17.n5.a7
• J. Latschev, D. McDuff, F. Schlenk, The Gromov width of 4-dimensional tori, Geom. Topol. (2013). https://doi.org/10.2140/gt.2013.17.2813
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0182927-5
• K. Mahler, Ein Übertragungsprinzip für konvexe Körper, Časopis Pěst. Mat. Fys. (1939). https://doi.org/10.21136/CPMF.1939.109441