OAI Math

All of openAI's results.

317 missions

Missions

21–40 of 317

Analysis Harmonic Analysis·Captain: wurtle

A uniform Hilbert transform estimate for Lipschitz directionsResearch Paper

Motivation

The Hilbert transform $Hf(x)=\mathrm{p.v.}\int f(x-t)\,\frac{dt}{t}$ is the basic singular integral of harmonic analysis. In the plane one can take it along a line through each point, with the direction of the line allowed to depend on the point: given a unit vector field $v:\mathbb R^2\to S^1$ , integrate $f$ along the segment through $x$ in direction $v(x)$ . Whether such directional Hilbert transforms are bounded on $L^2$ is one of the central problems connecting singular integrals, Kakeya-type geometry and time–frequency analysis. If $v$ depends on only one coordinate, the $L^2$ problem already contains Carleson's theorem on almost-everywhere convergence of Fourier series. For general fields some regularity of $v$ is necessary, and some truncation of the integration length is necessary because a field can turn.

Stein asked whether a Lipschitz field suffices when the integration length is at most a small multiple of $1/\mathrm{Lip}(v)$ . In the formulation of Lacey and Li, this is a uniform weak- $(2,2)$ conjecture. A parallel conjecture of Zygmund concerns the corresponding maximal averages.

Timeline

1966. Carleson proves almost-everywhere convergence of Fourier series of $L^2$ functions (doi:10.1007/BF02392815); the one-variable-field $L^2$ case of the directional problem reduces to this.
1987. Stein lists the Lipschitz directional Hilbert transform among problems in harmonic analysis in his ICM address (Problems in harmonic analysis related to curvature and oscillatory integrals).
1989. Bourgain proves an $L^2$ bound for the maximal averaging operator along analytic vector fields (doi:10.1017/CBO9780511662294.006).
2006. Lacey and Li prove annular weak- $(2,2)$ and strong $L^p$ , $p>2$ , bounds for directional Hilbert transforms with measurable directions (doi:10.1090/S0002-9947-06-03869-4), and a Lipschitz Kakeya maximal theorem.
2010. Lacey and Li's memoir develops the relation between maximal operators and the Hilbert-transform problem, with conditional results requiring stronger maximal estimates or $C^{1+\eta}$ fields (doi:10.1090/S0065-9266-10-00572-7).
2012. Stein and Street prove local $L^p$ bounds for singular Radon transforms associated with real-analytic maps (doi:10.1016/j.aim.2011.11.016).
2013. Bateman proves single-annulus $L^p$ estimates for fields depending on one coordinate (doi:10.4171/RMI/748); Bateman and Thiele prove strong $L^p$ bounds, $3/2<p<\infty$ , for the full transform along one-variable fields (doi:10.2140/apde.2013.6.1577).
2015–2017. Guo extends the one-variable setting to fields constant along Lipschitz curves (doi:10.2140/apde.2015.8.1263, doi:10.1090/tran/6750) and proves single-annulus variation-norm bounds for Lipschitz fields; Guo and Thiele treat a lacunary model of Lipschitz fields (doi:10.1112/S0025579316000280).
2018. Di Plinio and Parissis extend the lacunary framework (doi:10.1007/s11856-018-1724-y); Di Plinio, Guo, Thiele and Zorin-Kranich show that uniform $L^2$ bounds on vertical frequency bands imply the full short principal-value bound under a small Lipschitz condition (doi:10.1016/j.jfa.2018.07.005).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims the uniform strong $L^2$ bound at short scale for every Lipschitz field.

Setting

Let $v:\mathbb R^2\to S^1$ be Lipschitz with $\mathrm{Lip}(v)\le1$ . For $0<\varepsilon<a$ the short directional Hilbert transform is

H^{\varepsilon}_{v,a}f(x)=\int_{\varepsilon<|t|<a} f\bigl(x-t\,v(x)\bigr)\,\frac{dt}{t}.

The direction is frozen at the output point $x$ . For a Schwartz function $f$ the principal value $H_{v,a}f=\lim_{\varepsilon\downarrow0}H^\varepsilon_{v,a}f$ exists at every point, since $f(x-tv(x))-f(x+tv(x))=O_x(|t|)$ .

Formalization targets

Goal: Theorem 1.1

There are absolute constants $a_*\in(0,1/2)$ and $C_*<\infty$ such that every unit field $v$ with $\mathrm{Lip}(v)\le1$ satisfies, for all $f\in\mathcal S(\mathbb R^2)$ ,

\sup_{0<\varepsilon<a_*}\|H^{\varepsilon}_{v,a_*}f\|_{L^2}\le C_*\|f\|_{L^2},\qquad \|H_{v,a_*}f\|_2\le C_*\|f\|_2,

\bigl|\{x:|H_{v,a_*}f(x)|>\lambda\}\bigr|\le C_*^2\lambda^{-2}\|f\|_2^2\qquad(\lambda>0),

and the truncations and the principal value extend to bounded operators on $L^2$ with norm at most $C_*$ . The constants $a_*$ and $C_*$ are existential; no numerical value is fixed. The Lean statement OAI.LipschitzHilbert.main is open on the platform.

The proposal also contains OAI.LipschitzHilbert.uniform_truncation, the rescaled form for $K$ -Lipschitz fields at every outer length $R\le 1/(10^6K)$ . By the dilation $x\mapsto Kx$ it is the same estimate at the reciprocal-Lipschitz scale; its explicit constant $10^{-6}$ is a convention of the formalization, not of the paper.

Significance

The theorem answers the short-scale form of Stein's question affirmatively and with a strong (not only weak-type) $L^2$ bound, for fields depending on both coordinates and with no regularity beyond Lipschitz. Earlier unconditional results required the field to depend on one variable, to be constant along a foliation, to be analytic, to take lacunary directions, or restricted the frequency to one annulus. The uniformity in the inner truncation is an operator bound for each truncation, which is what the principal value and the weak-type bound are derived from.

The result is claimed in an OpenAI preprint of 87 pages; it has not been peer reviewed and no machine-checked proof exists. The Lean goal records the complete short-scale conclusion; a formal proof would certify a long chain of time–frequency arguments (wave-packet decompositions, size and density selection, a Lipschitz Kakeya input, and a phase-gain iteration).

Difficulty

Restricting to short scales limits how far the field turns but does not make the operator a Fourier multiplier: the line of integration still varies with the output point. Positive (maximal) operator bounds lose all oscillation, while the one-variable reduction to Carleson's theorem is unavailable when $v$ depends on both coordinates. The known band-to-full reassembly reduces matters to one vertical frequency band, but on a band one needs a restricted estimate with a logarithmic gain in the ratio of the measures of the input and test sets; the Lacey–Li Kakeya estimate only provides a polynomial loss in that ratio, so an additional oscillatory saving is required.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2); inputs are SchwartzMap Plane ℂ, norms are eLpNorm _ 2 volume in ℝ≥0∞.
The field is v : Plane → Plane with LipschitzWith 1 v and ‖v x‖ = 1 for all x.
twoSidedTruncation v ε a f x is the sum of interval integrals over $[-a,-\varepsilon]$ and $[\varepsilon,a]$ of $t^{-1}f(x-tv(x))$ ; smoothPrincipalValue integrates the symmetric quotient over $(0,a)$ , with the removable value at $t=0$ filled by the derivative.
ShortHilbertConclusion a C bundles the five clauses (truncation bound for $0<\varepsilon<a$ , principal-value bound, weak-(2,2) bound at every finite nonzero level, and bounded Lp extensions agreeing a.e. on Schwartz inputs). The goal asks for $a\in(0,1/2)$ and $C>0$ .

A complete development needs singular-integral and Littlewood–Paley machinery on $\mathbb R^2$ , wave-packet analysis and a Lipschitz Kakeya maximal estimate; much of this is reusable for other time–frequency problems. Contributions formalizing the band-restricted estimate, the band-to-full reassembly, or the one-dimensional inputs (the maximal truncated Hilbert transform) are welcome.

Selected references

OpenAI, A uniform Hilbert transform estimate for Lipschitz directions, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026/main.pdf
M. Lacey, X. Li, On a conjecture of E. M. Stein on the Hilbert transform on vector fields, Mem. Amer. Math. Soc., 2010. https://doi.org/10.1090/S0065-9266-10-00572-7
M. T. Lacey, X. Li, Maximal theorems for the directional Hilbert transform on the plane, Trans. Amer. Math. Soc., 2006. https://doi.org/10.1090/S0002-9947-06-03869-4
M. Bateman, C. Thiele, $L^p$ estimates for the Hilbert transforms along a one-variable vector field, Anal. PDE, 2013. https://doi.org/10.2140/apde.2013.6.1577
F. Di Plinio, S. Guo, C. Thiele, P. Zorin-Kranich, Square functions for bi-Lipschitz maps and directional operators, J. Funct. Anal., 2018. https://doi.org/10.1016/j.jfa.2018.07.005
S. Guo, C. Thiele, Hilbert transforms along Lipschitz direction fields: a lacunary model, Mathematika, 2017. https://doi.org/10.1112/S0025579316000280
E. M. Stein, B. Street, Multi-parameter singular Radon transforms III: real analytic surfaces, Adv. Math., 2012. https://doi.org/10.1016/j.aim.2011.11.016
L. Carleson, On convergence and growth of partial sums of Fourier series, Acta Math., 1966. https://doi.org/10.1007/BF02392815

3 thms1 active userReviewed

Completed

Analysis Harmonic Analysis·Captain: wurtle

An Endpoint Gradient Bound for the Centered Disk Maximal OperatorResearch Paper

Motivation

The Hardy–Littlewood maximal function replaces a function by the largest of its averages around each point. It is the basic tool for differentiation theorems and singular integrals, and it is bounded on $L^p$ for $p>1$ but not on $L^1$ . Kinnunen showed that it also preserves first-order Sobolev regularity: it is bounded on $W^{1,p}(\mathbb R^n)$ for $1<p<\infty$ , because $|\nabla Mf|\le M|\nabla f|$ pointwise (Kinnunen 1997). At $p=1$ this argument breaks, since $M$ is unbounded on $L^1$ . Hajłasz and Onninen asked whether the gradient estimate $\|\nabla Mf\|_1\le C\|\nabla f\|_1$ nevertheless holds (Question 1 in Ann. Acad. Sci. Fenn. Math. 2004). The question is a test of whether maximal operators improve or destroy regularity at the endpoint, where the usual $L^p$ machinery is unavailable.

This mission asks for a formal proof of the planar centered-disk case, as stated in an OpenAI preprint dated September 26, 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

1997 — Kinnunen: $M$ is bounded on $W^{1,p}$ , $1<p<\infty$ (Israel J. Math. 1997).
2002–2007 — In one dimension, Tanaka proves an $L^1$ derivative bound for the uncentered operator (Bull. Austral. Math. Soc. 2002); Aldaz and Pérez Lázaro obtain the sharp variation constant and absolute continuity (Trans. AMS 2007).
2004 — Hajłasz and Onninen pose the endpoint question.
2009 — Aldaz and Pérez Lázaro treat block-decreasing inputs in higher dimensions (Studia Math. 2009).
2015 — Kurka proves a variation bound for the one-dimensional centered operator (Ann. Acad. Sci. Fenn. Math. 2015).
2018 — Luiro proves the $L^1$ gradient estimate for radial inputs and the uncentered ball operator (Ark. Mat. 2018).
2020–2025 — Beltran–Madrid and Weigt treat fractional centered operators (JFA 2020; Math. Z. 2022); Weigt proves variation bounds for dyadic and uncentered-cube maximal operators (IMRN 2023; JEMS 2025); Lahti and Weigt show that a variation bound for the centered operator upgrades to Sobolev regularity (arXiv:2510.01936).
September 2026 — The OpenAI preprint claims the planar centered-disk endpoint bound (Theorem 1.1, p. 1).

Setting

Identify $\mathbb R^2$ with the Euclidean plane and write $B(x,r)$ for the open disk of radius $r$ centered at $x$ . For a locally integrable real function $f$ , the centered disk maximal function is

Mf(x)=\sup_{r>0}\frac1{\pi r^2}\int_{B(x,r)}|f(y)|\,dy\in[0,\infty].

The space $W^{1,1}(\mathbb R^2)$ consists of integrable $f$ whose distributional gradient is represented by an integrable vector field $\nabla f$ , i.e. $\int f\,\partial_i\varphi=-\int(\nabla f)_i\varphi$ for all $\varphi\in C_c^\infty$ . Norms of gradients are Euclidean: $\|\nabla f\|_1=\int|\nabla f|$ . For the signed estimate, put $A_tg(x)=\frac1{\pi t^2}\int_{B(x,t)}g$ and $S_{a,b}g(x)=\sup_{a\le t\le b}A_tg(x)$ .

Formalization targets

Milestone: Proposition 1.2 (signed finite-band estimate, p. 2)

There is an absolute constant $C$ such that for every real $g\in C_c^\infty(\mathbb R^2)$ and $0<a\le b$ with $b/a$ a power of two (including $1$ ),

\int_{\mathbb R^2}|\nabla S_{a,b}g|\,dx\le C\int_{\mathbb R^2}|\nabla g|\,dx,

with $C$ independent of $a$ , $b$ and the number of dyadic scales.

Goal: Theorem 1.1 (p. 1)

There is an absolute constant $C<\infty$ such that for every real $f\in W^{1,1}(\mathbb R^2)$ , $Mf$ is finite almost everywhere, locally integrable, belongs to $W^{1,1}_{\mathrm{loc}}(\mathbb R^2)$ , and has a globally integrable weak gradient with

\int_{\mathbb R^2}|\nabla Mf|\,dx\le C\int_{\mathbb R^2}|\nabla f|\,dx.

Significance

The result itself. It resolves the planar centered-disk case of the Hajłasz–Onninen question with no radiality or support assumption. As a consequence (Corollary 6.3, p. 39) the bound extends to $BV(\mathbb R^2)$ inputs and yields a co-area type perimeter bound for level sets of $M\mathbf 1_E$ . The constant is absolute but not optimized. Higher dimensions, other centered maximal operators, and continuity of $f\mapsto\nabla Mf$ in $W^{1,1}$ remain separate questions.

Formalizing it. Mathlib has Lebesgue integration, weak derivatives only in limited form, and no maximal-function regularity theory. A formal proof would need distributional gradients, Poincaré inequalities on squares, dyadic multiscale decompositions and a vector-measure representation of bounded distributional derivatives (the preprint's Appendix A). These pieces are reusable across harmonic analysis.

Difficulty

For $p>1$ one bounds $|\nabla Mf|\le M|\nabla f|$ and uses the strong maximal inequality, which fails for $p=1$ . One-dimensional proofs order the optimizing intervals, and that ordering has no analogue for families of centered disks. Fractional-order proofs use that optimizing balls overlap little, a mechanism that degenerates at order zero. The preprint (Sections 2–5) instead proves the signed finite-band estimate uniformly in the number of scales: it uses a vanishing first moment at interior maximizing radii, a concentration-in-a-thin-shell lemma (Lemma 2.4, p. 8), and two multiscale constructions that pay for direction changes in scale and space. A variation bound alone would leave a possibly singular derivative measure; removing the singular part needs the signed form of Proposition 1.2 applied to locally mean-subtracted inputs (Section 6).

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). maximal f x is an ℝ≥0∞-valued supremum over all real $r>0$ of lower Lebesgue integrals of $|f|$ over Metric.ball x r divided by $\pi r^2$ ; the goal asserts it is finite a.e. before passing to maximalReal = toReal.
HasWeakGradient f g is the integration-by-parts identity against every $C^\infty$ compactly supported test function, coordinatewise; the input is Integrable f, Integrable g, HasWeakGradient f g, which is exactly $W^{1,1}$ with weak gradient g. The bound is stated against this g, so it does not depend on a choice of representative.
InW11Loc asks for local integrability and a locally integrable weak gradient; the goal also asks for one integrable weak gradient G with ∫ ‖G‖ ≤ C * ∫ ‖g‖, C ≥ 0 chosen before f.
The milestone uses signed averages (Bochner integrals) and sSup over the closed radius band $[a,2^ma]$ ; the band envelope is continuous in $r$ , so the supremum is finite. Inputs are ContDiff ℝ ∞ with compact support.
The BV extension (Corollary 6.3) is not part of either target.

Selected references

OpenAI, An Endpoint Gradient Bound for the Centered Disk Maximal Operator, OpenAI Math Release preprint, September 26, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-Endpoint-Gradient-Bound-for-the-Centered-Disk-Maximal-Operator-September-26-2026/article.pdf
J. Kinnunen, The Hardy–Littlewood maximal function of a Sobolev function, Israel J. Math. (1997). https://doi.org/10.1007/BF02773636
P. Hajłasz, J. Onninen, On boundedness of maximal functions in Sobolev spaces, Ann. Acad. Sci. Fenn. Math. (2004). https://afm.journal.fi/article/view/135096
H. Tanaka, A remark on the derivative of the one-dimensional Hardy–Littlewood maximal function, Bull. Austral. Math. Soc. (2002). https://doi.org/10.1017/S0004972700020293
J. M. Aldaz, J. Pérez Lázaro, Functions of bounded variation, the derivative of the one dimensional maximal function, and applications to inequalities, Trans. AMS (2007). https://doi.org/10.1090/S0002-9947-06-04347-9
O. Kurka, On the variation of the Hardy–Littlewood maximal function, Ann. Acad. Sci. Fenn. Math. (2015). https://doi.org/10.5186/aasfm.2015.4003
H. Luiro, The variation of the maximal function of a radial function, Ark. Mat. (2018). https://doi.org/10.4310/ARKIV.2018.v56.n1.a9
J. Weigt, The variation of the uncentered maximal operator with respect to cubes, J. Eur. Math. Soc. (2025). https://doi.org/10.4171/JEMS/1575
P. Lahti, J. Weigt, The centered maximal operator removes the non-concave Cantor part from the gradient, arXiv:2510.01936 (2025). https://arxiv.org/abs/2510.01936v1

8 thms2 active usersReviewed

Discrete Geometry Functional Analysis·Captain: wurtle

The Mahler Conjecture for General Convex BodiesResearch Paper

Motivation

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

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

Timeline

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

Setting

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

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

and the volume product is

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

2 thms1 active userReviewed

Completed

Discrete Geometry Symplectic Geometry·Captain: wurtle

Symplectic Balls in Symmetric Polar ProductsResearch Paper

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

8 thms2 active usersReviewed

Completed

Analysis Discrete Geometry·Captain: wurtle

Petty’s projection-volume conjecture in dimensions at least fourResearch Paper

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

8 thms2 active usersReviewed

Completed

Discrete Geometry·Captain: wurtle

A product counterexample to the simplex maximum for projection-body volumeResearch Paper

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

52 thms2 active usersReviewed

Discrete Geometry Graph Theory Theoretical Computer Science·Captain: wurtle

Planar Graph Metrics Embed into L1 with Constant DistortionResearch Paper

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

2 thms1 active userReviewed

Completed

Discrete Geometry Graph Theory Theoretical Computer Science·Captain: wurtle

L1 Embeddings of Graphs of Bounded TreewidthResearch Paper

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

2 thms2 active usersReviewed

Discrete Geometry Harmonic Analysis Mathematical Physics·Captain: wurtle

An atomic certificate for triangular-lattice universal optimalityResearch Paper

Motivation

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

Timeline

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

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

Setting

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

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

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

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

Formalization targets

Milestone: Theorem 1.2 (sharp Gaussian minorants)

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

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

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

Goal: Theorem 1.1 (universal energy minimum)

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

2 thms1 active userReviewed

Discrete Geometry Harmonic Analysis·Captain: wurtle

A sharp Fourier certificate for planar circle packingResearch Paper

Motivation

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

Timeline

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

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1.1 (sharp Fourier certificate)

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

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

Lean: OAI.sharp_fourier_certificate, open on the platform.

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

2 thms1 active userReviewed

Analysis Discrete Geometry·Captain: wurtle

The logarithmic Brunn–Minkowski conjectureResearch Paper

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

2 thms1 active userReviewed

Completed

Discrete Geometry Functional Analysis Probability·Captain: wurtle

Subpolynomial dimension reduction in LpResearch Paper

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

2 thms2 active usersReviewed

Completed

Discrete Geometry Probability Theoretical Computer Science·Captain: wurtle

The Gaussian propeller bound in every dimensionResearch Paper

Motivation

Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of $x$ against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is $9/(8\pi)$ , attained by three planar sectors of angle $2\pi/3$ (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.

This mission asks for a formal proof of the propeller bound in every dimension, 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

1983–2003 — The Gaussian Minkowski (Ehrhard) inequality: Ehrhard for convex sets (Math. Scand. 1983), Latała when one set is convex (Studia Math. 1996), Borell for Borel sets (C. R. Acad. Sci. 2003); later van Handel's game proof (PTRF 2018).
2009 — Khot and Naor introduce the problem, reduce maximizers to conical partitions in the span of their centroids, and compute the three-cell value (Mathematika 2009); see also their sharp kernel-clustering paper (RSA 2013).
2013 — Heilman, Jagannath and Naor prove the conjecture in $\mathbb R^3$ with a computer-assisted argument (DCG 2013).
2022 — Heilman gives a conditional route for three or four cells in any dimension, under a stability hypothesis on noise-stability maximizers (arXiv:2209.11216).
September 2026 — The OpenAI preprint claims the bound for every dimension and every number of cells (Theorem 1.1, p. 1).

Setting

Let $\gamma_d$ be the standard Gaussian probability measure on $\mathbb R^d$ , with density $(2\pi)^{-d/2}e^{-\|x\|^2/2}$ . For a measurable set $A\subseteq\mathbb R^d$ , its centroid is the unnormalized vector

z(A)=\int_A x\,d\gamma_d(x)\in\mathbb R^d .

A measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$ consists of measurable sets such that almost every point (for $\gamma_d$ ) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is $F(A)=\sum_{i=1}^k\|z(A_i)\|^2$ . The propeller is the partition of $\mathbb R^d$ , $d\ge2$ , into the three sets $S_j\times\mathbb R^{d-2}$ , where $S_1,S_2,S_3$ are the planar sectors of opening $2\pi/3$ bounded by the rays at angles $\pm\pi/3$ and $\pi$ , with any further cells empty.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For all positive integers $d,k$ and every measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$ ,

\sum_{i=1}^k\Bigl\|\int_{A_i}x\,d\gamma_d(x)\Bigr\|^2\ \le\ \frac{9}{8\pi},

and for $d\ge2$ , $k\ge3$ the propeller is a measurable partition attaining equality.

Significance

The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant $9/(8\pi)$ fixes the loss factor $\alpha_k=\frac{8\pi}{9}(1-\frac1k)$ of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).

Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.

Difficulty

The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose $m$ nonzero centroids span an $(m-1)$ -dimensional space, so the three-dimensional theorem disposes of $m\le4$ active cells. The remaining cases $m\ge5$ cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.

Formalization scope

Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.
centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.
The goal is a conjunction: the bound for all $d,k\ge1$ , and, for $d\ge2$ , $k\ge3$ , that the explicit three-sector propeller d k (cells $\ge3$ empty) is a partition with value exactly $9/(8\pi)$ . The sectors are written with closed inequalities, so they overlap only on null rays.
No hypothesis is vacuous: the case $k=1$ is included (value $0$ ), and the equality clause pins the constant.

Selected references

OpenAI, The Gaussian propeller bound in every dimension, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf
S. Khot, A. Naor, Approximate kernel clustering, Mathematika 55 (2009), 129–165. https://doi.org/10.1112/S002557930000098X
S. Khot, A. Naor, Sharp kernel clustering algorithms and their associated Grothendieck inequalities, Random Struct. Algorithms 42 (2013), 269–300. https://doi.org/10.1002/rsa.20398
S. Heilman, A. Jagannath, A. Naor, Solution of the Propeller Conjecture in $\mathbb R^3$ , Discrete Comput. Geom. 50 (2013), 263–305. https://doi.org/10.1007/s00454-013-9530-0
S. Heilman, Hyperstable sets with voting and algorithmic hardness applications, arXiv:2209.11216 (2022). https://arxiv.org/abs/2209.11216v1
A. Ehrhard, Symétrisation dans l'espace de Gauss, Math. Scand. 53 (1983), 281–301. https://doi.org/10.7146/math.scand.a-12035
R. Latała, A note on the Ehrhard inequality, Studia Math. 118 (1996), 169–174. https://doi.org/10.4064/sm-118-2-169-174
C. Borell, The Ehrhard inequality, C. R. Acad. Sci. Paris 337 (2003), 663–666. https://doi.org/10.1016/j.crma.2003.09.031
R. van Handel, The Borell–Ehrhard game, Probab. Theory Relat. Fields 170 (2018), 555–585. https://doi.org/10.1007/s00440-017-0762-4
E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010), 295–341. https://doi.org/10.4007/annals.2010.171.295

57 thms5 active usersReviewed

Completed

Combinatorics Discrete Geometry Theoretical Computer Science·Captain: wurtle

The Euclidean Steinitz–Bergström theoremResearch Paper

Motivation: keeping partial sums of vectors small

Given vectors $v_1,\dots,v_N$ in the Euclidean unit ball of $\mathbb R^d$ that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on $d$ ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius $d$ suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is $O(\sqrt d)$ , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs $\varepsilon_i\in\{\pm1\}$ , chosen once and for all, such that every signed prefix $\sum_{i\le k}\varepsilon_iv_i$ is $O(\sqrt d)$ , independently of $N$ . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.

Timeline

1913 — Steinitz proves his rearrangement lemma for conditionally convergent vector series (historical account in Ambrus–Heck 2026, Section 2).
1954 — Behrend discusses the expected square-root growth in Euclidean space (Canad. J. Math., p. 108).
1980 — Grinberg and Sevast'yanov prove that partial sums can be kept within $d$ times the unit ball, for every norm (Funct. Anal. Appl.).
1994–2023 — Chobanyan's transference principle relates rearrangements to signed sums (Probability in Banach Spaces 9, 1994), later in a finite positive-forward, negative-reverse form (Chobanyan et al., Bull. TICMI 2023).
1998 / 2012 — Banaszczyk's Gaussian-measure balancing theorem (Random Structures Algorithms 1998) and his prefix bound $O(\sqrt d+\sqrt{\log N})$ for signed series and rearrangements (Random Structures Algorithms 2012).
2021 — Bansal, Jiang, Meka, Singla and Sinha state the $O(\sqrt d)$ prefix-signing question explicitly (Conjecture 6.3, arXiv:2111.07049).
2026 — Ambrus and Heck record the conjecture and its attribution to Bergström (Conjecture 5) and reduce it to a relaxed problem (Mathematika); Dutta, Jha and Jiang give efficient bounds $O(\sqrt d+d^{1/4}\log^{7/4}N)$ (arXiv:2604.13355).
2026 — An OpenAI preprint, The Euclidean Steinitz–Bergström theorem (OpenAI Math Release, September 24, 2026), claims the $O(\sqrt d)$ bound for both problems with an absolute constant. It has not been peer reviewed, and its proof is not formally verified.

Setting

Work in Euclidean space $\mathbb R^d$ with norm $\|\cdot\|_2$ , and let $v_1,\dots,v_N$ satisfy $\|v_i\|_2\le1$ ; repetitions and zero vectors are allowed. A prefix sum is $\sum_{i=1}^k$ for $0\le k\le N$ (the empty sum is $0$ ). For a zero-sum family, the Steinitz quantity

\beta(v_1,\dots,v_N)=\min_{\pi\in\mathfrak S_N}\ \max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2

is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant $S_2(d)$ is its supremum over all such families.

Formalization targets

Goal: prescribed-order signing and Euclidean Steinitz with one absolute constant (Theorems 1.1 and 1.2)

There is an absolute constant $C$ such that for all $d,N\ge1$ and all $v_1,\dots,v_N\in\mathbb R^d$ with $\|v_i\|_2\le1$ :

(Theorem 1.1) there are signs $\varepsilon_i\in\{-1,1\}$ with

\max_{0\le k\le N}\Bigl\|\sum_{i=1}^k\varepsilon_iv_i\Bigr\|_2\le C\sqrt d ;

(Theorem 1.2) if moreover $\sum_iv_i=0$ , some permutation $\pi$ satisfies

\max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2\le C\sqrt d .

The constant is not fixed. The simplex example in the source shows $S_2(d)\ge\tfrac12\sqrt d$ , so the order is optimal. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: $S_2(d)=\Theta(\sqrt d)$ . Theorem 1.1 settles the $\ell_2$ prefix-discrepancy question of Bansal et al., removing the $\sqrt{\log N}$ term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional $\ell_p$ Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.

Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.

Difficulty

Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all $N$ prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a $\sqrt{\log N}$ factor, because the probability that a random walk stays in a ball of radius $C\sqrt d$ for $N$ steps decays with $N$ . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), indexed by Fin N, with $d,N\ge1$ and $\|v_i\|\le1$ .
Prefixes are sums over $\{i : i < k\}$ for every natural $k\le N$ , so the empty prefix and the full sum are included.
SignedPrefixBound C asks for signs $\varepsilon_i\in\{-1,1\}$ (as reals) with every signed prefix at most $C\sqrt d$ . OrderingPrefixBound C asks, for zero-sum families, for a permutation $\pi$ with every reordered prefix at most $C\sqrt d$ . The goal is $\exists C,\ \mathrm{SignedPrefixBound}\,C\wedge\mathrm{OrderingPrefixBound}\,C$ ; the same constant serves both, as stated in the source.
The quantifier order is the source's: $C$ is chosen before $d$ , $N$ and the vectors.
Needed infrastructure: Gaussian measures of symmetric convex bodies, Steiner symmetrization, Dirichlet energies of densities, Ornstein–Uhlenbeck/Brownian survival estimates, and the Chobanyan transference. Contributions proving the transference step (Theorem 1.1 ⇒ Theorem 1.2) or the lower-bound example are welcome.

Selected references

V. S. Grinberg and S. V. Sevast'yanov, Value of the Steinitz constant, Funct. Anal. Appl. (1980).
F. A. Behrend, The Steinitz–Gross theorem on sums of vectors, Canad. J. Math. (1954).
S. Chobanyan, Convergence a.s. of rearranged random series in Banach space and associated inequalities, Probability in Banach Spaces 9 (1994).
W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures Algorithms (1998).
W. Banaszczyk, On series of signed vectors and their rearrangements, Random Structures Algorithms (2012).
N. Bansal, H. Jiang, R. Meka, S. Singla and M. Sinha, Prefix discrepancy, smoothed analysis, and combinatorial vector balancing, 2021. https://arxiv.org/abs/2111.07049
G. Ambrus and R. Heck, A note on the Steinitz Lemma, Mathematika (2026). https://doi.org/10.1112/mtk.70085
K. Dutta, A. V. Jha and H. Jiang, Near-optimal constructive bounds for $\ell_2$ prefix discrepancy and Steinitz problems via affine spectral independence, 2026. https://arxiv.org/abs/2604.13355
OpenAI, The Euclidean Steinitz–Bergström theorem, OpenAI Math Release preprint, September 24, 2026 (Theorems 1.1 and 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf

9 thms4 active usersReviewed

Completed

Analysis Discrete Geometry Functional Analysis·Captain: wurtle

A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embeddingResearch Paper

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

25 thms2 active usersReviewed

Combinatorics Functional Analysis Theoretical Computer Science·Captain: wurtle

Edit Distance in l1: Matching Bounds up to Constants in the ExponentResearch Paper

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

2 thms1 active userReviewed

Completed

Combinatorics Functional Analysis Theoretical Computer Science·Captain: wurtle

Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit DistanceResearch Paper

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

54 thms2 active usersReviewed

Complexity Theory Theoretical Computer Science·Captain: wurtle

The Unique Games TheoremResearch Paper

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

2 thms1 active userReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: wurtle

A Direct Proof of Optimal Max-Cut HardnessResearch Paper

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

2 thms1 active userReviewed

Complexity Theory Graph Theory Theoretical Computer Science·Captain: wurtle

The Factor-Two Hardness Threshold for Vertex CoverResearch Paper

Motivation

A vertex cover of a graph is a set of vertices meeting every edge; $\tau(G)$ denotes the minimum size of one. Computing $\tau(G)$ exactly is NP-hard, but a two-line algorithm — take both endpoints of a maximal matching — always returns a cover of size at most $2\tau(G)$ . Whether any polynomial-time algorithm achieves a fixed factor $2-\varepsilon$ is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below $10\sqrt5-21\approx1.36$ and, after the 2-to-2 Games Theorem, below $\sqrt2$ ; factor-two hardness was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that every fixed approximation factor below two is NP-hard, as claimed in an OpenAI preprint dated September 23, 2026 (source, Corollary 1.2, p. 1). The preprint's direct reduction starts from ordinary perfect-completeness Label Cover. 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 proves Node Cover NP-complete (Karp 1972); the maximal-matching algorithm gives factor $2$ .
1992–1998 — Feige–Goldwasser–Lovász–Safra–Szegedy (JACM 1996) link proof checking to approximation; the PCP theorem (Arora–Safra, JACM 1998; Arora–Lund–Motwani–Sudan–Szegedy, JACM 1998) gives a constant gap; Raz's parallel repetition (SICOMP 1998) yields Label Cover with arbitrarily small soundness.
2001 — Håstad: NP-hard below factor $7/6$ (JACM 2001).
2005 — Dinur–Safra: NP-hard below $10\sqrt5-21\approx1.36068$ (Annals 2005).
2002–2008 — Khot's Unique Games Conjecture (STOC 2002); Khot–Regev prove factor- $(2-\varepsilon)$ hardness assuming it (JCSS 2008).
2009 — Karakostas's algorithm achieves $2-\Theta(1/\sqrt{\log n})$ (TALG 2009), a saving that vanishes with $n$ .
2017–2023 — The 2-to-2 Games programme (Khot–Minzer–Safra, ToC 2025; Dinur–Khot–Kindler–Minzer–Safra, ToC 2025; Barak–Kothari–Steurer, ITCS 2019; Khot–Minzer–Safra expansion, Annals 2023) gives NP-hardness below $\sqrt2$ .
2026 — The OpenAI preprint claims NP-hardness for every fixed factor below $2$ .

Setting

A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count $n$ and a duplicate-free list of edges $\{u,v\}$ with $u<v$ . A set $S$ of vertices is a cover if every edge has an endpoint in $S$ , and $\tau(G)$ is the least size of a cover. An $\alpha$ -approximation algorithm is a deterministic polynomial-time machine that, on every graph, outputs a duplicate-free list of vertices that covers all edges and has length at most $\alpha\,\tau(G)$ .

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses; malformed strings are NO instances. A 3SAT decider is a deterministic polynomial-time machine answering membership correctly on every input.

Formalization targets

Milestone: the explicit cover gap (Theorem 1.1, p. 1)

For every integer $m\ge4$ there is a deterministic polynomial-time reduction $\varphi\mapsto G_\varphi$ from 3SAT to explicit simple graphs with

\varphi\text{ satisfiable}\Rightarrow \tau(G_\varphi)<\Bigl(\tfrac12+\tfrac1m\Bigr)|V(G_\varphi)|,\qquad \varphi\text{ unsatisfiable}\Rightarrow \tau(G_\varphi)>\Bigl(1-\tfrac1m\Bigr)|V(G_\varphi)|.

The ratio of the thresholds is $2-6/(m+2)\to2$ . In Lean: OAI.VertexCover.explicit_cover_gap.

Goal: factor-two threshold (Corollary 1.2, p. 1)

For every real $\alpha$ with $1\le\alpha<2$ , an $\alpha$ -approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:

\forall\,\alpha\in[1,2):\quad \mathrm{Approximation}(\alpha)\;\Longrightarrow\;\mathrm{ThreeSATDecision}.

In Lean: OAI.VertexCover.every_fixed_factor_below_two. The preprint derives it from Theorem 1.1 in its final section (pp. 23–24) by choosing $m$ from $\alpha$ and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies $2$ as the approximation threshold unless P = NP.

Significance

The result itself. The statement removes the Unique Games hypothesis from the Khot–Regev theorem and closes the gap between the elementary factor- $2$ algorithm and hardness. The density gap of Theorem 1.1 is also a statement about independent sets: YES graphs have independent sets of density nearly $1/2$ , NO graphs have none of density above $1/m$ .

Formalizing it. No machine-checked proof of any super-constant Vertex Cover hardness bound is known to exist. A complete development requires the perfect-completeness Label Cover theorem (Theorem 2.1, p. 4; PCP theorem plus parallel repetition, used as an external input), the explicit graph construction and its polynomial-time implementation (Proposition 3.3, p. 7), and the preprint's analytic soundness argument. The Label Cover input and a library for polynomial-time gap reductions on TM2 machines are reusable for many other hardness missions.

Difficulty

Soundness requires extracting short lists of candidate labels from an arbitrary large independent set, where each list may depend only on its own position's query. If a list also sees the opposite endpoint of a constraint or its occurrence index, the pair-decoding argument against Label Cover soundness breaks down (Introduction, pp. 3–4). Classical approaches either need the stronger Unique Games source promise (Khot–Regev) or only reach densities near $1-1/\sqrt2$ (the 2-to-2 route), which gives factor $\sqrt2$ rather than $2$ . Averaging to impose the information restriction can erase all variance; the analytic core is retaining it without any dependence on the label alphabet sizes.

Formalization scope

Graphs are VertexCover.ExplicitGraph: n : ℕ and a Nodup list of pairs in Fin n × Fin n with e.1 < e.2; coverNumber is the least cardinality of a covering Finset (always defined since univ covers).
Encodings: inputs are raw bits; graphs are encoded by ExplicitGraph.bits (vertex count, all vertex names, edge count, edge endpoints, each with prefix-free binary framing); an approximation's output list is encoded by natListBits.
Approximation α bundles a polynomial-time TM2 program on graph encodings with finite tape alphabets, whose output is duplicate-free, in range, covers every edge and has length at most α * coverNumber. ThreeSATDecision is a polynomial-time TM2 decider correct on every input.
The goal is an implication from an algorithm to a decider: no assumption P ≠ NP is built in, and the hypothesis $1\le\alpha<2$ is satisfied by real algorithms only if 3SAT is easy, which is exactly the content. It cannot be discharged trivially because Approximation α must be correct on every graph.
The milestone's thresholds are compared in ℝ with strict inequalities as in the source.

Welcome contributions: Label Cover hardness (PCP theorem + parallel repetition), Efron–Stein decompositions and variance inequalities on product spaces, and general complexity-theoretic infrastructure for Turing.TM2ComputableInPolyTime.

Selected references

OpenAI, The Factor-Two Hardness Threshold for Vertex Cover, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026/paper.pdf
R. M. Karp, Reducibility among combinatorial problems, Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
I. Dinur, S. Safra, On the hardness of approximating minimum vertex cover, Ann. of Math. 162 (2005). https://doi.org/10.4007/annals.2005.162.439
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
G. Karakostas, A better approximation ratio for the Vertex Cover problem, ACM Trans. Algorithms (2009). https://doi.org/10.1145/1597036.1597045
R. Raz, A parallel repetition theorem, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539795280895
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
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, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

3 thms1 active userReviewed

Top contributors

Rank	Contributor	Accepted solutions	Submitted problems
1	Eyal1990	1041	1450
2	Shuze Chen	822	3136
3	dbenbenn	342	316
4	fizzyinc3	297	0
5	polylog	44	8
6	Ethan Cheung	28	15
7	WillR	21	2
8	Yuxuan Xu	17	34
9	SamenHossain	11	19
10	queelius	7	0

OAI Math

Missions

A uniform Hilbert transform estimate for Lipschitz directionsResearch Paper

Motivation

Timeline

Setting

Formalization targets

Goal: Theorem 1.1

Significance

Difficulty

Formalization scope

Selected references

An Endpoint Gradient Bound for the Centered Disk Maximal OperatorResearch Paper

Motivation

Background

Setting

Formalization targets

Milestone: Proposition 1.2 (signed finite-band estimate, p. 2)

Goal: Theorem 1.1 (p. 1)

Significance

Difficulty

Formalization scope

Selected references

The Mahler Conjecture for General Convex BodiesResearch Paper

Motivation

Timeline

Setting

Formalization targets

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

Significance

Difficulty

Formalization scope

Selected references

Symplectic Balls in Symmetric Polar ProductsResearch Paper

Motivation

Timeline

Setting

Formalization targets

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

Goal: Theorem 1.1 (p. 1)

Significance

Difficulty

Formalization scope

Selected references

Petty’s projection-volume conjecture in dimensions at least fourResearch Paper

Motivation

Background

Setting

Formalization targets

Goal: Theorem 1.1 (p. 1)

Significance

Difficulty

Formalization scope

Selected references

A product counterexample to the simplex maximum for projection-body volumeResearch Paper

Motivation

Background

Setting

Formalization targets

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

Goal: Theorem 1 (p. 2)

Significance

Difficulty

Formalization scope

Selected references

Planar Graph Metrics Embed into L1 with Constant DistortionResearch Paper

Motivation: cut metrics, flows and the planar embedding conjecture

Timeline

Setting

Formalization targets

Goal: Theorem 1.1 (planar graph metrics in L1L_1L1​)

Significance

Difficulty

Formalization scope

Selected references

L1 Embeddings of Graphs of Bounded TreewidthResearch Paper

Motivation: L1L_1L1​ embeddings, sparsest cut and the GNRS conjecture

Timeline

Setting

Formalization targets

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

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

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