All missions

Motivation

Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching

$$\alpha_{\mathrm{GW}}=\min_{-1\le\rho<1}\frac{2\arccos\rho}{\pi(1-\rho)}=0.878567\ldots$$

(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above $16/17$, and optimality of $\alpha_{\mathrm{GW}}$ was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio $\alpha\in(\alpha_{\mathrm{GW}},1]$ is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1972 — Karp lists Max-Cut among the original NP-complete problems (Karp 1972).
• 1995 — Goemans and Williamson give the SDP algorithm with ratio $\alpha_{\mathrm{GW}}$ (JACM 1995).
• 2000–2001 — Håstad's optimal inapproximability results (JACM 2001) combined with the gadgets of Trevisan, Sorkin, Sudan and Williamson (SICOMP 2000) rule out ratios above $16/17$.
• 2002 — Feige and Schechtman show the SDP integrality gap approaches $\alpha_{\mathrm{GW}}$ (RSA 2002); Khot formulates the Unique Games Conjecture (STOC 2002).
• 2007–2010 — Khot, Kindler, Mossel and O'Donnell prove that $\alpha_{\mathrm{GW}}$ is optimal assuming the UGC, conditional on Majority Is Stablest (SICOMP 2007), which Mossel, O'Donnell and Oleszkiewicz prove (Annals 2010) via Borell's Gaussian noise-stability bound (1985). O'Donnell–Wu (STOC 2008) and Raghavendra (STOC 2008) extend the UG-based picture.
• 2017–2025 — The Grassmann-graph programme establishes the 2-to-1 Games Theorem with imperfect completeness: Khot–Minzer–Safra (ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (ToC 2025), Barak–Kothari–Steurer (ITCS 2019), Khot–Minzer–Safra expansion (Annals 2023).
• 2026 — The OpenAI preprint claims unconditional NP-hardness at every ratio above $\alpha_{\mathrm{GW}}$.

Setting

A simple unweighted graph on $N$ vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map $c$ from the vertices to $\{0,1\}$; its size is the number of unordered edges $\{u,v\}$ with $c(u)\ne c(v)$, and $\mathrm{MaxCut}(G)$ is the largest cut size. An algorithm is an $\alpha$-approximation if it always returns a cut of size at least $\alpha\cdot\mathrm{MaxCut}(G)$.

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for $\alpha$ consists of rationals $Y>0$ and $N\ge0$ with $N<\alpha Y$, and a deterministic polynomial-time map $\varphi\mapsto(G_\varphi,Q_\varphi)$ outputting a graph together with a positive integer scale $Q_\varphi$ such that

$$\varphi\in\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\ge Y,\qquad \varphi\notin\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\le N.$$

Given such a reduction, an $\alpha$-approximation algorithm would decide 3SAT by comparing its output with $N Q_\varphi$.

Formalization targets

Goal: optimal Max-Cut hardness (Theorem 1.1, p. 1)

For every real $\alpha$ with $\alpha_{\mathrm{GW}}<\alpha\le1$, a gap reduction for $\alpha$ from 3SAT to simple unweighted Max-Cut exists:

$$\forall\,\alpha\in(\alpha_{\mathrm{GW}},1]:\quad \mathrm{GapReduction}(\alpha)\ne\varnothing.$$

In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational $t\in(0,1)$, $B(t)=\tfrac{2}{\pi}\arcsin t$ and $0<\varepsilon<(t-B(t))/4$, it is NP-hard to distinguish $\mathrm{Val}\ge\frac{1+t}{2}-\varepsilon$ from $\mathrm{Val}\le\frac{1+B(t)}{2}+\varepsilon$ on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.

Significance

The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.

Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.

Difficulty

The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).

Formalization scope

• Graphs are OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.
• The output is a ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.
• alphaGW is defined as the sInf of $2\arccos\rho/(\pi(1-\rho))$ over $\rho\in[-1,1)$; this set is nonempty and bounded below, so the infimum is the true constant.
• The reduction is a Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.
• The hypothesis $\alpha_{\mathrm{GW}}<\alpha\le1$ is satisfiable, and the conclusion requires an actual strict gap noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.

Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.

Selected references

• OpenAI, A Direct Proof of Optimal Max-Cut Hardness, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026/paper.pdf
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• L. Trevisan, G. Sorkin, M. Sudan, D. Williamson, Gadgets, approximation, and linear programming, SIAM J. Comput. 29 (2000). https://doi.org/10.1137/S0097539797328847
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010). https://doi.org/10.4007/annals.2010.171.295
• U. Feige, G. Schechtman, On the optimality of the random hyperplane rounding technique for MAX CUT, Random Structures Algorithms 20 (2002). https://doi.org/10.1002/rsa.10036
• I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

Motivation

A Unique Game is a system of constraints between pairs of variables, each constraint saying that the label of one endpoint is a fixed permutation of the label of the other. Deciding whether all constraints can be satisfied is easy (propagate labels along a spanning tree), so the interesting question is approximate: given an instance in which almost all constraints can be satisfied, can a polynomial-time algorithm find a labeling that satisfies even a small fraction?

Khot's Unique Games Conjecture (UGC, 2002) asserts that it cannot, unless P = NP. The conjecture matters because many optimal approximation thresholds have been proved conditionally on it: the Goemans–Williamson ratio for Max-Cut (KKMO 2007), the factor $2$ for Vertex Cover (Khot–Regev 2008), the basic-SDP threshold for every constraint satisfaction problem (Raghavendra 2008), and hardness for ordering, multicut/sparsest-cut and correlation-clustering problems. An unconditional proof would turn all of these into NP-hardness results.

This mission asks for a machine-checked proof of the Unique Games Theorem as stated in an OpenAI preprint dated September 23, 2026 (source), which claims a positive resolution of the conjecture. The preprint has not been peer reviewed, and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

• 2001 — Håstad proves optimal inapproximability for linear equations mod 2 with near-perfect completeness (JACM 2001); this gap is the hardness input used by the preprint.
• 2002 — Khot introduces Unique Games and formulates the conjecture (STOC 2002).
• 2005–2008 — Conditional optimal hardness for Max-Cut (Khot, Kindler, Mossel, O'Donnell, SICOMP 2007), Vertex Cover (Khot–Regev, JCSS 2008) and every CSP (Raghavendra, STOC 2008). Khot–Vishnoi build SDP integrality gaps (JACM 2015, FOCS 2005).
• 2005–2010 — Algorithms that delimit the conjecture's quantifiers: Trevisan (ToC 2008), Charikar–Makarychev–Makarychev with value $1-O(\sqrt{\epsilon\log q})$ (STOC 2006), and the subexponential algorithm of Arora–Barak–Steurer (FOCS 2010).
• 2017–2018 — The 2-to-2 Games programme: Khot–Minzer–Safra (STOC 2017; ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (STOC 2018; ToC 2025), Barak–Kothari–Steurer's shortcode formulation (ITCS 2019), and the Grassmann expansion theorem of Khot–Minzer–Safra (Annals 2023). Together these give NP-hardness of Unique Games with completeness near $1/2$ and arbitrarily small soundness.
• 2026 — The OpenAI preprint claims completeness arbitrarily close to $1$, i.e. the full conjecture (Theorem 1.1, p. 2).

Setting

Fix a finite alphabet $K$. An instance $G$ has a finite vertex set and a nonempty list of oriented constraints $e=(u_e,v_e,\pi_e)$ with $\pi_e$ a permutation of $K$; repeated list entries count with multiplicity, and no weights are allowed. A labeling $a$ assigns a label to every vertex and satisfies $e$ when $a(v_e)=\pi_e(a(u_e))$. The value of $a$ is the fraction of satisfied constraints and $\mathrm{val}(G)$ is the maximum over labelings.

An instance is simple bipartite if its vertices split into two sides, every constraint goes from the first side to the second, and no two list entries join the same ordered pair. It is a translation instance over $K=\mathbb F_2^s$ if every constraint has the form $a(v_e)=a(u_e)+c_e$.

3SAT inputs are bit strings decoding to a conjunction of clauses with exactly three literal slots (repeated variables and literals allowed); the input is a YES instance when it decodes to a satisfiable formula.

Formalization targets

Goal: the Unique Games Theorem (Theorem 1.1, p. 2)

For every $\varepsilon,\delta\in(0,1/2)$ there exist $s\ge1$ and a deterministic polynomial-time map $\varphi\mapsto G_\varphi$ to simple bipartite translation instances over $\mathbb F_2^s$ such that

$$\varphi\in\mathrm{3SAT}\;\Longrightarrow\;\mathrm{val}(G_\varphi)\ge 1-\varepsilon,\qquad \varphi\notin\mathrm{3SAT}\;\Longrightarrow\;\mathrm{val}(G_\varphi)\le \delta .$$

The alphabet, the program and the running-time polynomial depend only on $(\varepsilon,\delta)$; the two errors are chosen independently, before the alphabet. In Lean this is OAI.UniqueGamesTheorem.theorem11, which asserts that the structure BinaryGapReduction ε δ is inhabited.

Significance

The result itself. The conjecture is the hypothesis behind a large body of tight approximation thresholds; the preprint's Section 8 (pp. 39–43) records how Theorem 1.1 feeds the earlier reductions for Max-Cut, Vertex Cover, Raghavendra's CSP theorem, ordering CSPs, multicut/sparsest cut and correlation clustering. Those reductions and thresholds are due to their original authors. The statement also fixes the conjecture's quantifier order (errors first, then alphabet), which is exactly what the known algorithms above do not contradict.

Formalizing it. No machine-checked proof of the UGC, or of the 2-to-2 theorem it builds on, is known to exist. A complete development would have to formalize Håstad's parity gap, classical parallel repetition for projection games, the Khot–Minzer–Safra Grassmann/shortcode inverse theorem (used as an external input via Theorem 5.1, p. 22 of the preprint), and the preprint's new latent-alphabet gadget and matrix test. Each of these is reusable well beyond this mission.

Difficulty

The central obstacle, identified in the preprint's introduction (pp. 2–4), is completeness: in a unique constraint every label permits exactly one reply, so the natural codeword tests lose a constant fraction of constraints even on honest proofs. For example, on the rank-one matrix shortcode the evaluation $M\mapsto Mz$ is preserved by a random rank-one update only with probability about $1/2$. The 2-to-2 theorem gives soundness but only near-$1/2$ completeness, and pushing completeness to $1-\varepsilon$ while keeping soundness $\delta$ independent of the alphabet is a separate problem that the earlier programme left open.

Formalization scope

• Instances are Foundations.Target.Instance q over alphabet Fin q, with constraints given by explicit forward/inverse permutation tables and a nonemptiness proof; the value is countSatisfied / constraints.length in ℝ, so division by zero cannot occur.
• The reduction is a Turing.TM2ComputableInPolyTime program from raw input bits (identity encoding, so runtime is measured in the raw input length including sparse variable names) to the bit encoding gameBits; its tape alphabets must be finite.
• coordinates : Fin alphabet ≃ (Fin s → ZMod 2) fixes the $\mathbb F_2^s$ structure, and translations requires every constraint to be a translation in these coordinates; simpleBipartite gives the orientation and the no-parallel-edge condition on list positions.
• The 3SAT language is BinaryLanguage.language: inputs that decode (canonically) to a satisfiable three-slot formula. Malformed inputs are NO instances and must be mapped to low-value games.
• The hypotheses $0<\varepsilon,\delta<1/2$ are satisfiable and the conclusion is a data-carrying structure, so there is no vacuous reading; the completeness clause requires an actual labeling, and soundness quantifies over all labelings.

Welcome contributions: a reusable Lean library for PCP-style gap reductions on TM2 machines, Fourier analysis over $\mathbb F_2^n$, parallel repetition for projection games, and the Grassmann expansion theorem.

Selected references

• OpenAI, The Unique Games Theorem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Unique-Games-Theorem-September-23-2026/paper.pdf
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017
• S. Khot, On the Unique Games Conjecture, CCC 2010. https://doi.org/10.1109/CCC.2010.19
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
• S. Khot, O. Regev, Vertex cover might be hard to approximate to within 2−ε, J. Comput. Syst. Sci. 74 (2008). https://doi.org/10.1016/j.jcss.2007.06.019
• P. Raghavendra, Optimal algorithms and inapproximability results for every CSP?, STOC 2008. https://doi.org/10.1145/1374376.1374414
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• B. Barak, P. Kothari, D. Steurer, Small-set expansion in shortcode graph and the 2-to-2 conjecture, ITCS 2019. https://doi.org/10.4230/LIPIcs.ITCS.2019.9
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• S. Arora, B. Barak, D. Steurer, Subexponential algorithms for Unique Games and related problems, FOCS 2010. https://doi.org/10.1109/FOCS.2010.59

Motivation

Edit distance $\mathrm{ED}(x,y)$, the least number of single-symbol insertions, deletions and substitutions turning $x$ into $y$, is the standard distance on strings. Embedding strings into $\ell_1$ with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for $\ell_1$, so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.

This preprint gives two independent constructions of binary word sets whose least $\ell_1$ distortion is $\exp(\Omega(\sqrt{\log d\log\log d}))$, two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.

Background

• 1966, 1974. Levenshtein introduces insertion/deletion codes; Wagner and Fischer describe alignments by increasing traces.
• 1995. Linial, London and Rabinovich develop finite metric embeddings into $\ell_1$.
• 1999. Schulman and Zuckerman construct asymptotically good codes for insertions and deletions.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary sets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove a $(\log d)^{1/2 - o(1)}$ lower bound by Fourier analysis of cuts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for fixed-length binary strings.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound.
• 2026. The OpenAI preprint Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance (dated September 27, 2026), a companion to Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, proves the results below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ with $|\Sigma| \ge 2$ and an integer $d \ge 1$, let $\Sigma^{\le d}$ be the words of length at most $d$, including the empty word. For an injective $f : \Sigma^{\le d} \to \ell_1$,

$$\mathrm{dist}(f) = \Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big), \qquad E_\Sigma(d) = \inf_f \mathrm{dist}(f).$$

The longest common subsequence $\mathrm{LCS}(x,y)$ and the deficit $r_L(x,y) = L - \mathrm{LCS}(x,y)$ for words of length $L$ are used in the coding results. A binary substitution $c : \Sigma \to \{0,1\}^w$ replaces each letter by a codeword.

In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most $d$, and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.

Formalization targets

Goal: finiteCircle_fullMain

The conjunction of the paper's main statements, with common absolute constants:

• Theorem 1.1. For $d \ge d_0$ and every finite $\Sigma$ with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\log\log d}\big),$$

and the same bounds for $\sup_{|\Sigma| \ge 2} E_\Sigma(d)$.

• Lower constructions (Sections 5–7): for each $d \ge d_0$, both the mask construction and the excluded-prime construction, encoded in binary, give a set of words of one common length $n \le d$ with least distortion at least $\exp(c\sqrt{\log d\log\log d})$.
• Theorem 4.1 (two binary substitutions): for every alphabet of $A \ge 2$ letters there are codes $c : \Sigma \to \{0,1\}^w$ with $w = O(\log 2A)$ and $a\,w\,r_L(x,y) \le r_{wL}(c(x),c(y)) \le w\,r_L(x,y)$ for equal-length words, $\mathrm{ED}(c(x),c(y)) \le w\,\mathrm{ED}(x,y)$, plus the local separation property each construction needs.
• Theorem 8.1 (uniform upper bound): a deterministic finite-dimensional map $F$ with $\mathrm{ED}(x,y) \le \|F(x)-F(y)\|_1 \le \exp(C\sqrt{\log d\log\log d})\,\mathrm{ED}(x,y)$.

Significance

The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of $\log E_\Sigma(d)$ is $\sqrt{\log d\log\log d}$; this improves the previous $\Omega(\log d)$ lower bound to $\exp(\Omega(\sqrt{\log d\log\log d}))$. The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.

Difficulty

Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every $\ell_1$ image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.

Formalization scope

• Words are List α with Fintype α; the domain $\Sigma^{\le d}$ is a subtype by length; the empty word is included.
• distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into $\ell_1(\mathbb N)$; exponentScale d = sqrt(log d · log log d) with natural logarithms.
• The lower witnesses fix the paper's constructions (prime assignments MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length $n \le d$.
• UniformUpper asks for a map into Fin M → ℝ with the $\ell_1$ norm written as a finite sum.

The goal is not vacuous: a set with one element would have least distortion $0$, so witnesses must be nontrivial, and both bounds are required uniformly.

Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.

Selected references

• OpenAI, Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf
• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• L. J. Schulman, D. Zuckerman, Asymptotically good codes correcting insertions, deletions, and transpositions, IEEE Trans. Inform. Theory 45(7), 1999. https://doi.org/10.1109/18.796406
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

Motivation

Edit distance $\mathrm{ED}(x,y)$ is the least number of single-symbol insertions, deletions and substitutions transforming a string $x$ into $y$. It is the basic similarity measure for strings, but it is expensive to compute and awkward to index. A standard way around this is to embed strings into $\ell_1$ so that $\ell_1$ distances approximate edit distances; the quality of such a map is its distortion. Low-distortion embeddings give fast approximate nearest-neighbour search and sketching for edit distance, so the best possible distortion has been studied for two decades.

This preprint determines the exponential scale of the optimal distortion: for strings of length at most $d$, it is $\exp(\Theta(\sqrt{\log d\,\log\log d}))$, uniformly over finite alphabets.

Background

• 1966. Levenshtein studies codes correcting insertions, deletions and substitutions.
• 1974. Wagner and Fischer describe edit scripts through increasing traces (alignments).
• 1995. Linial, London and Rabinovich develop the geometry of finite metric embeddings into $\ell_1$.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary subsets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove an $\Omega(\sqrt{\log d/\log\log d})$ lower bound via cuts and Fourier analysis of noisy shifts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for binary strings of length $d$.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound for binary strings of length $d$.
• 2026. The OpenAI preprint Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent (dated September 27, 2026) proves a matching lower bound $\exp(\Omega(\sqrt{\log d\log\log d}))$. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ and $d \ge 1$, let $\Sigma^{\le d}$ be the set of strings of length at most $d$, including the empty string. Edit scripts may pass through strings of any length. Let $\ell_1$ be the space of absolutely summable real sequences. Define

$$E_\Sigma(d) = \inf_{f:\Sigma^{\le d}\hookrightarrow \ell_1}\Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big),$$

the infimum over injective maps with no restriction on dimension or computability.

In Lean (OAI.EditDistortion), edit x y is the least length of a Script true n x y of unit insertions, deletions and substitutions on List Alpha; L1 = lp (fun _ : ℕ => ℝ) 1; distortion ρ f is the product of the two maximal ratios for an embedding f : X ↪ L1; leastDistortion is the infimum over embeddings; E Alpha d applies this to {x : List Alpha // x.length ≤ d}; exponentScale c d = exp(c·sqrt(log d · log log d)).

Formalization targets

Goal: Theorem 1.1

There are absolute $c, C > 0$ and $d_0$ such that for every $d \ge d_0$ and every finite alphabet with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\,\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\,\log\log d}\big).$$

The lower bound is witnessed by a finite set of binary strings of one common length at most $d$, and the same two bounds hold for $\sup_{2 \le |\Sigma| < \infty} E_\Sigma(d)$.

Significance

The result. Theorem 1.1 shows that the Ostrovsky–Rabani embedding is optimal up to the constant in the exponent, closing the gap between $\Omega(\log d)$ (Krauthgamer–Rabani) and $\exp(O(\sqrt{\log d\log\log d}))$. It rules out any $\ell_1$ embedding of edit distance with distortion $\exp(o(\sqrt{\log d\log\log d}))$, which limits $\ell_1$-based approaches to approximate edit-distance search.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The upper bound relies on Ostrovsky and Rabani's fixed-length theorem (Theorem 5.1 in the preprint, taken from the literature) plus reductions proved in the preprint, so a full formalization also requires formalizing the Ostrovsky–Rabani embedding. The lower bound (Sections 2–4) is the new contribution.

Difficulty

Any lower bound must control every alignment of two strings, including matchings that cross the boundaries of the blocks used to build them, because an insertion or deletion shifts an entire suffix. Earlier Fourier-analytic arguments (Khot–Naor) and recursive constructions (Krauthgamer–Rabani) lose too much to reach the $\sqrt{\log d\log\log d}$ exponent; reaching it requires a construction whose combinatorial separation and an $\ell_1$ displacement inequality match at that scale.

Formalization scope

• Strings are List Alpha with Fintype Alpha, 2 ≤ card Alpha; the domain includes the empty string and all lengths up to $d$.
• Edit distance includes substitutions; edit is an sInf over script lengths, which is attained since scripts always exist.
• distortion uses sSup over finitely many ratios (the domain is finite), so no default values arise; leastDistortion is sInf over all injective maps into $\ell_1(\mathbb{N})$.
• BinaryWitness c d asks for a finite nonempty set of Boolean lists of common length $n \le d$ whose least distortion is at least exponentScale c d; a singleton has least distortion $0$, so the witness must be nontrivial.

The statement cannot be met trivially: both bounds are required with constants uniform in the alphabet.

Needed infrastructure: cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite abelian groups, prime-number estimates (Rosser–Schoenfeld), and the Ostrovsky–Rabani construction. Contributions toward the displacement inequality (Proposition 2.2) or the recursive construction (Proposition 3.1) are welcome.

Selected references

• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), Article 23, 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

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: a logarithmic strengthening of Brunn–Minkowski

The Brunn–Minkowski inequality $|(1-\lambda)K+\lambda L|\ge|K|^{1-\lambda}|L|^\lambda$ is a cornerstone of convex geometry, with consequences ranging from the isoperimetric inequality to concentration of measure. The $L_p$ Brunn–Minkowski theory of Firey and Lutwak replaces the Minkowski combination, whose support function is $(1-\lambda)h_K+\lambda h_L$, by a $p$-mean of support functions. As $p\downarrow0$ the $p$-mean becomes the geometric mean $h_K^{1-\lambda}h_L^{\lambda}$, giving the logarithmic combination of two bodies. In 2012 Böröczky, Lutwak, Yang and Zhang conjectured that, for origin-symmetric convex bodies, the logarithmic combination already satisfies the multiplicative Brunn–Minkowski bound. This would be a strict strengthening of the classical inequality in the symmetric case. The conjecture is equivalent to a logarithmic Minkowski inequality for cone-volume measures and, by work of Saroglou, implies the (B)-conjecture for even log-concave measures. Symmetry is essential: the inequality fails for general bodies.

Timeline

• 1962–1993 — Firey introduces $p$-means of convex bodies (Math. Scand. 10); Lutwak develops the $L_p$ Brunn–Minkowski–Firey theory (J. Differential Geom. 38).
• 2012 — Böröczky, Lutwak, Yang and Zhang pose the origin-symmetric log-Brunn–Minkowski conjecture (Problem 1.1), prove it in the plane, and show its equivalence with the logarithmic Minkowski inequality (Adv. Math.); in 2013 they characterize even cone-volume measures (J. Amer. Math. Soc. 26).
• 2015–2016 — Saroglou proves the inequality for bodies unconditional in a common basis (Geom. Dedicata) and shows that the Lebesgue case implies the same inequality for all even log-concave measures, hence the (B)-conjecture (Mathematika).
• 2017 — Colesanti, Livshyts and Marsiglietti prove a local version near Euclidean balls (J. Funct. Anal. 273).
• 2020–2022 — Chen, Huang, Li and Liu prove the global $L_p$ inequality for $p$ close to $1$ (Adv. Math. 368); Kolesnikov and Milman prove the local $L_p$ inequality for $p\ge1-cn^{-3/2}$ (Mem. AMS 277); Putterman proves local-to-global equivalence for all $p\in[0,1)$ (J. Funct. Anal. 280); Böröczky and Kalantzopoulos treat bodies with common reflection symmetries (Trans. AMS 375, 2022).
• 2023 — van Handel proves the local logarithmic inequality for origin-symmetric zonoids (GAFA Seminar).
• 2026 — An OpenAI preprint, The logarithmic Brunn–Minkowski conjecture (OpenAI Math Release, September 23, 2026), claims the conjecture for origin-symmetric convex bodies in every dimension. It has not been peer reviewed, and its proof is not formally verified.

Setting

A convex body $K\subset\mathbb R^n$ is a compact convex set with nonempty interior; it is origin-symmetric if $K=-K$, in which case $0$ is an interior point. Its support function is

$$h_K(u)=\max_{x\in K}\langle x,u\rangle ,\qquad u\in S^{n-1},$$

which is strictly positive for origin-symmetric bodies. For a positive function $f$ on the sphere, the Wulff body is

$$\mathcal W[f]=\bigcap_{u\in S^{n-1}}\{x:\langle x,u\rangle\le f(u)\}.$$

The logarithmic combination of $K,L$ with parameter $\lambda\in[0,1]$ is $\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]$. In general $h_K^{1-\lambda}h_L^{\lambda}$ is not itself a support function, which is why the Wulff body is needed. $|\cdot|$ denotes Lebesgue measure.

Formalization targets

Goal: the even logarithmic Brunn–Minkowski inequality (Theorem 1.1)

For $n\ge1$, origin-symmetric convex bodies $K,L\subset\mathbb R^n$ and $0\le\lambda\le1$,

$$\bigl|\mathcal W[h_K^{1-\lambda}h_L^{\lambda}]\bigr|\ \ge\ |K|^{1-\lambda}\,|L|^{\lambda}.$$

The goal statement is published on the platform with status Open.

Significance

The result itself. By the arithmetic–geometric mean inequality, $\mathcal W[h_K^{1-\lambda}h_L^\lambda]\subseteq(1-\lambda)K+\lambda L$, so the theorem strengthens the multiplicative Brunn–Minkowski inequality for symmetric bodies. It implies the symmetric $L_p$ Brunn–Minkowski inequality for every $0<p<1$ (Corollary 1.2 of the source), the logarithmic Minkowski inequality for cone-volume measures, and, through Saroglou's transfer, the (B)-conjecture: $t\mapsto\mu(e^tK)$ is log-concave for every even log-concave measure $\mu$ and origin-symmetric convex body $K$ (Corollary 8.1 of the source).

Formalizing it. The statement uses only Euclidean space, support functions and Lebesgue measure, all in Mathlib. The proof uses smooth approximation of polytopes, moment coordinates, a variance bound and a tensor estimate. A formal proof would put a long-standing conjecture of convex geometry on a machine-checked footing; Mathlib does not yet contain the classical Brunn–Minkowski inequality in this generality, and that would be a natural reusable milestone.

Difficulty

The classical proofs of Brunn–Minkowski (Prékopa–Leindler, mass transport) apply to Minkowski sums, but the logarithmic combination is not a Minkowski sum and $h_K^{1-\lambda}h_L^\lambda$ is not a support function, so these tools give only the weaker inclusion bound. Local (second-variation) approaches reduce the problem to a spectral gap for the Hilbert–Brunn–Minkowski operator on even functions, but local-to-global arguments had only been completed near the ball, for zonoids, or under extra symmetry. Without symmetry the inequality is false, so any argument must use the evenness of the bodies.

Formalization scope

• Space is EuclideanSpace ℝ (Fin n) with $n\ge1$; convex bodies are compact, convex, with nonempty interior; symmetry is x ∈ K ↔ -x ∈ K.
• The support function is a real sSup of $\langle x,u\rangle$ over $K$, nonempty and bounded for a convex body, so it is the true maximum. Real powers rpow are applied to positive support values (positivity follows from symmetry and nonempty interior).
• The Wulff body is the intersection of half-spaces over unit vectors $u$. Volumes are volume in ℝ≥0∞, with ℝ≥0∞-valued powers $1-\lambda$ and $\lambda$. At $\lambda\in\{0,1\}$ the inequality reduces to $|K|\le|K|$ (resp. $|L|\le|L|$), so the edge cases are consistent.
• Needed infrastructure: support functions and Wulff shapes, polytope approximation, the Prékopa–Leindler inequality, and log-concave measures. Contributions formalizing the planar case, the unconditional case (Saroglou) or Corollary 1.2 from Theorem 1.1 are welcome.

Selected references

• W. J. Firey, p-Means of convex bodies, Math. Scand. 10 (1962), 17–24. https://doi.org/10.7146/math.scand.a-10510
• E. Lutwak, The Brunn–Minkowski–Firey theory I, J. Differential Geom. 38 (1993), 131–150. https://doi.org/10.4310/jdg/1214454097
• K. J. Böröczky, E. Lutwak, D. Yang and G. Zhang, The log-Brunn–Minkowski inequality, Adv. Math. (2012). https://doi.org/10.1016/j.aim.2012.07.015
• K. J. Böröczky, E. Lutwak, D. Yang and G. Zhang, The logarithmic Minkowski problem, J. Amer. Math. Soc. 26 (2013), 831–852. https://doi.org/10.1090/S0894-0347-2012-00741-3
• C. Saroglou, Remarks on the conjectured log-Brunn–Minkowski inequality, Geom. Dedicata (2015). https://doi.org/10.1007/s10711-014-9993-z
• C. Saroglou, More on logarithmic sums of convex bodies, Mathematika (2016). https://doi.org/10.1112/S0025579316000061
• A. V. Kolesnikov and E. Milman, Local $L^p$-Brunn–Minkowski inequalities for $p<1$, Mem. Amer. Math. Soc. 277 (2022). https://doi.org/10.1090/memo/1360
• E. Putterman, Equivalence of the local and global versions of the $L^p$-Brunn–Minkowski inequality, J. Funct. Anal. 280 (2021). https://doi.org/10.1016/j.jfa.2021.108956
• R. van Handel, The local logarithmic Brunn–Minkowski inequality for zonoids, GAFA Seminar 2020–2022 (2023). https://doi.org/10.1007/978-3-031-26300-2_14
• OpenAI, The logarithmic Brunn–Minkowski conjecture, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-logarithmic-Brunn-Minkowski-conjecture-September-23-2026/paper.pdf

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: 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 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