All missions

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

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

Timeline

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

Setting

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

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

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

Formalization targets

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

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

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

$C_k$ is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives $\lambda_*\le\phi_*\le C_k\lambda_*$ for every multicommodity instance on graphs of treewidth less than $k$. By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum $L_1$ distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion $(2+\varepsilon)C_k$. With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation: cut metrics, flows and the planar embedding conjecture

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

Timeline

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

Setting

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

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

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

This mission asks for a formal proof of an explicit counterexample in dimension $20$, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

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

Setting

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

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

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

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

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

Formalization targets

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

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

Goal: Theorem 1 (p. 2)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

This mission asks for a formal proof of the conjecture in every dimension $n\ge4$, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

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

Setting

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

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

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

Formalization targets

Goal: Theorem 1.1 (p. 1)

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

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

This mission asks for a formal proof that it does, as claimed in an OpenAI preprint dated September 22, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

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

Setting

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

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

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

Formalization targets

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

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

Goal: Theorem 1.1 (p. 1)

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

$$c_G(U_K)=4,$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Timeline

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

Setting

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

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

and the volume product is

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

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

Formalization targets

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

The 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

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

Motivation

The Riemann mapping theorem says that every simply connected proper domain in the plane is conformally equivalent to the unit disk. For domains with more complicated complements one needs a model with many "holes". Koebe's Kreisnormierungsproblem (1908) asks whether every domain in the Riemann sphere is conformally equivalent to a circle domain, one whose complementary components are all round disks or points. Such a model would give a canonical geometric picture of an arbitrary planar domain, and it is closely tied to circle packings, Kleinian groups and the geometry of hyperbolic surfaces of genus zero.

Timeline

• 1908. Koebe poses the problem (Nachr. Ges. Wiss. Göttingen, 1908).
• 1920. Koebe's treatment of the finitely connected case (doi:10.1007/BF01199400).
• 1993. He and Schramm prove the conjecture for countably connected domains (doi:10.2307/2946541).
• 1995. Schramm introduces transboundary extremal length and treats domains bounded by points and $K$-quasicircles (doi:10.1007/BF02788827).
• 2025. Rajala shows that arbitrary interior exhaustions can fail to have circle-domain limits and proves an exhaustion refinement theorem for countably connected domains (doi:10.1353/ajm.2025.a966291); Ntalampekos and Rajala study exhaustions of circle domains (arXiv:2312.06840).
• 2026. Esmayli and Rajala prove uniformization for cospread domains and under a quasitripod condition (arXiv:2401.08485); Karafyllia and Ntalampekos treat spherical Gromov-hyperbolic domains (arXiv:2405.13782). Ntalampekos surveys the area (arXiv:2603.15098).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the conjecture in its unrestricted form.

Setting

The Riemann sphere is $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$, with local coordinate $z$ near finite points and $1/z$ near $\infty$. A domain is a nonempty connected open subset. A map $f$ is conformal at $p$ if it is continuous at $p$ and, in these coordinates, complex differentiable at $p$ with nonzero derivative. A conformal equivalence $f:U\to V$ is a bijection that is conformal at every point of $U$ and whose inverse is conformal at every point of $V$.

A closed round disk in $\widehat{\mathbb C}$ is the image of the closed unit disk under a Möbius transformation $z\mapsto (az+b)/(cz+d)$, $ad-bc\ne0$; these are closed Euclidean disks, closed half-planes together with $\infty$, and complements of open disks. A circle domain is a domain each of whose complementary connected components is a closed round disk or a single point. The complement may be empty, finite, countable or uncountable.

Formalization targets

Goal: Theorem 1.1 (circle-domain uniformization)

$$\forall\,G\subset\widehat{\mathbb C}\ \text{domain}\quad\exists\,\Omega\ \text{circle domain},\ \exists\,f:G\xrightarrow{\ \text{conformal}\ }\Omega\ \text{bijective}.$$

Lean: OAI.Problem047.koebe_circle_domain, open on the platform.

Significance

The theorem would complete the existence half of Koebe's problem with no restriction on the number, size or geometry of the complementary components. The paper derives a consequence for hyperbolic geometry (Corollary 8.1): every complete hyperbolic surface of genus zero is isometric to the boundary of the convex hull of a closed set in $\partial_\infty\mathbb H^3$ whose components are round disks or points. Combined with the exhaustion theorem of Ntalampekos and Rajala, it also gives convergent finitely connected approximations for every proper domain. Uniqueness up to Möbius maps is a different question (the He–Schramm rigidity conjecture), addressed in the companion mission on removable boundaries.

The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. Mathlib has neither the Riemann mapping theorem in full generality nor finitely connected circle-domain uniformization, so a formal proof would build substantial reusable complex-analytic infrastructure.

Difficulty

The standard approach uniformizes finitely connected approximations, whose complements are finitely many round disks, and passes to a limit. The difficulty is control at the limit: with possibly uncountably many complementary components, a limiting component can be strictly larger than the round disk obtained by following one approximating disk, or can be a non-round continuum for which no disk was followed at all. Rajala showed that arbitrary exhaustions can indeed fail to produce circle-domain limits, so the approximations must be chosen with care, and all components must be controlled simultaneously, not one at a time.

Formalization scope

• Sphere := OnePoint ℂ; Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it.
• IsConformalAt f p: ContinuousAt f p and a nonzero HasDerivAt of $f$ in the charts chart p, chart (f p) (identity coordinate at finite points, $z\mapsto1/z$ at $\infty$).
• IsConformalEquivalence f U V: $f$ conformal on $U$, MapsTo f U V, and a conformal g on $V$ with MapsTo g V U that is a two-sided inverse.
• IsCircleDomain V: open, IsConnected (hence nonempty), and every connectedComponentIn Vᶜ p is a singleton or IsRoundClosedDisk (a Möbius image of the closed unit disk).
• The goal quantifies over all open connected U; there is no countability or regularity assumption on the complement.

A complete development needs finitely connected uniformization, normal families on the sphere, Dirichlet energy and extremal length, and component correspondence for limits. Contributions formalizing the named intermediate results (Theorem 3.1 finite transfer, Theorem 4.3 compatible barrier lemma, Theorem 5.1 positive-law alternative, Theorem 7.5 retained-test transfer) or the classical He–Schramm countable case are welcome.

Selected references

• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Koebes-Circle-Domain-Conjecture-September-23-2026/paper.pdf
• P. Koebe, Über die Uniformisierung beliebiger analytischer Kurven (Dritte Mitteilung), Nachr. Ges. Wiss. Göttingen, 1908.
• P. Koebe, Abhandlungen zur Theorie der konformen Abbildung VI, Math. Z., 1920. https://doi.org/10.1007/BF01199400
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• O. Schramm, Transboundary extremal length, J. Analyse Math., 1995. https://doi.org/10.1007/BF02788827
• K. Rajala, Uniformization of planar domains by exhaustion, Amer. J. Math., 2025. https://doi.org/10.1353/ajm.2025.a966291
• D. Ntalampekos, K. Rajala, Exhaustions of circle domains, IMRN, 2025. https://doi.org/10.1093/imrn/rnaf296
• B. Esmayli, K. Rajala, Conformal uniformization of domains bounded by quasitripods, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0035
• C. Karafyllia, D. Ntalampekos, Uniformization of Gromov hyperbolic domains by circle domains, Duke Math. J., 2026. https://doi.org/10.1215/00127094-2025-0076
• D. Ntalampekos, Uniformization problems in the plane: A survey, preprint, 2026. https://arxiv.org/abs/2603.15098

Motivation

A circle domain is a domain in the Riemann sphere whose complementary components are round disks or points. Koebe asked in 1908 whether every domain is conformally equivalent to a circle domain (existence). A second question is rigidity: when is that circle-domain model unique up to Möbius transformations? For finitely and countably connected domains the model is unique, but for domains with uncountably many boundary components uniqueness can fail, and the boundary geometry decides. He and Schramm conjectured that a circle domain is rigid exactly when its boundary is conformally removable. Rigidity is what makes the circle-domain model canonical, and it connects conformal geometry with removability questions for quasiconformal and Sobolev maps.

Timeline

• 1993. He and Schramm prove uniformization and rigidity for countably connected circle domains (doi:10.2307/2946541).
• 1994. He and Schramm prove rigidity when the boundary has $\sigma$-finite linear measure, and conjecture that rigidity is equivalent to conformal removability of the boundary (doi:10.1007/BF01231761).
• 2000. Jones and Smirnov relate removability for continuous Sobolev functions to quasiconformal removability (doi:10.1007/BF02384320).
• 2016. Younsi proves that conformal rigidity is equivalent to quasiconformal rigidity and studies the removability formulations (doi:10.1016/j.aim.2016.08.039).
• 2020. Ntalampekos and Younsi prove rigidity under square integrability of the quasihyperbolic distance, covering Hölder and John circle domains (doi:10.1007/s00222-019-00921-1).
• 2023–2024. Ntalampekos proves rigidity when point components are countably negligible for extremal distance (CNED) and continuous Sobolev extension across closed CNED sets (doi:10.1090/tran/8923, doi:10.1007/s00029-024-00951-5).
• 2025. Rajala constructs a rigid circle domain with non-removable boundary, so rigidity does not imply removability (doi:10.1112/plms.70081).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the remaining implication: removability implies rigidity.

Setting

The Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$ has local coordinates $z$ and $1/z$. A map is conformal at $p$ if it is continuous there and complex differentiable with nonzero derivative in these coordinates; a conformal equivalence $f:\Omega\to\Omega'$ is a bijection, conformal on $\Omega$, with conformal inverse. A Möbius transformation is $z\mapsto(az+b)/(cz+d)$ with $ad-bc\neq0$. A closed round disk is the Möbius image of the closed unit disk. A circle domain is a nonempty connected open set whose complementary components are closed round disks or points.

A compact $E\subset\widehat{\mathbb C}$ is conformally removable if every orientation-preserving homeomorphism of $\widehat{\mathbb C}$ that is conformal on $\widehat{\mathbb C}\setminus E$ is Möbius. A circle domain $\Omega$ is conformally rigid if every conformal equivalence from $\Omega$ onto another circle domain is the restriction of a Möbius transformation.

Formalization targets

Goal: Theorem 1.1

$$\Omega,\Omega'\ \text{circle domains},\ \ \partial\Omega\ \text{conformally removable},\ \ f:\Omega\to\Omega'\ \text{conformal equivalence}\ \Longrightarrow\ \exists M\ \text{Möbius}:\ f=M|_\Omega.$$

Lean: OAI.Problem047.removability_implies_rigidity, open on the platform. The complement may have any cardinality, and no boundary extension of $f$ is assumed.

Significance

Together with Rajala's counterexample to the converse, the theorem would settle the He–Schramm rigidity conjecture: removability is sufficient but not necessary. It subsumes the earlier sufficient conditions ($\sigma$-finite length, Hölder/John domains, CNED point sets) whenever those boundaries are removable. The intermediate Theorem 5.1, a continuous Sobolev extension theorem across compact totally disconnected conformally removable sets, is of independent interest. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Removability is a statement about homeomorphisms of the whole sphere, while rigidity starts from a map defined only on the domain. The obvious route, extending $f$ to a homeomorphism of the sphere and then invoking removability, fails: a point component of the complement of $\Omega$ may correspond to a disk component of $\Omega'$ and vice versa, so the coordinates of $f$ need not extend continuously, and nothing a priori controls boundary behaviour at uncountably many point components whose union can have positive area.

Formalization scope

• Sphere := OnePoint ℂ, Möbius maps are Matrix.GeneralLinearGroup (Fin 2) ℂ acting on it; conformality uses the charts $z$ and $1/z$ with HasDerivAt and a nonzero derivative.
• IsCircleDomain: open, IsConnected, and every connectedComponentIn of the complement is a singleton or a Möbius image of the closed unit disk.
• IsConformallyRemovable E: IsCompact E and every homeomorphism h : Sphere ≃ₜ Sphere that is homotopic to the identity (orientation preserving) and conformal on Eᶜ equals some Möbius map everywhere.
• The boundary is frontier U; the conclusion is ∃ M, ∀ p ∈ U, f p = M • p.
• The shared definitions are those of the Koebe circle-domain mission of the same family.

A complete development needs the theory of conformal maps on the sphere, Sobolev functions and Dirichlet energy in the plane, the measurable Riemann mapping theorem (used for the conductivity deformation), and component correspondence. Contributions formalizing Theorem 5.1 (continuous Sobolev extension), Proposition 6.2 (common point traces), or the He–Schramm countable case are welcome.

Selected references

• OpenAI, Removable Boundaries and Rigidity of Circle Domains, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Removable-Boundaries-and-Rigidity-of-Circle-Domains-September-23-2026/paper.pdf
• Z.-X. He, O. Schramm, Fixed points, Koebe uniformization and circle packings, Ann. of Math., 1993. https://doi.org/10.2307/2946541
• Z.-X. He, O. Schramm, Rigidity of circle domains whose boundary has σ-finite linear measure, Invent. Math., 1994. https://doi.org/10.1007/BF01231761
• M. Younsi, Removability, rigidity of circle domains and Koebe's conjecture, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2016.08.039
• D. Ntalampekos, M. Younsi, Rigidity theorems for circle domains, Invent. Math., 2020. https://doi.org/10.1007/s00222-019-00921-1
• D. Ntalampekos, Rigidity and continuous extension for conformal maps of circle domains, Trans. Amer. Math. Soc., 2023. https://doi.org/10.1090/tran/8923
• D. Ntalampekos, CNED sets: countably negligible for extremal distances, Selecta Math., 2024. https://doi.org/10.1007/s00029-024-00951-5
• P. W. Jones, S. K. Smirnov, Removability theorems for Sobolev functions and quasiconformal maps, Ark. Mat., 2000. https://doi.org/10.1007/BF02384320
• K. Rajala, Rigid circle domains with non-removable boundaries, Proc. Lond. Math. Soc., 2025. https://doi.org/10.1112/plms.70081
• OpenAI, Koebe's Circle-Domain Conjecture, preprint, September 23, 2026.

Motivation: which bounded domains cover compact spaces?

A bounded symmetric domain is a bounded connected open set in $\mathbb C^m$ with, at every point, a holomorphic involution having that point as an isolated fixed point. Examples are the ball, the polydisc and the Siegel upper half-spaces in their bounded realizations. They are the universal covers of compact locally symmetric varieties, such as compact quotients of the ball, and play a central role in algebraic geometry and number theory. A classical theme in several complex variables is that a bounded domain with a large automorphism group must be very special: Wong and Rosay showed that an automorphism orbit accumulating at a strongly pseudoconvex boundary point forces the ball, and Frankel showed that convex domains with compact quotients are symmetric.

Kollár and Pardon, studying algebraic varieties whose universal cover is semialgebraic, asked the following bounded-domain question: if a bounded semialgebraic open subset of a complex affine variety admits a properly discontinuous cocompact group of biholomorphisms, must it be a bounded symmetric domain? Semialgebraicity is a finiteness condition on the shape of the domain. It does not make the boundary smooth or convex, and it imposes nothing on the group.

Timeline

• 1970 — Vey proves that a divisible generalized Siegel domain is symmetric (Ann. Sci. ÉNS 3).
• 1977 — Wong characterizes the ball by its automorphism group among strongly pseudoconvex domains (Invent. Math. 41).
• 1979 — Rosay localizes Wong's theorem to a single $C^2$ strongly pseudoconvex boundary point (Ann. Inst. Fourier 29).
• 1989 — Frankel proves that a convex hyperbolic domain with compact quotient is a bounded symmetric domain, including non-free actions (Acta Math. 163).
• 2012 — Kollár and Pardon pose the bounded semialgebraic domain question (arXiv v2, Question 25) in Algebraic varieties with semialgebraic universal cover (J. Topol. 5; arXiv:1104.2309v2).
• 2021 — Zimmer shows that a $C^{1,1}$-bounded domain covering a compact manifold is a ball (Indiana Univ. Math. J. 70).
• 2026 — An OpenAI preprint, Symmetry of semialgebraic bounded domains with compact quotient (OpenAI Math Release, September 24, 2026), claims an affirmative answer to the Kollár–Pardon question. It has not been peer reviewed, and its proof is not formally verified.

Setting

An affine variety is a reduced complex algebraic set $V\subset\mathbb C^n$, the common zero locus of a set of polynomials. A subset of $\mathbb C^n$ is semialgebraic if it is a finite Boolean combination of sets $\{p=0\}$ and $\{p>0\}$, with $p$ a real polynomial in the real and imaginary parts of the coordinates. Let $U\subseteq V$ be open in $V$, connected, semialgebraic and bounded. A map on $U$ is holomorphic if near each point it is the restriction of a holomorphic map on an open subset of $\mathbb C^n$; a biholomorphism is a homeomorphism that is holomorphic in both directions. A group $\Gamma$ acts properly discontinuously if the action is proper for the discrete topology on $\Gamma$ (finite stabilizers are allowed), and the action is cocompact if $U/\Gamma$ is compact. $U$ is smooth if each point has a neighbourhood in $U$ biholomorphic to an open subset of some $\mathbb C^m$.

Formalization targets

Goal: semialgebraic bounded domains with compact quotient are symmetric (Theorem 1.1)

Let $U$ be a nonempty connected semialgebraic bounded open subset of a complex affine variety $V\subset\mathbb C^n$, and let a group $\Gamma$ act on $U$ by biholomorphisms, properly discontinuously and with $U/\Gamma$ compact. Then

$$U\ \text{is smooth, and}\quad U\cong D\ \text{biholomorphically for some bounded symmetric domain } D\subset\mathbb C^m .$$

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

Significance

The result itself. The theorem answers the Kollár–Pardon question affirmatively. The ambient variety may be singular and nonnormal, the quotient may have finite quotient singularities, and no convexity, boundary regularity or homogeneity is assumed. It shows that semialgebraicity of a single affine realization forces the classical picture: a compact quotient of a semialgebraic bounded domain is a compact quotient of a bounded symmetric domain. This complements the universal-cover classification of the companion preprint on semialgebraic universal covers of normal projective varieties.

Formalizing it. The statement only uses polynomials, real-analytic Boolean combinations, holomorphic maps on subsets of $\mathbb C^n$ and group actions, all available in Mathlib. The proof, however, draws on Nash cell decompositions, analytic discs, scaling limits of automorphisms and Vey's theorem on divisible Siegel domains, none of which is formalized. A formal development would provide reusable semialgebraic geometry and several-complex-variables infrastructure.

Difficulty

The classical rigidity arguments (Wong–Rosay, Frankel, Zimmer) need a smooth strongly pseudoconvex or convex boundary point at which rescaled automorphisms converge to a model domain. A semialgebraic boundary can have corners with several complex-normal directions, and the normal fibres can shrink at rates that depend on tangential parameters, so the naive rescaling limit can collapse to a degenerate set. Moreover $U$ is not known to be a manifold at the start, so smoothness must be proved from the group action before any differential geometry is available. The heart of the proof is a noncollapse estimate that yields a Siegel-type quadratic model $\{\operatorname{Im}w-H(z,z)\in C\}$ to which Vey's theorem applies.

Formalization scope

• $V$ is IsAffineAlgebraic, the zero set of a set of complex polynomials in Fin n → ℂ; $U\subseteq V$ is open in the subspace topology of $V$, IsConnected (hence nonempty), bounded, and semialgebraic through an inductive predicate on real polynomials in $(\operatorname{Re}z,\operatorname{Im}z)$, closed under complement and union.
• $\Gamma$ is an arbitrary group with the discrete topology acting on the subtype $U$, with ProperSMul and a compact orbit space. Each $\gamma$ acts holomorphically in the sense of local ambient analytic extension; since $\gamma^{-1}$ also acts, the elements act by biholomorphisms. A non-faithful action is allowed and is harmless, since properness forces finite stabilizers.
• IsSmooth U asks for local biholomorphisms of neighbourhoods in $U$ onto open subsets of some $\mathbb C^m$. IsBoundedSymmetricDomain D asks that $D$ be open, connected and bounded, and have at each point an involutive biholomorphism fixing it with that point isolated among its fixed points.
• The zero-dimensional case (a point) is included and is trivial, matching the source convention.
• Needed infrastructure: semialgebraic cell decomposition and selection, Montel-type compactness on singular analytic sets, analytic discs, Kobayashi/Carathéodory-type distance estimates and the structure theory of Siegel domains. Each would be reusable.

Selected references

• J. Vey, Sur la division des domaines de Siegel, Ann. Sci. École Norm. Sup. (4) 3 (1970), 479–506. https://www.numdam.org/article/ASENS_1970_4_3_4_479_0.pdf
• B. Wong, Characterization of the unit ball in $\mathbb C^n$ by its automorphism group, Invent. Math. 41 (1977), 253–257. https://doi.org/10.1007/BF01403050
• J.-P. Rosay, Sur une caractérisation de la boule parmi les domaines de $\mathbb C^n$ par son groupe d'automorphismes, Ann. Inst. Fourier 29 (1979), 91–97. https://doi.org/10.5802/aif.768
• S. Frankel, Complex geometry of convex domains that cover varieties, Acta Math. 163 (1989), 109–149. https://doi.org/10.1007/BF02392734
• J. Kollár and J. Pardon, Algebraic varieties with semialgebraic universal cover, J. Topol. 5 (2012), 199–212. https://doi.org/10.1112/jtopol/jts001
• A. Zimmer, Smoothly bounded domains covering compact manifolds, Indiana Univ. Math. J. 70 (2021), 2653–2676. https://arxiv.org/abs/1910.05288v2
• M. Coste, Real algebraic sets, lecture notes, 2005. https://indico.ictp.it/event/a04204/session/10/contribution/7/material/0/0.pdf
• OpenAI, Symmetry of semialgebraic bounded domains with compact quotient, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Symmetry-of-semialgebraic-bounded-domains-with-compact-quotient-September-24-2026/paper.pdf

Motivation: when is a split tangent bundle integrable?

If a complex manifold is a product $X_1\times X_2$, its tangent bundle splits as the sum of the pulled-back tangent bundles of the factors, and each summand is integrable: the bracket of two local holomorphic vector fields tangent to a summand stays in that summand. Conversely, given a holomorphic decomposition $T_X=E_1\oplus E_2$, one wants to know whether it comes from a product. Integrability of the summands is the necessary local condition, and it can fail: Höring exhibited a non-integrable summand on the product of an abelian surface with $\mathbb P^1$ (Höring 2007, Example 2.14). For rationally connected projective manifolds — those in which two general points lie on a rational curve, a class including all Fano manifolds — Höring showed that integrability of one summand already yields a compatible product decomposition, which made automatic integrability the remaining question.

Timeline

• 2000 — Beauville studies how a tangent splitting of a compact Kähler manifold leads to a product decomposition of its universal cover (Beauville 2000).
• 2002 — Campana and Peternell treat Fano manifolds with a two-summand splitting when one summand has rank one or two, hence every two-summand splitting of a Fano manifold of dimension at most five (Campana–Peternell 2002, Theorems 3.5–3.6, Corollary 3.7).
• 2007 — Höring proves that on a rationally connected projective manifold integrability of one summand gives a compatible product (Höring 2007, Theorem 1.4).
• 2008 — Höring conjectures that at least one summand is integrable and proves it when all summands of a uniruled manifold have rank at most two (Höring 2008, Conjecture 1.2, Lemma 4.21).
• 2026 — Höring proves integrability with algebraic leaves on $\mathbb Q$-factorial klt varieties of Fano type, giving actual products in the smooth Fano case, and formulates the smooth rationally connected statement as Conjecture 1.5; a singular rationally connected counterexample shows smoothness matters (Höring 2026).
• 2026 — An OpenAI preprint, Integrability of split tangent bundles on rationally connected manifolds (OpenAI Math Release, September 23, 2026), claims this conjecture in full: both summands are always integrable. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

A complex manifold $X$ of dimension $n$ is a Hausdorff, second-countable space with a holomorphic atlas to $\mathbb C^n$. $X$ is projective if it admits an injective holomorphic immersion into a complex projective space $\mathbb P^N$; for compact $X$ this is a closed embedding.

A rational curve in $X$ is a holomorphic map $\mathbb P^1\to X$. A compact connected projective manifold is rationally connected if there is a nonempty Zariski-open set $U\subseteq X\times X$ such that every pair $(x,y)\in U$ lies on the image of a rational curve. Here Zariski-open is measured through the projective embedding: $U$ is the complement of the common zero set of a family of bihomogeneous polynomials in the two sets of homogeneous coordinates.

A holomorphic splitting $T_X=E_1\oplus E_2$ is given by a holomorphic field of idempotent linear maps $P_x$ on the tangent spaces, with $E_1=\operatorname{im}P$ and $E_2=\ker P$, both of positive rank at every point. A family of subspaces $D$ is integrable if for every open $U$ and every pair of holomorphic vector fields $V,W$ on $U$ with values in $D$, the Lie bracket $[V,W]$ takes values in $D$.

Formalization targets

Goal: Theorem 1.1 (automatic integrability)

Let $X$ be a smooth connected projective complex manifold of dimension at least two which is rationally connected. For every holomorphic decomposition $T_X=E_1\oplus E_2$ into subbundles of positive rank,

$$[\Gamma(U,E_1),\Gamma(U,E_1)]\subseteq\Gamma(U,E_1)\quad\text{and}\quad[\Gamma(U,E_2),\Gamma(U,E_2)]\subseteq\Gamma(U,E_2)$$

for every open $U\subseteq X$, where $\Gamma(U,E_i)$ denotes holomorphic sections over $U$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem has no rank or positivity hypothesis, and it settles the smooth rationally connected case of Höring's conjecture. Combined with Höring's product theorem it gives Corollary 1.2: every holomorphic splitting of the tangent bundle of a smooth rationally connected projective manifold comes from an isomorphism $X\simeq X_1\times X_2$ identifying $E_i$ with the factor tangent bundles. It also applies to general fibers of the rationally connected quotient of a uniruled compact Kähler manifold, supplying the integrability premise in Höring's structure theorems (Corollary 5.1). Together with the companion preprint on universal-cover splitting for compact Kähler manifolds, it covers both the integrability question and the global product question.

Formalizing it. The statement involves projective embeddings, Zariski-open sets of pairs, rational curves and holomorphic distributions, all expressed from first principles over Mathlib's manifold library. A machine-checked proof would certify a classical-looking but new geometric argument; the compatible product (Corollary 1.2) is not part of this goal.

Difficulty

The bracket of two sections of $E_1$, projected to $E_2$, is a tensor $\bigwedge^2E_1\to E_2$, and the task is to show it vanishes. The natural approach is to restrict to rational curves and use positivity, as in the Fano and low-rank cases, but without positivity or rank assumptions the restricted bundles can have summands of either sign and no vanishing follows directly. Smoothness cannot be dropped: a singular rationally connected example with a non-integrable summand exists (Höring 2026, Example 4.3), so the argument must use the manifold structure in an essential way. Rational connectedness is also needed: Höring's example on an abelian surface times $\mathbb P^1$ is a smooth projective manifold with a non-integrable summand.

Formalization scope

• ComplexManifold carries its dimension, a Hausdorff second-countable topology, and an analytic (ω) atlas modeled on Fin dim → ℂ. The theorem assumes ConnectedSpace, CompactSpace and 2 ≤ X.dim.
• ProjectiveEmbedding X is an injective map to ℙ ℂ (Fin (N+1) → ℂ) that is holomorphic and immersive in every affine patch.
• RationalCurve X is a holomorphic map from $\mathbb P^1$ given by two holomorphic maps $\mathbb C\to X$ agreeing via $z\mapsto z^{-1}$; RationallyConnected e asks for a nonempty, dense, Zariski-open set of pairs (bihomogeneous polynomial complement) all joined by rational curves. Density is automatic for a nonempty Zariski-open subset of the irreducible variety $X\times X$, so stating it does not narrow the class.
• TangentSplitting X is a holomorphic idempotent field on the tangent bundle with range and kernel of positive rank at every point. Integrable uses VectorField.mlieBracketWithin for sections that are holomorphic on an open set.
• The conclusion asserts integrability of both the range and the kernel; the compatible product of Corollary 1.2 is not asserted.
• Infrastructure needed: holomorphic maps from $\mathbb P^1\times\mathbb P^1$, resolution of indeterminacy for rational maps of surfaces, holomorphic bundles on $\mathbb P^1$, families of rational curves. The splitting and integrability definitions are reusable for the companion universal-cover mission.

Selected references

• A. Beauville, Complex manifolds with split tangent bundle, in Complex Analysis and Algebraic Geometry (de Gruyter, 2000), 61–70. https://arxiv.org/abs/math/9809033v2
• F. Campana, T. Peternell, Projective manifolds with splitting tangent bundle, I, Math. Z. 241 (2002), 613–637. https://doi.org/10.1007/s00209-002-0435-5
• A. Höring, Uniruled varieties with split tangent bundle, Math. Z. 256 (2007), 465–479. https://arxiv.org/abs/math/0505327v3
• A. Höring, The structure of uniruled manifolds with split tangent bundle, Osaka J. Math. 45 (2008), 1067–1084. https://www.i-repository.net/contents/osakacu/sugaku/111F0000002-04504-14.pdf
• A. Höring, Fano varieties with split tangent sheaf, preprint (2026). https://arxiv.org/abs/2602.15427v1
• J. Kollár, Y. Miyaoka, S. Mori, Rationally connected varieties, J. Algebraic Geom. 1 (1992), 429–448.
• OpenAI, Integrability of split tangent bundles on rationally connected manifolds, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026/main.pdf