Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.13981Formalized record≥ 2.15Open frontier

11 provers on it22 of 23 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record≤ 1.9202796Open frontier

4 provers on it7 of 8 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 2Formalized record

19 provers on it9 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 4Formalized record≤ 2Open frontier

8 provers on it17 of 18 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 19Formalized record≤ 5Open frontier

41 provers on it17 of 19 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Analysis Partial Differential Equations·Captain: wurtle

The Subcritical Hénon–Lane–Emden ConjectureResearch Paper

Motivation: Liouville theorems for Lane–Emden systems

Liouville theorems say that certain nonlinear elliptic equations have no positive solutions on the whole space. Beyond their own interest, they are the key input in blow-up and rescaling arguments that give a priori bounds, existence results and singularity estimates for equations on bounded domains (Gidas–Spruck 1981; Polačik–Quittner–Souplet 2007). For the scalar equation $-\Delta u=u^p$ , Gidas and Spruck proved nonexistence in the whole subcritical range. For the coupled Lane–Emden system $-\Delta u=v^p$ , $-\Delta v=u^q$ , the corresponding statement — no positive solutions below the critical hyperbola $\frac1{p+1}+\frac1{q+1}=\frac{n-2}{n}$ — is the Lane–Emden conjecture; before the source, it had been proved only in dimensions $n\le4$ and in partial ranges. The weighted Hénon–Lane–Emden version, with factors $|x|^A$ and $|x|^B$ , asks the same question for the weighted hyperbola.

Timeline

1981 — Gidas and Spruck: scalar subcritical Liouville theorem and the blow-up method for a priori bounds (CPAM 1981; CPDE 1981).
1993, 1996 — Mitidieri: a Rellich-type identity for systems and early nonexistence regions (CPDE 1993; DIE 1996).
1996 — Serrin and Zou: the unweighted conjecture for $n=3$ under a growth condition (DIE 1996).
2007 — Polačik, Quittner and Souplet remove the growth condition for $n=3$ (Duke 2007).
2009 — Souplet proves the Lane–Emden conjecture for $n=4$ (Adv. Math. 2009); Chen and Li use integral systems and moving planes under integrability hypotheses (DCDS 2009).
2010 — Bidaut-Véron and Giacomini identify the critical weighted hyperbola in the radial theory and prove radial existence on and above it (ADE 2010).
2012 — Phan formulates the weighted question for $A,B>-2$ (Conjecture C) and proves bounded, low-dimensional and conditional cases (ADE 2012).
2014 — Fazly and Ghoussoub: bounded and stable cases for nonnegative weights (DCDS 2014).
2019 — Li and Zhang prove the Hénon–Lane–Emden conjecture in $\mathbb R^3$ (JDE 2019); Cheng and Huang give an energy-estimate criterion for the unweighted conjecture (DCDS 2019).
2022 — H. Li: restricted exponent ranges in dimensions four and five (Adv. Nonlinear Stud. 2022).
2025–2026 — K. Li, M. Li and Wei: a new unweighted region for $p,q\ge1$ when $n\ge5$ (preprint, 2025). Huang and Zou state the all-real-weight, origin-continuous assertion as Conjecture B (J. London Math. Soc. 2026). Xu and Luo treat radial higher-order systems (JDE 2026).
2026 — An OpenAI preprint, The Subcritical Hénon–Lane–Emden Conjecture (OpenAI Math Release, September 24, 2026), claims the full subcritical nonexistence theorem for every $n\ge2$ and all real weights. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Fix an integer $n\ge2$ , exponents $p,q>0$ and real weights $A,B$ . The Hénon–Lane–Emden system is

-\Delta u=|x|^A\,v^p,\qquad -\Delta v=|x|^B\,u^q\qquad\text{in }\mathbb R^n\setminus\{0\},

where $\Delta=\sum_i\partial_i^2$ is the Laplacian. A solution in the sense of the source is a pair $u,v\in C^2(\mathbb R^n\setminus\{0\})\cap C(\mathbb R^n)$ with $u(x)>0$ and $v(x)>0$ for every $x\in\mathbb R^n$ , including the origin, satisfying both equations at every $x\neq0$ . The exponents are subcritical if

\frac{n+A}{p+1}+\frac{n+B}{q+1}>n-2 .

In Lean, Space n = EuclideanSpace ℝ (Fin n), IsSolution n p q A B u v packages continuity, ContDiffOn ℝ 2 off the origin, strict positivity everywhere and the two equations with Mathlib's Laplacian and real powers, and Subcritical is the displayed inequality.

Formalization targets

Goal: subcritical nonexistence (Theorem 1.1)

n\ge2,\ p,q>0,\ A,B\in\mathbb R,\ \frac{n+A}{p+1}+\frac{n+B}{q+1}>n-2\ \Longrightarrow\ \nexists\,(u,v)\ \text{solving the system as above}.

This is exactly Theorem 1.1 of the source. Taking $A=B=0$ gives the unweighted Lane–Emden conjecture (Corollary 1.2) for $n\ge3$ . The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem gives a positive answer to Huang and Zou's Conjecture B and, with $A=B=0$ , to the Lane–Emden conjecture in every dimension. It needs no radial symmetry, boundedness, integrability, finite energy, stability or growth condition at infinity. Combined with the radial existence theorem of Bidaut-Véron and Giacomini, it also settles Phan's Conjecture C for $n\ge3$ and $A,B>-2$ , including existence on the critical hyperbola (Corollary 6.2). Through the blow-up method, Liouville theorems of this type give a priori bounds and singularity and decay estimates for Lane–Emden-type systems on bounded domains.

Formalizing it. The statement is elementary: classical derivatives, the Euclidean Laplacian and real powers. The proof uses potential estimates, a localized virial (Rellich–Pohozaev type) identity, a geometric interval inequality and a dilation argument. All of these are within reach of Mathlib's analysis library, which makes the theorem a realistic test of large-scale PDE formalization.

Difficulty

The weighted statement does not follow from the unweighted one at the same exponents. For example, $n=5$ , $p=q=4$ , $A=B=3$ is weighted-subcritical, while $\frac1{p+1}+\frac1{q+1}=\frac25<\frac35$ is unweighted-supercritical. Weighted subcriticality also does not give the unweighted input in Phan's transfer argument. Translations do not preserve the weighted equation, so moving-plane and translation-based compactness arguments are unavailable. The level sets $\{|x|^Bu^q>t\}$ have endpoint values that vary with $|x|$ , which breaks the unweighted interval comparison. Finally, since no energy, decay or stability bound is assumed, the localized energy has to be bounded from the subcritical gap alone.

Formalization scope

The domain is EuclideanSpace ℝ (Fin n) with $n\ge2$ , and $p,q,A,B$ are real with $p,q>0$ . Weights are Real.rpow ‖x‖ A, used only at $x\neq0$ , so the junk value of rpow at $0$ never enters. The nonlinearities Real.rpow (v x) p are evaluated at strictly positive arguments.
Regularity is Continuous on all of $\mathbb R^n$ and ContDiffOn ℝ 2 on $\{0\}^c$ . Positivity is required at every point, including the origin, as in the source; differentiability at the origin is not assumed.
The conclusion is the nonexistence of any such pair. Every hypothesis is satisfiable (supercritical solutions exist), so the statement is not trivialized.
Infrastructure needed: Newtonian potentials and distributional extension across a point, Rellich–Pohozaev identities, polar integration and dilation arguments. These pieces would serve other Liouville-type theorems.

Selected references

B. Gidas and J. Spruck, Global and local behavior of positive solutions of nonlinear elliptic equations, Comm. Pure Appl. Math. 34 (1981), 525–598. https://doi.org/10.1002/cpa.3160340406
B. Gidas and J. Spruck, A priori bounds for positive solutions of nonlinear elliptic equations, Comm. PDE 6 (1981), 883–901. https://doi.org/10.1080/03605308108820196
E. Mitidieri, A Rellich type identity and applications, Comm. PDE 18 (1993), 125–151. https://doi.org/10.1080/03605309308820923
E. Mitidieri, Nonexistence of positive solutions of semilinear elliptic systems in $\mathbb R^N$ , Differential Integral Equations 9 (1996), 465–479. https://doi.org/10.57262/die/1367969966
J. Serrin and H. Zou, Non-existence of positive solutions of Lane–Emden systems, Differential Integral Equations 9 (1996), 635–653. https://doi.org/10.57262/die/1367969879
P. Polačik, P. Quittner and P. Souplet, Duke Math. J. 139 (2007), 555–579. https://doi.org/10.1215/S0012-7094-07-13935-8
P. Souplet, The proof of the Lane–Emden conjecture in four space dimensions, Adv. Math. 221 (2009), 1409–1427. https://doi.org/10.1016/j.aim.2009.02.014
W. Chen and C. Li, An integral system and the Lane–Emden conjecture, Discrete Contin. Dyn. Syst. 24 (2009), 1167–1184. https://doi.org/10.3934/dcds.2009.24.1167
M.-F. Bidaut-Véron and H. Giacomini, A new dynamical approach of Emden–Fowler equations and systems, Adv. Differential Equations 15 (2010), 1033–1082. https://doi.org/10.57262/ade/1355854434
Q. H. Phan, Adv. Differential Equations 17 (2012), 605–634. https://doi.org/10.57262/ade/1355702970
M. Fazly and N. Ghoussoub, On the Hénon–Lane–Emden conjecture, Discrete Contin. Dyn. Syst. 34 (2014), 2513–2533. https://doi.org/10.3934/dcds.2014.34.2513
K. Li and Z. Zhang, Proof of the Hénon–Lane–Emden conjecture in $\mathbb R^3$ , J. Differential Equations 266 (2019), 202–226. https://doi.org/10.1016/j.jde.2018.07.036
Z. Cheng and G. Huang, A Liouville theorem for the subcritical Lane–Emden system, Discrete Contin. Dyn. Syst. 39 (2019), 1359–1377. https://doi.org/10.3934/dcds.2019058
H. Li, Adv. Nonlinear Stud. 22 (2022), 517–533. https://doi.org/10.1515/ans-2022-0027
L.-H. Huang and W. Zou, J. London Math. Soc. 113 (2026), e70412. https://doi.org/10.1112/jlms.70412
Y. Xu and H. Luo, Liouville type theorems for higher order elliptic systems, J. Differential Equations 453 (2026), 113823. https://doi.org/10.1016/j.jde.2025.113823
OpenAI, The Subcritical Hénon–Lane–Emden Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Subcritical-Henon-Lane-Emden-Conjecture-September-24-2026/paper.pdf

10 thms2 active usersReviewed

Completed

Analysis Partial Differential Equations·Captain: wurtle

Strict hot spots and absence of interior critical points on smooth simply connected planar domainsResearch Paper

Motivation

Heat in an insulated planar plate evolves by the heat equation with Neumann boundary condition. For generic initial temperature, after a long time the temperature minus its average is dominated by an eigenfunction of the first positive Neumann eigenvalue. Rauch asked in 1974 where the hottest and coldest points of the plate end up, and conjectured that they move to the boundary (Rauch 1975). In spectral form, the hot spots conjecture asks whether a first nonconstant Neumann eigenfunction attains its maximum and minimum only on the boundary. The question links spectral geometry, reflected Brownian motion and elliptic PDE, and it is known to depend on topology: it fails for some domains with holes.

This mission asks for a machine-checked proof of the strict form of the conjecture for all smooth bounded simply connected planar domains, as claimed in an OpenAI preprint dated September 24, 2026 (source): every nonzero first-positive Neumann eigenfunction has no interior critical point at all. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

1975 — Rauch poses the problem in lectures on qualitative PDE theory (Rauch 1975).
1999 — Bañuelos and Burdzy distinguish strict and nonstrict formulations and prove cases by coupling of reflected Brownian motions (J. Funct. Anal. 1999). Burdzy and Werner construct a counterexample with two holes (Ann. of Math. 1999).
2000 — Jerison and Nadirashvili prove the conjecture for convex planar domains with two axes of symmetry (JAMS 2000); Bass and Burdzy find examples with both extrema in the interior (Duke 2000).
2002–2004 — Pascu treats convex domains with one symmetry (Trans. AMS 2002); Atar and Burdzy treat lip domains (JAMS 2004).
2005 — Burdzy obtains a counterexample with a single hole and states the simply connected planar conjecture explicitly (Duke 2005, Conjecture 1.2(ii)).
2007 — Miyamoto handles nearly circular convex domains under a spectral-diameter condition.
2015–2022 — Siudeja proves the conjecture for a class of acute triangles (Math. Z. 2015); Judge and Mondal exclude interior critical points on every triangle (Ann. of Math. 2020, erratum 2022).
2021–2024 — Rohleder introduces a variational principle for tangent vector fields (arXiv:2106.05224; 2024), the starting point of the preprint.
2025–2026 — Sharp bounds on the failure of the conjecture (de Dios Pont–Hsu–Taylor, 2025); classification of critical points on triangles (Chen–Gui–Yao, Invent. Math. 2026).
September 2026 — The OpenAI preprint claims the strict conjecture for all smooth bounded simply connected planar domains (Theorem 1.1, p. 1).

Setting

Let $\Omega\subset\mathbb R^2$ be a nonempty bounded open simply connected set with $C^\infty$ boundary. The first positive Neumann eigenvalue is

\mu=\mu_1(\Omega)=\inf\Bigl\{\frac{\int_\Omega|\nabla v|^2}{\int_\Omega v^2}: v\in H^1(\Omega),\ \int_\Omega v=0,\ v\ne0\Bigr\},

counting only positive eigenvalues (many sources call it $\mu_2$ ). The first positive Neumann eigenspace $V$ consists of the $u\in H^1(\Omega)$ with $\int_\Omega u=0$ and

\int_\Omega\nabla u\cdot\nabla v=\mu\int_\Omega uv\qquad\text{for all }v\in H^1(\Omega).

This weak formulation encodes $-\Delta u=\mu u$ in $\Omega$ with $\partial_\nu u=0$ on $\partial\Omega$ . Eigenspace functions are smooth up to the boundary.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every nonzero $u\in V$ ,

\nabla u(x)\ne0\quad(x\in\Omega),\qquad\text{and}\qquad \min_{\partial\Omega}u<u(x)<\max_{\partial\Omega}u\quad(x\in\Omega).

This holds for every member of the eigenspace, also when $\mu$ is a multiple eigenvalue. In Lean this is OAI.StrictHotSpots.main_theorem.

Significance

The result itself. It resolves Burdzy's simply connected planar hot spots conjecture in its strongest form: not only do the extrema lie on the boundary, but there are no interior saddle points either, for every eigenfunction in the eigenspace. Combined with the Burdzy–Werner and Burdzy one-hole counterexamples, it shows that simple connectivity is exactly the dividing line among smooth planar domains. The intermediate kernel theorem (Theorem 5.1, p. 12), a conditional negativity statement for reciprocal Green kernels of the disk, is stated independently of the eigenfunction problem.

Formalizing it. A complete development needs Sobolev spaces on smooth planar domains, the Riemann mapping theorem with boundary regularity, Neumann elliptic regularity, and the theory of conditionally negative definite kernels. Each is reusable. No machine-checked proof of any hot spots result, including the triangle case, is known to exist.

Difficulty

Each Cartesian derivative of an eigenfunction solves the same Helmholtz equation, but its boundary values have no fixed sign, so a maximum-principle argument on one directional derivative fails on a general domain with no preferred direction. Coupling methods need convexity or symmetry. The preprint instead uses the Neumann condition jointly on both derivatives (the gradient is tangent to the boundary), via a nonnegative quadratic form whose null space consists exactly of eigenfunction gradients (Proposition 3.1, p. 7). The central difficulty is to build enough scalar boundary multipliers preserving that null space; this requires proving that a reciprocal kernel $K(p,s)K(p,t)/N(s,t)$ is conditionally negative semidefinite (Theorem 5.1, p. 12), through regularized Green kernels, a complete Nevanlinna–Pick-type matrix property, and a boundary limit.

Formalization scope

$\Omega$ is a subset of EuclideanSpace ℝ (Fin 2): nonempty, open, bounded, IsSimplyConnected (which includes path-connectedness), with a smooth local defining function $\rho$ with nonzero derivative at every boundary point.
$H^1$ is encoded by HasH1Gradient Ω v g: $v,g\in L^2(\Omega)$ and $g$ is the weak gradient of $v$ against smooth test functions compactly supported in $\Omega$ . $\mu$ is the sInf of Rayleigh quotients over mean-zero nonzero $H^1$ functions; this set is nonempty and bounded below by $0$ .
InFirstNeumannEigenspace Ω u requires $u\in C^\infty(\overline\Omega)$ , mean zero, and the weak eigen-equation for all $H^1$ test pairs. The smoothness-up-to-the-boundary clause is a standard regularity fact for Neumann eigenfunctions on smooth domains (the preprint cites Showalter for it), so it does not exclude any eigenfunction.
The hypothesis $u\ne0$ is pointwise somewhere in $\Omega$ . The conclusion uses sInf/sSup of $u$ on frontier Ω, which is compact and nonempty, so these are the true minimum and maximum.
A vacuous reading is excluded: the eigenspace is nontrivial on every such domain (Rellich compactness), so the goal is a genuine statement about actual eigenfunctions.

Selected references

OpenAI, Strict hot spots and absence of interior critical points on smooth simply connected planar domains, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Strict-hot-spots-and-absence-of-interior-critical-points-on-smooth-simply-connected-planar-domains-September-24-2026/main.pdf
J. Rauch, Five problems: an introduction to the qualitative theory of partial differential equations, in Partial Differential Equations and Related Topics, LNM 446 (1975). https://doi.org/10.1007/BFb0070610
R. Bañuelos, K. Burdzy, On the "hot spots" conjecture of J. Rauch, J. Funct. Anal. 164 (1999). https://doi.org/10.1006/jfan.1999.3397
K. Burdzy, W. Werner, A counterexample to the "hot spots" conjecture, Ann. of Math. 149 (1999). https://doi.org/10.2307/121027
K. Burdzy, The hot spots problem in planar domains with one hole, Duke Math. J. 129 (2005), 481–502. https://doi.org/10.1215/S0012-7094-05-12932-5
D. Jerison, N. Nadirashvili, The "hot spots" conjecture for domains with two axes of symmetry, J. Amer. Math. Soc. 13 (2000), 741–772. https://doi.org/10.1090/S0894-0347-00-00346-5
R. Atar, K. Burdzy, On Neumann eigenfunctions in lip domains, J. Amer. Math. Soc. 17 (2004), 243–265. https://doi.org/10.1090/S0894-0347-04-00453-9
C. Judge, S. Mondal, Euclidean triangles have no hot spots, Ann. of Math. 191 (2020). https://doi.org/10.4007/annals.2020.191.1.3
J. Rohleder, A new approach to the hot spots conjecture, arXiv:2106.05224 (2021). https://arxiv.org/abs/2106.05224v4

14 thms2 active usersReviewed

Completed

Analysis Partial Differential Equations·Captain: wurtle

Nonuniqueness for bounded measurable scalar conductivities in three dimensionsResearch Paper

Motivation

Calderón's inverse conductivity problem asks whether the electrical conductivity inside a body is determined by voltage and current measurements on its boundary. Mathematically, a conductivity $\gamma$ on a domain $\Omega$ defines the elliptic equation $\operatorname{div}(\gamma\nabla u)=0$ , and the boundary data are encoded by the Dirichlet-to-Neumann (DN) operator $\Lambda_\gamma$ , which maps a boundary voltage to the resulting boundary current. The problem underlies electrical impedance tomography and is the model case of a large family of inverse boundary-value problems. Calderón (1980) posed it for bounded measurable conductivities bounded away from zero; how much regularity uniqueness requires has been a central question since.

Background

1974. Miller constructs elliptic divergence-form equations with nonunique continuation (doi:10.1007/BF00247634).
1980. Calderón poses the problem and proves injectivity of the linearization at constant conductivities.
1987. Sylvester and Uhlmann prove uniqueness for smooth conductivities in dimension $n\ge3$ (doi:10.2307/1971291).
2006. Astala and Päivärinta prove uniqueness for bounded measurable conductivities in the plane (doi:10.4007/annals.2006.163.265).
2015–2016. Haberman proves uniqueness for $W^{1,n}$ conductivities in dimensions three and four (doi:10.1007/s00220-015-2460-3); Caro and Rogers prove it for Lipschitz conductivities in all dimensions $n\ge3$ (doi:10.1017/fmp.2015.9).
2020. Daudé, Kamran and Nicoleau give anisotropic (matrix-valued) counterexamples with partial data, via nonunique continuation (doi:10.1017/fms.2020.1).

In dimension $n\ge3$ , uniqueness for merely bounded measurable scalar conductivities remained unresolved. The source of this mission is an OpenAI preprint dated September 23, 2026, which constructs a counterexample in dimension three.

Setting

Let $\Omega=B(0,3)\subset\mathbb R^3$ . A conductivity is a measurable $\gamma:\Omega\to\mathbb R$ with $0<c\le\gamma\le C$ almost everywhere. Let $H^1(\Omega)$ be the Sobolev space, $H^1_0(\Omega)$ the closure of compactly supported smooth functions, and $H^{1/2}(\partial\Omega)\cong H^1(\Omega)/H^1_0(\Omega)$ the trace space, with dual $H^{-1/2}(\partial\Omega)$ . For a trace $f$ , let $u_f\in H^1(\Omega)$ be the unique function with trace $f$ such that

\int_\Omega\gamma\,\nabla u_f\cdot\nabla\varphi\,dx=0\qquad(\varphi\in H^1_0(\Omega)).

The DN operator $\Lambda_\gamma:H^{1/2}(\partial\Omega)\to H^{-1/2}(\partial\Omega)$ is

\langle\Lambda_\gamma f,g\rangle=\int_\Omega\gamma\,\nabla u_f\cdot\nabla v\,dx,\qquad \operatorname{Tr}v=g.

Formalization targets

Goal: Theorem 1.1

There are $\gamma_0,\gamma_1\in L^\infty(B(0,3))$ and $0<c<C$ with

c\le\gamma_j\le C\ \text{a.e.},\qquad \gamma_j=1\ \text{near }\partial B(0,3),\qquad |\{\gamma_0\ne\gamma_1\}|>0,\qquad \Lambda_{\gamma_0}=\Lambda_{\gamma_1}.

The Lean statement OAI.ScalarConductivity.main_nonuniqueness is open on the platform.

Significance

The theorem shows that scalar Calderón uniqueness fails in the bounded measurable class in dimension three, in contrast with the planar theorem of Astala–Päivärinta and the Lipschitz and $W^{1,n}$ uniqueness results in higher dimensions. It locates the regularity threshold for uniqueness strictly between $L^\infty$ and the known positive classes. By Corollary 1.2, counterexamples can be localized: any finite family of disjoint balls inside any Lipschitz domain supports $2^m$ distinct conductivities with the same DN map.

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

Difficulty

Matrix-valued counterexamples exist, but they do not transfer to scalar conductivities: scalar coefficients can approximate matrix ones only in the sense of $G$ - or $H$ -convergence, and Rondi's example shows that exact realization of a full boundary map by a scalar coefficient can fail. Moreover, Daudé–Kamran–Nicoleau note an obstruction for full-boundary data: a weakly harmonic factor with constant full boundary trace is constant. One must therefore match the entire DN operator (every boundary input) exactly, with a scalar coefficient, and with uniform ellipticity bounds; the paper does so with a nested family of scalar blocks realizing prescribed current triples exactly.

Formalization scope

$H^1(B(0,3))$ is the closure, in $L^2(B;\mathbb R^4)$ , of the jets $(f,\nabla f)$ of smooth $f$ ; $H^1_0$ is the closure of jets of smooth $f$ with compact support in the ball; the trace space is the quotient and the DN operator is a continuous linear map into its continuous dual.
IsDirichletToNeumann γ Λ requires existence and uniqueness of the weak $\gamma$ -harmonic extension of every trace and the weak flux identity against every $v\in H^1$ .
EqualOneNearBoundary asks for $r<3$ with $\gamma=1$ a.e. on $\{r<|x|<3\}$ ; bounds and measurability are stated almost everywhere on the ball.

A complete development needs Sobolev spaces on a ball, weak solutions of divergence-form equations (Lax–Milgram), trace spaces, and the paper's block constructions (convex-integration-type scalarization). Contributions formalizing Theorem 3.1 (exact finite-field scalarization), Proposition 4.1 (branching block) and Corollary 1.2 are welcome.

Selected references

OpenAI, Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026/paper.pdf
A. P. Calderón, On an inverse boundary value problem, Seminar on Numerical Analysis and its Applications to Continuum Physics, Rio de Janeiro, 1980.
J. Sylvester, G. Uhlmann, A global uniqueness theorem for an inverse boundary value problem, Ann. of Math., 1987. https://doi.org/10.2307/1971291
K. Astala, L. Päivärinta, Calderón's inverse conductivity problem in the plane, Ann. of Math., 2006. https://doi.org/10.4007/annals.2006.163.265
P. Caro, K. M. Rogers, Global uniqueness for the Calderón problem with Lipschitz conductivities, Forum Math. Pi, 2016. https://doi.org/10.1017/fmp.2015.9
B. Haberman, Uniqueness in Calderón's problem for conductivities with unbounded gradient, Comm. Math. Phys., 2015. https://doi.org/10.1007/s00220-015-2460-3
T. Daudé, N. Kamran, F. Nicoleau, On nonuniqueness for the anisotropic Calderón problem with partial data, Forum Math. Sigma, 2020. https://doi.org/10.1017/fms.2020.1

6 thms2 active usersReviewed

Analysis Mathematical Physics Partial Differential Equations·Captain: wurtle

Nonuniqueness for the periodic hard-sphere Boltzmann equationResearch Paper

Motivation: uniqueness of weak Boltzmann solutions

The Boltzmann equation describes a dilute gas through a density $F(t,x,v)$ of particles at position $x$ with velocity $v$ , evolving by free transport and binary collisions. For hard spheres, the collision rate is proportional to the normal relative speed. In 1989 DiPerna and Lions constructed global renormalized solutions for all initial data with finite mass, energy and entropy, and weak stability holds at the same level. Existence and stability do not give uniqueness, though: the physical bounds do not even make the quadratic collision term locally integrable, and the uniqueness of general renormalized solutions is a basic question in kinetic theory (Silvestre 2022, §2). Uniqueness is known only under much stronger assumptions, such as Maxwellian upper bounds or closeness to equilibrium.

Timeline

1974 — Ukai: global existence and uniqueness near a Maxwellian for periodic cutoff hard potentials (Proc. Japan Acad. 1974).
1978 — Kaniel and Shinbrot: uniqueness and local existence under Maxwellian upper bounds (CMP 1978).
1988 — Golse, Lions, Perthame and Sentis: velocity averaging lemmas (JFA 1988).
1989 — DiPerna and Lions: global renormalized solutions and weak stability (Ann. of Math. 1989); the entropy inequality follows in 1991 (ARMA 1991).
1999 — For the spatially homogeneous hard-sphere equation, Mischler and Wennberg prove uniqueness among conservative solutions with finite mass and energy (Ann. IHP C 1999); Wennberg gives homogeneous nonuniqueness examples in which the energy increases (J. Stat. Phys. 1999).
2010 — Levermore and Masmoudi give a periodic formulation of renormalized solutions relative to a Maxwellian (ARMA 2010).
2024–2026 — Ill-posedness results: Chen–Holmer for the constant kernel (Ann. PDE 2024), Chen–Guo–Shen–Zhang for hard spheres in Gaussian-weighted $L^2_vH^s_x$ (arXiv:2606.01331). Gismondi, Golding and Novack conjecture nonuniqueness of renormalized inhomogeneous Landau and Boltzmann solutions for a dense class of data (arXiv:2608.13758).
2026 — An OpenAI preprint, Nonuniqueness for the periodic hard-sphere Boltzmann equation (OpenAI Math Release, September 23, 2026), claims a single finite-entropy datum on $\mathbb T^3\times\mathbb R^3$ with two distinct admissible solutions. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Phase space is $\Omega=\mathbb T^3_x\times\mathbb R^3_v$ , with $\mathbb T^3=\mathbb R^3/\mathbb Z^3$ . For incoming velocities $v,v_*$ and a collision normal $\omega\in S^2$ , put $a=(v-v_*)\cdot\omega$ , $v'=v-a\omega$ , $v_*'=v_*+a\omega$ . The hard-sphere collision operator is

Q(F,F)(v)=\int_{\mathbb R^3\times S^2}|a|\,\big(F(v')F(v_*')-F(v)F(v_*)\big)\,dv_*\,d\omega ,

with ordinary surface measure on $S^2$ ; the two terms are the gain and the loss. The Cauchy problem is $(\partial_t+v\cdot\nabla_x)F=Q(F,F)$ , $F(0)=F_0$ . An initial datum has finite entropy if it is nonnegative and $\int_\Omega F_0(1+|v|^2+|\log F_0|)<\infty$ .

A solution is admissible (Definition 2.1 of the source) if, with $M(v)=(2\pi)^{-3/2}e^{-|v|^2/2}$ :

it is renormalized: the equation holds weakly for $M\beta(F/M)$ for every $C^1$ $\beta$ with $\beta(0)=0$ and $|\beta'(z)|\le C_\beta/(1+z)$ , and the separately renormalized gain and loss are integrable on bounded time intervals;
it is weakly continuous in $L^1$ against every bounded measurable test and takes the initial value $F_0$ ;
mass, energy and absolute entropy stay bounded on bounded time intervals;
it conserves local mass and total momentum, and satisfies the energy inequality and the relative-entropy inequality with the full entropy dissipation at every time.

Formalization targets

Goal: two admissible solutions from one datum (Theorem 1.1)

There is a nonnegative finite-entropy datum $F_0$ with bounded velocity support, two admissible global solutions $F,G$ with initial datum $F_0$ , and a time $T>0$ such that

F,G\in C([0,T];L^1(\Omega)),\qquad Q^\pm(F),\,Q^\pm(G)\in L^1([0,T]\times\Omega),\qquad F(t)\neq G(t)\ \text{in } L^1 \text{ for some } t\in[0,T].

This is Theorem 1.1 of the source (p. 3), with the difference placed in the common interval of strong continuity, which is where the source establishes it. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem shows that the DiPerna–Lions framework, even with local mass conservation, momentum conservation and the energy and entropy inequalities retained, does not determine the evolution uniquely. The example is spatially inhomogeneous and periodic, and the two solutions start from exactly the same datum, unlike ill-posedness results that compare nearby data. On the interval where they differ, both solutions satisfy the unrenormalized equation. The datum has bounded velocities but unbounded amplitudes concentrated at smaller and smaller spatial scales, which points to the kind of extra control a uniqueness theorem has to impose.

Formalizing it. The statement fixes a long list of admissibility conditions. Its definitions are a useful contribution in their own right: renormalized solutions, entropy dissipation and kinetic test functions on the torus are not in Mathlib. The 65-page proof (colored decompositions, Carleman representation, velocity averaging, a dilation limit and a branching analysis) is a long-term target. Its propositions are natural milestones.

Difficulty

Constructing two different weak limits is not the hard part: approximations with and without a small "hot seed" give two candidate solutions. The difficulty is to show that they really differ. A vanishing seed can produce a hit on the a priori cap that carries arbitrarily little mass, and weak compactness can erase it in the limit. The source must rule out this loss of information uniformly as the cold velocity distributions collapse onto an axis, where the weight controlling the hot density is singular. At the same time every admissibility condition, including the entropy-dissipation inequality and local mass conservation, has to survive the limits. Energy-increasing constructions (Wennberg) and homogeneous examples do not meet these constraints.

Formalization scope

Velocities live in EuclideanSpace ℝ (Fin 3), positions in Fin 3 → AddCircle 1, and densities are real functions on phase space. The sphere carries (volume).toSphere, which is ordinary surface area, not a probability measure.
gain and loss are Bochner integrals. To prevent them from silently returning $0$ on non-integrable fibers, AdmissibleGlobal requires fiberwise integrability and space-time integrability of the renormalized gain and loss.
AdmissibleGlobal f₀ F encodes Definition 2.1: finite entropy at each time, a.e. initial value, weak continuity against bounded measurable tests, uniform moment bounds, the renormalized equation for all Renormalization $\beta$ and all smooth periodic KineticTest $\varphi$ , local mass conservation against MassTest, total momentum conservation, the energy inequality, and the entropy inequality in ℝ≥0∞ with the lower semicontinuous extension of $(A-B)\log(A/B)$ .
StrongEarly T F adds $T>0$ , strong $L^1$ continuity on $[0,T]$ via eLpNorm, and integrability of gain and loss on $[0,T]$ . Distinctness is ¬ (F t =ᵐ G t) for some $t\in[0,T]$ .
Infrastructure needed: averaging lemmas, renormalized-solution compactness, the Carleman representation, and estimates on free transport on the torus. Contributions to any of these are welcome.

Selected references

R. J. DiPerna and P.-L. Lions, On the Cauchy problem for Boltzmann equations: global existence and weak stability, Ann. of Math. 130 (1989), 321–366. https://doi.org/10.2307/1971423
R. J. DiPerna and P.-L. Lions, Global solutions of Boltzmann's equation and the entropy inequality, Arch. Ration. Mech. Anal. 114 (1991), 47–55. https://doi.org/10.1007/BF00375684
C. D. Levermore and N. Masmoudi, From the Boltzmann equation to an incompressible Navier–Stokes–Fourier system, Arch. Ration. Mech. Anal. 196 (2010), 753–809. https://doi.org/10.1007/s00205-009-0254-5
L. Silvestre, Regularity estimates and open problems in kinetic equations, arXiv:2204.06401 (2022). https://doi.org/10.48550/arXiv.2204.06401
S. Kaniel and M. Shinbrot, The Boltzmann equation. I. Uniqueness and local existence, Comm. Math. Phys. 58 (1978), 65–84. https://doi.org/10.1007/BF01624788
S. Ukai, On the existence of global solutions of mixed problem for non-linear Boltzmann equation, Proc. Japan Acad. 50 (1974), 179–184. https://doi.org/10.3792/pja/1195519027
S. Mischler and B. Wennberg, On the spatially homogeneous Boltzmann equation, Ann. Inst. H. Poincaré C 16 (1999), 467–501. https://doi.org/10.1016/S0294-1449(99)80025-0
B. Wennberg, An example of nonuniqueness for solutions to the homogeneous Boltzmann equation, J. Stat. Phys. 95 (1999), 469–477. https://doi.org/10.1023/A:1004546031908
F. Golse, P.-L. Lions, B. Perthame and R. Sentis, Regularity of the moments of the solution of a transport equation, J. Funct. Anal. 76 (1988), 110–125. https://doi.org/10.1016/0022-1236(88)90051-1
X. Chen and J. Holmer, Well/ill-posedness bifurcation for the Boltzmann equation with constant collision kernel, Ann. PDE 10 (2024), Art. 14. https://doi.org/10.1007/s40818-024-00177-w
X. Chen, Y. Guo, S. Shen and Z. Zhang, Sharp $H^s_x$ ill-posedness of the hard-sphere Boltzmann equation, arXiv:2606.01331 (2026). https://doi.org/10.48550/arXiv.2606.01331
N. Gismondi, W. Golding and M. Novack, A sharp rigidity/flexibility threshold for the isotropic Landau equation, arXiv:2608.13758 (2026). https://doi.org/10.48550/arXiv.2608.13758
OpenAI, Nonuniqueness for the periodic hard-sphere Boltzmann equation, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 3; Definition 2.1, p. 8). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026/paper.pdf

4 thms2 active usersReviewed

Completed

Mathematical Physics Partial Differential Equations·Captain: wurtle

Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell systemResearch Paper

Motivation

The relativistic Vlasov–Maxwell system is the basic kinetic model of a collisionless plasma: a cloud of charged particles, described by a phase-space density, moves under the electromagnetic field it generates, and the field evolves by Maxwell's equations with the particles as sources. Whether smooth, compactly supported data in three dimensions always produce a solution that stays smooth for all time has been the central question about the Cauchy problem for this system since the 1980s. Weak solutions exist globally, but they come without regularity or uniqueness, and every previous global classical result required smallness, a dimensional reduction, symmetry, or a nearby global reference solution.

This mission asks for a machine-checked proof of global existence and uniqueness of classical solutions for arbitrary smooth admissible data, as claimed in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

1984 — Wollman proves local existence and uniqueness of classical solutions (CPAM 1984).
1986 — Glassey and Strauss show that a classical solution continues as long as the momentum support stays bounded (ARMA 1986); in 1987 they prove global existence for initially dilute plasmas (CMP 1987).
1985–1998 — Glassey and Schaeffer obtain global classical solutions for symmetric relativistic Vlasov–Poisson (CMP 1985) and for reduced Vlasov–Maxwell models in one and one-half, two and one-half, and two dimensions (1990, 1997, 1998).
1989 — DiPerna and Lions prove global existence of weak solutions for large data (CPAM 1989); Rein treats the relativistic case directly (CMS 2004).
1990 — Rein proves stability of global existence near suitable global solutions (CMP 1990).
2002–2003 — New proofs of the continuation criterion by Klainerman–Staffilani (CPAA 2002) and Bouchut–Golse–Pallard (ARMA 2003).
2004–2016 — Refined continuation criteria: Schaeffer's small-data theorem with momentum tails (IUMJ 2004), Pallard (IUMJ 2005), Luk and Strain's two-dimensional projection criterion (CMP 2014) and moment bounds (ARMA 2016).
2020–2025 — Small-particle global results with large fields: Bigorgne (CMP 2020; APDE 2025), Wei–Yang (CMP 2021).
2026 — Wang establishes large-data global existence under cylindrical symmetry (arXiv:2203.01199, arXiv:2607.14685).
September 2026 — The OpenAI preprint claims the general large-data result without symmetry (Theorem 1.1, p. 3).

Setting

For momentum $v\in\mathbb R^3$ let $q(v)=\sqrt{1+|v|^2}$ and $u(v)=v/q(v)$ (the relativistic velocity, $|u|<1$ ). The unknowns are a particle density $f(t,x,v)\ge0$ and fields $E(t,x),B(t,x)\in\mathbb R^3$ , with charge and current densities $\rho_f=\int f\,dv$ and $j_f=\int u(v)f\,dv$ . In the one-species normalization the system is

\partial_tf+u(v)\cdot\nabla_xf+(E+u(v)\times B)\cdot\nabla_vf=0,

\partial_tE-\nabla_x\times B=-j_f,\qquad \partial_tB+\nabla_x\times E=0,\qquad \nabla_x\cdot E=\rho_f,\qquad \nabla_x\cdot B=0 .

A smooth admissible datum $(f_0,E_0,B_0)$ has $f_0\in C_c^\infty(\mathbb R^3_x\times\mathbb R^3_v)$ , $f_0\ge0$ , $E_0,B_0$ smooth with every derivative bounded and $E_0,B_0\in L^2$ , and satisfies $\nabla\cdot E_0=\rho_{f_0}$ , $\nabla\cdot B_0=0$ . A classical solution on $[0,\infty)$ is a $C^1$ triple solving the system pointwise, with $E,B$ continuous in time with values in $L^2$ , and with $f(t,\cdot,\cdot)$ supported in a fixed compact set on each bounded time interval.

Formalization targets

Goal: Theorem 1.1 (p. 3)

Every smooth admissible datum generates a classical solution on $[0,\infty)$ with the given initial values; for every finite $T$ the solution is $C^\infty$ on $[0,T]\times\mathbb R^6$ (respectively $[0,T]\times\mathbb R^3$ for the fields) with compact phase-space support on $[0,T]$ ; and any other classical solution with the same datum agrees with it at every $t\ge0$ . This is OAI.RVM.global_classical_solution.

Significance

The result itself. It settles the large-data global classical regularity problem for three-dimensional relativistic Vlasov–Maxwell, with no size, symmetry or neutrality assumption; nonzero total charge with its Coulomb tail is allowed. Global well-posedness at this level is the starting point for questions about long-time behaviour, scattering and stability of plasma equilibria that previously could only be posed for small or symmetric data.

Formalizing it. The proof combines the Glassey–Strauss representation of fields along backward light cones, energy-flux estimates, a delicate signed bootstrap, and local well-posedness and continuation theory. None of this PDE infrastructure (wave-equation representation formulas, characteristics of transport equations in phase space, Sobolev local theory) is currently available in a proof assistant at the needed level, so each component is reusable.

Difficulty

By the Glassey–Strauss criterion it suffices to bound the momentum support on finite time intervals. The natural approach estimates the absolute value of the force along a characteristic using the retarded field representation and energy flux through light cones. At receiver energy $w$ this loses a factor $\sqrt w$ relative to what is needed (Section 1.2, p. 4); the loss comes from sources whose velocity is much closer to the light ray than the receiver's. The preprint instead estimates the signed momentum increment $V_X(t_2)-V_X(t_1)$ , integrating the retarded force along source trajectories before taking norms (Proposition 2.1, p. 5; Lemma 6.1, p. 24), controls direction changes (Lemma 7.1, p. 29), and closes a bootstrap whose time-to-double lower bounds have a divergent sum (Section 9).

Formalization scope

Space and momentum are EuclideanSpace ℝ (Fin 3); derivatives are Fréchet derivatives in coordinate directions; the time derivative is derivWithin on $[0,\infty)$ , so $t=0$ is one-sided.
Admissible encodes $C^\infty$ with compact support and nonnegativity for $f_0$ ; ContDiff ℝ ∞ with all iterated derivatives bounded and MemLp 2 for $E_0,B_0$ ; and both Gauss constraints pointwise.
Classical requires $C^1$ regularity on the closed half-spaces, $f\ge0$ , continuity of $t\mapsto E(t),B(t)$ into $L^2$ on $[0,\infty)$ , compact phase support on each $[0,T]$ , all five equations pointwise for $t\ge0$ (including both constraints), and the initial values.
The conclusion asserts existence, smoothness on every finite horizon, and uniqueness within the same classical class; uniqueness is pointwise equality at all $t\ge0$ . The hypotheses are satisfiable (e.g. $f_0=0$ , $E_0=B_0=0$ ), so the statement is not vacuous.
$\rho$ and $j$ are Bochner integrals in $v$ ; for compactly supported $f$ these are the genuine moments.

Selected references

OpenAI, Global classical solutions of the three-dimensional relativistic Vlasov–Maxwell system, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-classical-solutions-of-the-three-dimensional-relativistic-Vlasov-Maxwell-system-September-23-2026/paper.pdf
R. T. Glassey, W. A. Strauss, Singularity formation in a collisionless plasma could occur only at high velocities, Arch. Ration. Mech. Anal. 92 (1986). https://doi.org/10.1007/BF00250732
R. T. Glassey, W. A. Strauss, Absence of shocks in an initially dilute collisionless plasma, Comm. Math. Phys. 113 (1987). https://doi.org/10.1007/BF01223511
S. Wollman, An existence and uniqueness theorem for the Vlasov–Maxwell system, Comm. Pure Appl. Math. 37 (1984). https://doi.org/10.1002/cpa.3160370404
R. J. DiPerna, P.-L. Lions, Global weak solutions of Vlasov–Maxwell systems, Comm. Pure Appl. Math. 42 (1989). https://doi.org/10.1002/cpa.3160420603
J. Luk, R. M. Strain, A new continuation criterion for the relativistic Vlasov–Maxwell system, Comm. Math. Phys. 331 (2014). https://doi.org/10.1007/s00220-014-2108-8
F. Bouchut, F. Golse, C. Pallard, Classical solutions and the Glassey–Strauss theorem for the 3D Vlasov–Maxwell system, Arch. Ration. Mech. Anal. 170 (2003). https://doi.org/10.1007/s00205-003-0265-6
S. Klainerman, G. Staffilani, A new approach to study the Vlasov–Maxwell system, Commun. Pure Appl. Anal. 1 (2002). https://doi.org/10.3934/cpaa.2002.1.103
X. Wang, Large data global solution of the 3D RVM system with cylindrical symmetry, arXiv:2203.01199 and arXiv:2607.14685 (2026). https://arxiv.org/abs/2607.14685v1

5 thms2 active usersReviewed

Completed

Differential Geometry Optimal Transport Partial Differential Equations·Captain: wurtle

Global Support and Convex Injectivity Domains under Weak MTWResearch Paper

Motivation: curvature conditions in optimal transport on manifolds

In optimal transport on a Riemannian manifold with the quadratic cost $c(x,y)=d(x,y)^2/2$ , the regularity of optimal maps is governed by a fourth-order curvature quantity of the cost, the Ma–Trudinger–Wang (MTW) tensor. Its nonnegativity on orthogonal pairs, the weak MTW condition (A3w), is necessary for continuity of optimal maps, and together with convexity of the tangent injectivity domains it yields the global geometric "supporting" properties used in regularity theory. Whether weak MTW by itself forces those injectivity domains to be convex was proposed by Villani and proved previously only under a nonfocality assumption, which excludes cut points that are also conjugate points.

Background

2005 — Ma, Trudinger and Wang introduce a strictly positive curvature condition for regularity of transport potentials (MTW 2005).
2009 — Trudinger and Wang treat the degenerate nonnegative form A3w (TW 2009); Loeper proves necessity for continuity and the supporting-mountain principle (Loeper 2009).
2010 — Loeper and Villani connect MTW to cut-locus geometry, proving convexity under strong MTW and nonfocality (Loeper–Villani 2010); Kim and McCann give a geometric formulation and a double-mountain principle (Kim–McCann 2010); Figalli's Bourbaki survey (Astérisque 332, 2010).
2011 — Figalli, Rifford and Villani derive the global supporting principle from weak MTW plus convex injectivity domains (FRV 2011); Villani proposes that weak MTW alone should force convexity of every tangent injectivity domain (Villani 2011, §4.2).
2015 — Figalli, Gallouët and Rifford prove that implication on nonfocal manifolds (FGR 2015, Thm 1.7).
2026 — An OpenAI preprint, Global Support and Convex Injectivity Domains under Weak MTW (OpenAI Math Release, September 25, 2026), claims the implication on every smooth compact connected Riemannian manifold of dimension $n\ge2$ , with conjugate cut points allowed. It has not been peer reviewed and its theorems are not formally verified.

Setting

Let $(M,g)$ be a smooth, connected, compact Riemannian manifold without boundary, of dimension $n\ge2$ , with geodesic distance $d$ and exponential map $\exp_x:T_xM\to M$ . The open tangent injectivity domain at $x$ is

I(x)=\{v\in T_xM:\ d(x,\exp_x(av))=a|v|_x\ \text{for some } a>1\},

the set of velocities whose geodesic is still minimizing slightly beyond time one. With $c(x,y)=d(x,y)^2/2$ , the MTW quantity at $v\in I(x)$ is

\mathfrak S_{(x,v)}(\xi,\eta)=-\frac32\,\frac{\partial^4}{\partial s^2\,\partial t^2}\,c\big(\exp_x(t\xi),\exp_x(v+s\eta)\big)\Big|_{s=t=0},

and weak MTW means $\mathfrak S_{(x,v)}(\xi,\eta)\ge0$ whenever $\langle\xi,\eta\rangle_x=0$ , for all $x$ and $v\in I(x)$ . No nonfocality, strict positivity, or prior convexity is assumed.

In Lean, $M$ is a Mathlib Riemannian manifold modelled on EuclideanSpace ℝ (Fin n) (so without boundary), with CompactSpace, ConnectedSpace and IsRiemannianManifold linking the metric-space distance to the Riemannian metric. exp x v is the time-one point of a smooth curve with initial point $x$ , initial velocity $v$ , and locally constant-speed distance-realizing behaviour; mtw is the iterated one-variable derivative formula above.

Formalization targets

Goal: convexity of injectivity domains

If $(M,g)$ satisfies weak MTW, then for every $x\in M$ , every $v_0,v_1\in I(x)$ and $\theta\in[0,1]$ ,

(1-\theta)v_0+\theta v_1\in I(x),

i.e. $I(x)$ is convex. This is Theorem 1.1 of the source. The goal is published on the platform with status Open.

Significance

The result itself. Combined with the Figalli–Rifford–Villani supporting principle, convexity of injectivity domains under weak MTW alone removes an extra geometric hypothesis from the regularity theory of optimal transport on compact manifolds, and covers focal manifolds where minimizing geodesics may reach conjugate cut points. The source also proves a global supporting property, convexity of lifted gap sections, and uniform $C^{1,1}$ intermediate-time geometry (Theorem 1.2), which feed the companion preprint on bi-Hölder regularity of transport maps.

Formalizing it. The statement uses only geodesics, distance and a four-fold derivative of the squared distance, so it can be phrased with current Mathlib Riemannian infrastructure. A proof needs nonsmooth analysis of the distance function near the cut locus, semiconvex potentials and their subdifferentials, and a continuity (degree) argument; this layer would be reusable for other cut-locus results.

Difficulty

The cost $c$ is smooth only before the cut locus, while convexity of $I(x)$ concerns segments whose interior points might a priori leave the region where $\mathfrak S$ is defined. Weak MTW controls the cost Hessian only in directions perpendicular to a velocity segment and gives no strict inequality. Smooth-cost concavity arguments therefore cannot be applied beyond their domain, and nonfocality — the assumption that cut points are reached strictly before conjugate points — is exactly what earlier proofs used to keep the cost smooth along the segment.

Formalization scope

exp is defined through complete geodesics with prescribed initial data (ContMDiff curve, mfderiv at $0$ equal to $v$ , locally $d(\gamma s,\gamma r)=|v|\,|s-r|$ ); on a compact manifold such a geodesic exists and is unique, so the Classical.choose fallback is never used.
injectivityDomain matches $I(x)$ exactly; mtw uses iterated deriv, which is the true fourth derivative wherever the cost is smooth (the case $v\in I(x)$ , near $s=t=0$ ).
The hypothesis quantifies over all $x$ , all $v\in I(x)$ , and all $g_x$ -orthogonal $\xi,\eta$ ; the conclusion is Convex ℝ (injectivityDomain x) for every $x$ .
Dimension $n\ge2$ , compactness and connectedness are explicit hypotheses; boundaryless-ness comes from the Euclidean model.
Needed infrastructure: Hopf–Rinow and uniqueness of geodesics, first and second variation, semiconcavity of the distance squared, cut and conjugate locus theory.

Selected references

X.-N. Ma, N. S. Trudinger and X.-J. Wang, Regularity of potential functions of the optimal transportation problem, Arch. Ration. Mech. Anal. 177 (2005), 151–183. https://doi.org/10.1007/s00205-005-0362-9
N. S. Trudinger and X.-J. Wang, On the second boundary value problem for Monge–Ampère type equations and optimal transportation, Ann. Sc. Norm. Super. Pisa 8 (2009), 143–174. https://doi.org/10.2422/2036-2145.2009.1.07
G. Loeper, On the regularity of solutions of optimal transportation problems, Acta Math. 202 (2009), 241–283. https://doi.org/10.1007/s11511-009-0037-8
G. Loeper and C. Villani, Regularity of optimal transport in curved geometry: the nonfocal case, Duke Math. J. 151 (2010), 431–485. https://doi.org/10.1215/00127094-2010-003
Y.-H. Kim and R. J. McCann, Continuity, curvature, and the general covariance of optimal transportation, J. Eur. Math. Soc. 12 (2010), 1009–1040. https://doi.org/10.4171/JEMS/221
A. Figalli, Regularity of optimal transport maps [after Ma–Trudinger–Wang and Loeper], Séminaire Bourbaki 2008/2009, Astérisque 332 (2010), 341–368.
A. Figalli, L. Rifford and C. Villani, Necessary and sufficient conditions for continuity of optimal transport maps on Riemannian manifolds, Tohoku Math. J. 63 (2011), 855–876. https://doi.org/10.2748/tmj/1325886291
C. Villani, Regularity of optimal transport and cut locus: from nonsmooth analysis to geometry to smooth analysis, Discrete Contin. Dyn. Syst. 30 (2011), 559–571. https://doi.org/10.3934/dcds.2011.30.559
A. Figalli, T. O. Gallouët and L. Rifford, On the convexity of injectivity domains on nonfocal manifolds, SIAM J. Math. Anal. 47 (2015), 969–1000. https://doi.org/10.1137/140961821
OpenAI, Global Support and Convex Injectivity Domains under Weak MTW, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf

19 thms2 active usersReviewed

Completed

Differential Geometry Geometry & Topology·Captain: wurtle

A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved MetricResearch Paper

Motivation

Along a geodesic of a Riemannian manifold, a Jacobi field describes how nearby geodesics spread apart. Two points of a geodesic are conjugate if some nonzero Jacobi field vanishes at both; a metric has no conjugate points if this never happens. Nonpositive sectional curvature implies no conjugate points (by the Rauch comparison), and the two conditions share many consequences: the universal cover is diffeomorphic to $\mathbb R^n$ via the exponential map, and the fundamental group controls the geometry. For a single metric the converse fails: Gulliver (1975) produced metrics without conjugate points that have regions of positive curvature. The existence question is subtler: must a closed manifold that carries some metric without conjugate points also carry some metric of nonpositive curvature? Ivanov and Kapovitch (2014) and the Burns–Matveev survey (2021) ask this, explicitly including dimension three.

Background

1963. Milnor's Morse Theory develops the index-form framework for conjugate points.
1975. Gulliver shows that absence of conjugate points does not force nonpositive curvature for an individual metric (doi:10.1090/S0002-9947-1975-0383294-0).
1995. Leeb characterizes 3-manifolds with nonpositively curved metrics and gives two-piece graph-manifold obstructions (doi:10.1007/BF01231445).
1996. Kapovich and Leeb study discrete group actions on nonpositively curved spaces (doi:10.1007/BF01445254).
2014. Ivanov and Kapovitch ask the existence question (Questions 1.1, 8.1), single out graph manifolds glued from punctured-torus products, and prove that a closed 3-manifold has a metric without focal points iff it has one of nonpositive curvature (doi:10.4310/jdg/1393424918).
2021. Burns and Matveev list the question (Question 4.1.2) (doi:10.1017/etds.2019.73).

In dimension two the answer is positive (Euler characteristic and uniformization), so dimension three is the first case. The source of this mission is an OpenAI preprint dated September 24, 2026, which answers the question negatively in dimension three.

Setting

Let $M$ be a closed (compact, boundaryless) connected smooth 3-manifold with a smooth Riemannian metric $g$ . In a chart, with Christoffel symbols $\Gamma^i_{jk}$ , a curve $\gamma$ is a geodesic if $\ddot\gamma^i+\Gamma^i_{jk}\dot\gamma^j\dot\gamma^k=0$ . With covariant derivative $D_s$ along $\gamma$ and curvature $R(X,Y)Z=\nabla_X\nabla_YZ-\nabla_Y\nabla_XZ-\nabla_{[X,Y]}Z$ , a Jacobi field is a smooth vector field $J$ along $\gamma$ with

D_s^2J+R(J,\dot\gamma)\dot\gamma=0.

$g$ has no conjugate points if every Jacobi field vanishing at two distinct times vanishes identically. $g$ has nonpositive sectional curvature if $g(R(u,v)v,u)\le0$ for all tangent vectors $u,v$ .

Formalization targets

Goal: Theorem 1.1

\exists\,M\ \text{closed, connected, orientable smooth 3-manifold}:\quad \exists\,g\ \text{without conjugate points},\quad \nexists\,g'\ \text{with } \sec_{g'}\le0.

The Lean statement OAI.ThreeManifold.main_theorem is open on the platform.

Significance

The theorem shows that, starting in dimension three, the existence of a metric without conjugate points is strictly weaker than the existence of a nonpositively curved metric, answering the Ivanov–Kapovitch question. The same manifold carries no locally CAT(0) length metric and, by the Ivanov–Kapovitch equivalence, no metric without focal points, so it separates "no conjugate points" from "no focal points" as well. The example is a graph manifold glued from two copies of (punctured torus) $\times S^1$ , exactly the test case Ivanov and Kapovitch proposed.

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

Difficulty

Two separate problems must be solved. The obstruction side (no nonpositively curved metric) follows from Leeb's graph-manifold criterion and is group-theoretic. The construction side is analytic: one must build a metric across the gluing neck and prove that every complete geodesic, including those that enter and leave the neck infinitely often at arbitrary angles, has no conjugate points. Nonpositive curvature is not available in the neck, so the Rauch comparison does not apply; the index form must be controlled with endpoint terms uniformly in entry angle, turning height and excursion time.

Formalization scope

Manifolds are ChartedSpace (Fin 3 → ℝ) with IsManifold 𝓘(ℝ, Fin 3 → ℝ) ∞, compact, connected, Hausdorff, second countable; orientability is OrientedAtlas (all transition maps have positive Jacobian determinant).
Metrics are ContMDiffRiemannianMetric; Christoffel symbols and curvature are computed in every atlas chart from fderiv of the coordinate metric.
IsGeodesicOn g γ U asks for a smooth curve satisfying the geodesic equation in every chart on the open interval U; IsJacobiFieldOn asks for chart-smooth fields satisfying the Jacobi equation.
NoConjugatePoints g: for every open interval U, geodesic and Jacobi field on U, vanishing at two distinct times forces vanishing on U.
NonpositiveSectionalCurvature g: $g(R(u,v)v,u)\le0$ for all chart points and vectors; the goal asserts no smooth metric on the same smooth manifold has this property.

A complete development needs Riemannian geometry in coordinates, geodesic flows and Jacobi fields, the index form, Cartan–Hadamard/flat torus theorems and the group theory of graph manifolds. Contributions formalizing Theorem 2.1 (no proper cocompact CAT(0) action), Lemma 6.2 (index-form criterion) and Proposition 6.1 (assembly of passage estimates) are welcome.

Selected references

OpenAI, A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Three-Manifold-Without-Conjugate-Points-and-Without-a-Nonpositively-Curved-Metric-September-24-2026/paper.pdf
S. Ivanov, V. Kapovitch, Manifolds without conjugate points and their fundamental groups, J. Differential Geom., 2014. https://doi.org/10.4310/jdg/1393424918
K. Burns, V. S. Matveev, Open problems and questions about geodesics, Ergodic Theory Dynam. Systems, 2021. https://doi.org/10.1017/etds.2019.73
R. Gulliver, On the variety of manifolds without conjugate points, Trans. Amer. Math. Soc., 1975. https://doi.org/10.1090/S0002-9947-1975-0383294-0
B. Leeb, 3-manifolds with(out) metrics of nonpositive curvature, Invent. Math., 1995. https://doi.org/10.1007/BF01231445
M. Kapovich, B. Leeb, Actions of discrete groups on nonpositively curved spaces, Math. Ann., 1996. https://doi.org/10.1007/BF01445254
J. Milnor, Morse Theory, Princeton University Press, 1963.

31 thms2 active usersReviewed

Completed

Analysis Differential Geometry Optimal Transport·Captain: wurtle

Weak Hessian bounds along every geodesic in RCD spacesResearch Paper

Motivation: from weak Hessian bounds to every geodesic

On a smooth Riemannian manifold, an upper bound $\nabla^2F\le G\,g$ on the Hessian of a function $F$ immediately bounds the second derivative of $F$ along every geodesic: $(F\circ\sigma)''\le|\dot\sigma|^2\,G\circ\sigma$ . In non-smooth geometry this step breaks down. On metric measure spaces with Ricci curvature bounded below in the synthetic sense — the $\mathrm{RCD}(K,N)$ spaces — Hessians exist only weakly: inequalities are tested against the reference measure $m$ , whereas a single prescribed geodesic can lie in a set of measure zero. Passing from a distributional Hessian bound to a statement about every individual geodesic is a recurring need, for example in characterizing lower bounds on sectional curvature synthetically (in the same release the preprint accompanies an OpenAI preprint on Gigli's distributional-curvature characterization of Alexandrov spaces). Earlier results get this passage only under extra regularity.

Timeline

2014 — Savaré's self-improvement of the Bakry–Émery condition gives a measure-valued Bochner calculus on $\mathrm{RCD}(K,\infty)$ spaces (Savaré 2014).
2015 — Ambrosio, Gigli and Savaré identify Bakry–Émery bounds with Riemannian curvature-dimension bounds (Ann. Probab. 2015). Ketterer uses an exponential change of measure under a Hessian assumption with Sobolev regularity (Ketterer 2015, Thm 7.1).
2018 — Gigli's second-order calculus on $\mathrm{RCD}$ spaces: Hessians of test functions and $\nabla_{\nabla g}\nabla g=\nabla(\Gamma(g)/2)$ (Gigli, Mem. AMS 2018). Han passes from infinitesimal to weak convexity by entropy convexity for $e^{-au}m$ , assuming second-order Sobolev regularity (Han 2018); Sturm treats semiconvex functions by vanishing entropy (Sturm 2018).
2020 — Kapovitch and Ketterer derive geodesic convexity from an $L^2$ -Hessian bound for Laplacian-domain functions (J. reine angew. Math. 2020, Thm 4.7).
2021 — Braun, Habermann and Sturm develop variable-curvature equivalences (J. Math. Pures Appl. 2021).
2024–2025 — Brena and Gigli discuss the passage from weak Hessian bounds to geodesic convexity and propose a change-of-measure route, identifying the regularity it needs (Potential Anal. 2025, Remarks 2.3–2.4). Deng proves that finite-dimensional $\mathrm{RCD}(K,N)$ spaces are non-branching (Geom. Topol. 2025, Thm 1.3).
2026 — An OpenAI preprint, Weak Hessian bounds along every geodesic in RCD spaces (OpenAI Math Release, September 24, 2026), claims the passage under only bounded Lipschitz regularity of $F$ and bounded continuous $G$ . It has not been peer reviewed, and the claim has not been formally verified.

Setting

$(M,d,m)$ is a complete separable metric space with a Borel measure $m$ that charges every nonempty open set and is finite on bounded sets. $\mathrm{RCD}(K,N)$ , for $K\in\mathbb R$ and $1<N<\infty$ , means the (unreduced) Lott–Sturm–Villani curvature-dimension condition $\mathrm{CD}(K,N)$ for optimal transport between absolutely continuous probability measures with finite second moment, together with a quadratic Cheeger energy (infinitesimal Hilbertianity).

The minimal weak upper gradient $|\nabla f|$ is defined through test plans (probability measures on absolutely continuous curves with bounded compression and finite kinetic energy). Polarization gives $\Gamma(u,v)=\langle\nabla u,\nabla v\rangle$ , and the Laplacian is the nonpositive generator, $\int\Gamma(u,v)\,dm=-\int(\Delta u)v\,dm$ . The test class consists of bounded, globally Lipschitz $g$ in the domain of $\Delta$ with $\Delta g\in W^{1,2}$ . For such compactly supported $g$ and nonnegative compactly supported Lipschitz $h$ , the weak Hessian evaluation of $F$ is

H_F(\nabla g,\nabla g)(h)= -\int_M\big(\Gamma(h,g)+h\,\Delta g\big)\,\Gamma(F,g)\,dm-\int_M h\,\Gamma\!\big(F,\tfrac12\Gamma(g)\big)\,dm .

A constant-speed minimizing geodesic is a curve $\sigma:[0,1]\to M$ with $d(\sigma_s,\sigma_t)=|s-t|\,\ell$ , where $\ell=d(\sigma_0,\sigma_1)$ . All of these notions are defined from scratch in the Lean development (IsTestPlan, weakGradient, gamma, IsLaplacian, IsTestFunction, weakHessian, CurvatureDimension, RCD).

Formalization targets

Goal: weak Hessian bounds along every geodesic (Theorem 1.1)

Let $(M,d,m)$ be a full-support $\mathrm{RCD}(K,N)$ space with $1<N<\infty$ . Let $F$ be bounded and globally Lipschitz and $G$ bounded and continuous, and assume

H_F(\nabla g,\nabla g)(h)\le\int_M h\,G\,\Gamma(g)\,dm

for all compactly supported test functions $g$ and all nonnegative $h\in\mathrm{Lip}_c(M)$ . Then every constant-speed minimizing geodesic $\sigma$ of length $\ell$ satisfies $(F\circ\sigma)''\le\ell^2\,G\circ\sigma$ in distributions on $(0,1)$ :

\int_0^1F(\sigma_t)\,\varphi''(t)\,dt\le\ell^2\int_0^1G(\sigma_t)\,\varphi(t)\,dt\qquad\text{for all } 0\le\varphi\in C_c^\infty(0,1).

The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. If the source's proof is correct, the theorem makes a measure-theoretic Hessian inequality usable on every prescribed geodesic, including geodesics that are invisible to almost-everywhere statements. For constant $G=c$ it says that $t\mapsto F(\sigma_t)-c\ell^2t^2/2$ is concave on every geodesic. Compared with earlier results, $F$ needs only to be bounded and Lipschitz (no second-order Sobolev or Laplacian-domain regularity), $G$ may vary in space, and $m$ may have infinite total mass. Such geodesic convexity statements feed into synthetic characterizations of sectional-curvature lower bounds and into rigidity arguments on $\mathrm{RCD}$ spaces.

Formalizing it. The statement depends on a large definitional layer: test plans, weak upper gradients, Cheeger energy, the Laplacian, Lott–Sturm–Villani $\mathrm{CD}(K,N)$ and the weak Hessian. None of these is in Mathlib. Formalizing them faithfully is reusable infrastructure for the whole theory of metric measure spaces with Ricci bounds. The proof itself relies on deep inputs (Savaré's self-improvement, the Ambrosio–Gigli–Savaré and Braun–Habermann–Sturm equivalences, Deng's non-branching theorem), so the realistic path is to state those inputs as milestones.

Difficulty

A weak Hessian bound holds only after integration against $m$ . A naive argument would average the bound over a family of geodesics and then localize, but a fixed geodesic can carry zero measure, and almost-everywhere statements about transport geodesics say nothing about it. The natural fix — change the measure to $e^{\lambda F}m$ and use entropy convexity — requires the weighted Bochner inequality on the weighted test class. A Lipschitz weight does not preserve that class: the drift term $\Gamma(V,u)$ need not be Sobolev, as an explicit Euclidean example in the source shows (Remark 4.2). Localizing to one geodesic also needs uniqueness of geodesics between nearby endpoints, which in this generality comes from non-branching of finite-dimensional $\mathrm{RCD}$ spaces.

Formalization scope

$X$ is a MetricSpace with Borel σ-algebra, CompleteSpace and SeparableSpace; $m$ is a Measure X with FullSupport and FiniteOnBoundedSets. RCD m K N is the unreduced CurvatureDimension with the $\tau$ coefficients for all $N'\ge N$ , plus QuadraticCheegerEnergy (the parallelogram law for Cheeger energy).
IsTestFunction requires the function itself (not merely a representative) to be bounded and globally Lipschitz, in the Laplacian domain, with Sobolev Laplacian. WeakHessianUpperBound m F G quantifies over compactly supported test functions $g$ and compactly supported nonnegative Lipschitz $h$ .
Geodesics are continuous maps Set.Icc 0 1 → X with $d(\sigma_s,\sigma_t)=|s-t|\,d(\sigma_0,\sigma_1)$ , so constant curves are included (the conclusion is then trivial). The conclusion CurveSecondDerivativeBound integrates over $[0,1]$ against smooth nonnegative $\varphi$ with tsupport φ ⊆ Ioo 0 1.
Choice-based definitions (weakGradient, laplacian) return $0$ when the object does not exist. The hypotheses on $F$ (bounded Lipschitz) and the test-function requirements ensure that the relevant gradients and Laplacians exist, so the hypothesis is not vacuous.
Contributions welcome: a faithful library of test plans, minimal weak upper gradients and the Laplacian on metric measure spaces; the Lott–Sturm–Villani $\mathrm{CD}(K,N)$ condition; entropy and Wasserstein geodesics.

Selected references

N. Gigli, Nonsmooth differential geometry — an approach tailored for spaces with Ricci curvature bounded from below, Mem. Amer. Math. Soc. 251 (2018). https://doi.org/10.1090/memo/1196
G. Savaré, Self-improvement of the Bakry–Émery condition and Wasserstein contraction of the heat flow in $\mathrm{RCD}(K,\infty)$ metric measure spaces, Discrete Contin. Dyn. Syst. 34 (2014), 1641–1661. https://doi.org/10.3934/dcds.2014.34.1641
L. Ambrosio, N. Gigli and G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43 (2015), 339–404. https://doi.org/10.1214/14-AOP907
M. Braun, K. Habermann and K.-T. Sturm, Optimal transport, gradient estimates, and pathwise Brownian coupling on spaces with variable Ricci bounds, J. Math. Pures Appl. 147 (2021), 60–97. https://doi.org/10.1016/j.matpur.2021.01.002
C. Ketterer, Obata's rigidity theorem for metric measure spaces, Anal. Geom. Metr. Spaces 3 (2015), 278–295. https://doi.org/10.1515/agms-2015-0016
K.-T. Sturm, Gradient flows for semiconvex functions on metric measure spaces — existence, uniqueness and Lipschitz continuity, Proc. Amer. Math. Soc. 146 (2018), 3985–3994. https://doi.org/10.1090/proc/14061
B.-X. Han, Characterizations of monotonicity of vector fields on metric measure spaces, Calc. Var. PDE 57 (2018). https://doi.org/10.1007/s00526-018-1388-9
V. Kapovitch and C. Ketterer, CD meets CAT, J. reine angew. Math. 766 (2020), 1–44. https://arxiv.org/abs/1712.02839
C. Brena and N. Gigli, Fine representation of Hessian of convex functions and Ricci tensor on RCD spaces, Potential Anal. 62 (2025), 703–737. https://doi.org/10.1007/s11118-024-10153-5
Q. Deng, Hölder continuity of tangent cones in $\mathrm{RCD}(K,N)$ spaces and applications to non-branching, Geom. Topol. 29 (2025), 1037–1114. https://doi.org/10.2140/gt.2025.29.1037
OpenAI, Weak Hessian bounds along every geodesic in RCD spaces, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-Hessian-bounds-along-every-geodesic-in-RCD-spaces-September-24-2026/weak-hessian-geodesics.pdf

14 thms2 active usersReviewed

Completed

Calculus of Variations Differential Geometry·Captain: wurtle

The Isoperimetric Conjecture for the Cubic Flat Three-TorusResearch Paper

Motivation

The isoperimetric problem asks, for each prescribed volume, for the regions of least boundary area. In Euclidean space the answer is the round ball. In a compact space with topology the answer changes with the volume: small regions still look like balls, but larger regions can save area by wrapping around the space. The unit cubic flat three-torus $\mathbb R^3/\mathbb Z^3$ is the simplest compact example in three dimensions, and the periodic isoperimetric problem on it is equivalent, by reflection, to the relative isoperimetric problem in a cube. It is a standard test case for how local Euclidean geometry interacts with global topology, and it has been studied in connection with periodic minimal and constant-mean-curvature surfaces (Hauswirth–Pérez–Romon–Ros 2004; Ros 2005).

The conjectured answer is a sequence of three phases: balls, solid circular tubes around shortest closed geodesics, and slabs between parallel coordinate tori, followed by their complements. This mission asks for a machine-checked proof of that conjecture, including the classification of every minimizer, as claimed in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

1972 — Hadwiger proves that a coordinate cut minimizes at half volume for the cube (Monatsh. Math. 1972).
1992–1996 — Ritoré and Ros develop stability and structure results for constant-mean-curvature surfaces in flat three-manifolds (Comment. Math. Helv. 1992; Trans. AMS 1996); Ritoré's thesis records Hsiang's coordinate reflection symmetry (1994).
2000 — Barthe and Maurey recover Hadwiger's half-volume result by Gaussian comparison (Ann. IHP 2000). Morgan and Johnson's small-volume comparison implies that balls minimize for sufficiently small volume on compact flat manifolds (Indiana Univ. Math. J. 2000, Theorem 4.4).
2004 — Hauswirth, Pérez, Romon and Ros state the ball–tube–slab prediction and prove that a nonstandard minimizing boundary is connected of genus $2$ , $3$ or $4$ , with curvature–area bounds (Trans. AMS 2004).
2005 — Ros's survey records the conjecture for the cubic torus and cube (Clay Math. Proc. 2, 2005, Section 1.6).
2013 — Acerbi, Fusco and Morini prove that slabs are the only minimizers near half volume (Comm. Math. Phys. 2013, Theorem 5.3), without effective ranges.
2026 — Milman obtains effective ranges for the phases, including the ball phase up to volume fraction $0.120582\ldots$ , and reduces the profile conjecture to the two transition volumes $4\pi/81$ and $1/\pi$ (Comm. Pure Appl. Math. 2026, Theorems 1.2–1.3).
September 2026 — The OpenAI preprint claims the full conjecture with all equality cases (Theorem 1.1, p. 1).

Setting

Let $\mathbb T=\mathbb R^3/\mathbb Z^3$ with its flat metric and volume measure $|\cdot|$ (total volume $1$ ). For a measurable $E\subseteq\mathbb T$ , its perimeter is the De Giorgi perimeter

P(E)=\sup\Bigl\{\int_E \operatorname{div}F : F \text{ a smooth vector field on }\mathbb T,\ |F|\le1\Bigr\}\in[0,\infty],

which equals the boundary area when $\partial E$ is smooth, and is insensitive to null-set changes. $E$ has finite perimeter if $P(E)<\infty$ . A minimizer at volume $V$ is a finite-perimeter $E$ with $|E|=V$ and $P(E)\le P(F)$ for all finite-perimeter $F$ with $|F|=V$ .

For $0<V<1$ put $v=\min(V,1-V)$ and

I(V)=\min\Bigl\{(36\pi)^{1/3}v^{2/3},\;2\sqrt{\pi v},\;2\Bigr\}.

The three expressions are the perimeters of a ball of volume $v$ , a solid circular tube of volume $v$ around a shortest closed geodesic (a coordinate circle of length $1$ ), and a slab of width $v$ between two coordinate tori. The branches cross at $V_1=4\pi/81$ and $V_2=1/\pi$ .

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every $V\in(0,1)$ :

a minimizer at volume $V$ exists;
every minimizer has perimeter exactly $I(V)$ ;
a set $E$ is a minimizer at volume $V\le 1/2$ if and only if, up to an isometry of $\mathbb T$ and a null set, it is a ball of radius $(3V/(4\pi))^{1/3}$ when $V\le 4\pi/81$ , a solid tube of radius $\sqrt{V/\pi}$ about a shortest closed geodesic when $4\pi/81\le V\le1/\pi$ , or a slab of width $V$ between coordinate tori when $1/\pi\le V$ ; for $V>1/2$ the minimizers are exactly the complements of those at volume $1-V$ .

The ranges are closed, so at each transition volume both adjacent types are minimizers and there are no others. This is OAI.CubicTorus.unit_cubic_isoperimetric.

Significance

The result itself. It determines the isoperimetric profile of the cubic three-torus and the reflected relative profile of the unit cube at every volume, settling a conjecture explicitly posed by Hauswirth–Pérez–Romon–Ros and Ros. The equality classification at the transitions is new even granting Milman's reduction, which classifies minimizers on the open branches once the endpoint values are known but leaves extra co-minimizers at $4\pi/81$ and $1/\pi$ to be excluded.

Formalizing it. The proof combines geometric measure theory (existence and regularity of minimizers), structure theorems for stable CMC surfaces, a differential inequality for the profile, and certified one-variable numerics. A formal proof would certify the whole chain; existence and regularity of isoperimetric regions in a flat torus are themselves substantial missing library pieces. No machine-checked version of the result, or of the Euclidean isoperimetric inequality for finite-perimeter sets in this generality, is known to exist.

Difficulty

The main obstruction is to rule out minimizers whose boundary is a connected surface of genus $2$ , $3$ or $4$ (Theorem 2.1, p. 3, quoting Hauswirth–Pérez–Romon–Ros). The general curvature–area bound and the profile differential inequality (Lemma 2.3, p. 4) exclude such surfaces away from the transitions but not at $V_1,V_2$ themselves. At the cylinder–slab transition $V_2=1/\pi$ , the planar isoperimetric inequality applied to horizontal sections leaves a deficit in a central curvature range; the preprint closes it with a calibration of a corner section, a nesting argument for planar sections, and a Jensen estimate (Section 6, Proposition 6.7, p. 19), supplemented by certified numerical bounds (Appendix B).

Formalization scope

The torus is PiLp 2 (fun _ : Fin 3 => AddCircle 1), whose metric is the flat torus metric; volume is the pushforward of Lebesgue measure on the half-open unit cube.
Perimeter is the De Giorgi supremum over $C^\infty$ $\mathbb Z^3$ -periodic vector fields on $\mathbb R^3$ with $|F|\le1$ , valued in ℝ≥0∞; no regularity of $E$ is assumed. Finite perimeter also requires null-measurability.
Minimizers are global: the comparison ranges over all finite-perimeter sets of the same volume.
The canonical ball is the metric ball about $0$ ; the tube is $\{x:\|x_1\|^2+\|x_2\|^2<V/\pi\}$ around the $x_0$ -direction geodesic; the slab is $\{x:\|x_0\|<V/2\}$ . CongruentAE allows any isometry of $\mathbb T$ followed by a null-set change.
The phase ranges are closed, so both types are included at ties, matching the source. The statement is not vacuous: existence is part of the conclusion, and the profile value is a concrete real number.

Useful reusable infrastructure: sets of finite perimeter on flat tori, compactness and lower semicontinuity of perimeter, and the Euclidean isoperimetric inequality.

Selected references

OpenAI, The Isoperimetric Conjecture for the Cubic Flat Three-Torus, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026/article.pdf
L. Hauswirth, J. Pérez, P. Romon, A. Ros, The periodic isoperimetric problem, Trans. Amer. Math. Soc. 356 (2004), 2025–2047. https://doi.org/10.1090/S0002-9947-03-03362-2
A. Ros, The isoperimetric problem, in Global Theory of Minimal Surfaces, Clay Math. Proc. 2 (2005), 175–209. https://www.claymath.org/wp-content/uploads/2022/03/cmip02.pdf
E. Milman, Isoperimetric inequalities on slabs with applications to cubes and Gaussian slabs, Comm. Pure Appl. Math. 79 (2026), 1012–1072. https://doi.org/10.1002/cpa.70020
E. Acerbi, N. Fusco, M. Morini, Minimality via second variation for a nonlocal isoperimetric problem, Comm. Math. Phys. 322 (2013), 515–557. https://doi.org/10.1007/s00220-013-1733-y
H. Hadwiger, Gitterperiodische Punktmengen und Isoperimetrie, Monatsh. Math. 76 (1972), 410–418. https://doi.org/10.1007/BF01297304
F. Morgan, D. L. Johnson, Some sharp isoperimetric theorems for Riemannian manifolds, Indiana Univ. Math. J. 49 (2000), 1017–1041. https://www.lehigh.edu/~dlj0/papers/morgan-johnson.pdf
M. Ritoré, A. Ros, Stable constant mean curvature tori and the isoperimetric problem in three space forms, Comment. Math. Helv. 67 (1992), 293–305. https://doi.org/10.1007/BF02566501

12 thms2 active usersReviewed

Completed

Analysis Differential Geometry Partial Differential Equations·Captain: wurtle

Smooth counterexamples to Yau's nodal upper bound in dimensions three and fourResearch Paper

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. In 1982 Yau asked whether, on a fixed smooth closed Riemannian manifold of dimension $d$ , the $(d-1)$ -dimensional measure of the nodal set of every eigenfunction with eigenvalue $\lambda$ is comparable to $\sqrt\lambda$ from above and below (Yau, Problem section, Annals of Math. Studies 102, 1982). The conjectured two-sided bound

c_g\sqrt\lambda\le\mathcal H^{d-1}_g(Z_u)\le C_g\sqrt\lambda,

with constants depending only on the metric, has organized several decades of work on unique continuation and quantitative zero sets of elliptic equations. The lower and upper inequalities are logically separate, and a fixed metric must be distinguished from a metric chosen anew for each eigenvalue.

Timeline

1978. Brüning proves the sharp lower bound on smooth surfaces (doi:10.1007/BF01214561).
1982. Yau states the conjecture.
1988. Donnelly and Fefferman prove both bounds for real-analytic metrics (doi:10.1007/BF01393691).
1989. Hardt and Simon give a general non-polynomial upper estimate for smooth metrics (doi:10.4310/jdg/1214443599).
1990. Donnelly and Fefferman prove the surface upper bound $C\lambda^{3/4}$ (doi:10.1090/S0894-0347-1990-1035413-2).
2015–2017. Enciso and Peralta-Salas, then with Steinerberger, prescribe the nodal set of a first eigenfunction by choosing the metric (doi:10.4310/jdg/1442364650, doi:10.1093/imrn/rnw126).
2018. Logunov proves a polynomial upper estimate in dimension $\ge3$ (doi:10.4007/annals.2018.187.1.4) and the sharp lower estimate in every dimension (doi:10.4007/annals.2018.187.1.5); Logunov and Malinnikova improve the surface exponent to $3/4-\beta$ (doi:10.1007/978-3-319-59078-3_17).
2023. Hezari proves upper bounds for Gevrey and certain quasianalytic metrics (doi:10.1007/s00220-023-04853-z).

After Logunov, the smooth upper bound was known to be polynomial in $\lambda$ but not of order $\sqrt\lambda$ . The source of this mission, an OpenAI preprint dated September 23, 2026, claims that the upper bound fails for fixed smooth metrics in dimensions three and four.

Setting

Let $(M,g)$ be a closed connected smooth Riemannian manifold of dimension $d$ . In local coordinates, with $|g|=\det(g_{ij})$ and $(g^{ij})$ the inverse matrix, the Laplace–Beltrami operator is $\Delta_g u=|g|^{-1/2}\partial_i(|g|^{1/2}g^{ij}\partial_j u)$ . An eigenfunction with eigenvalue $\lambda>0$ is a nonzero real $u$ with $-\Delta_g u=\lambda u$ ; its nodal set is $Z_u=\{u=0\}$ , measured by $\mathcal H^{d-1}_g$ , Hausdorff measure for the Riemannian distance of $g$ .

The round metric $g_*$ on $S^3\subset\mathbb R^4$ is the pullback of the Euclidean inner product. A $C^\infty$ neighborhood of $g_*$ is any set of metrics containing all $g$ whose coefficient functions, in finitely many charts and on compact subsets, have derivatives up to some order within $\varepsilon$ of those of $g_*$ .

Formalization targets

Goal: Theorem 1.1 (three-sphere)

For every $C^\infty$ neighborhood $\mathcal N$ of $g_*$ there are $g_\infty\in\mathcal N$ , nonzero smooth $u_j$ and $\lambda_j>0$ with

-\Delta_{g_\infty}u_j=\lambda_ju_j,\qquad \lambda_j\to\infty,\qquad \frac{\mathcal H^2_{g_\infty}(Z_{u_j})}{\sqrt{\lambda_j}}\to\infty.

Lean: OAI.YauCounterexamples.sphere_three, open on the platform.

Milestone: Theorem 1.2 (four-manifold)

There are a smooth metric $g_\infty$ on $S^2\times\mathbb T^2$ , nonzero smooth $u_j$ and $\lambda_j\to\infty$ with $-\Delta_{g_\infty}u_j=\lambda_ju_j$ and $\mathcal H^3_{g_\infty}(Z_{u_j})/\sqrt{\lambda_j}\to\infty$ .

Significance

Theorem 1.1 disproves the upper-bound half of Yau's conjecture for smooth metrics already in dimension three, with metrics arbitrarily close to the round sphere, where the bound does hold. Neither theorem asserts a power-law excess, and neither contradicts the lower bound. Together with the companion preprints of this family (a sharp $\sqrt\lambda$ upper bound on smooth surfaces, and power-law violations in dimension at least five) it would locate the boundary of validity of the upper bound by dimension. The result is claimed in an OpenAI preprint that has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Approximate eigenfunctions (quasimodes) with large nodal sets are comparatively easy to build locally. The obstacle is to replace each quasimode by an exact eigenfunction of an ordinary Laplace–Beltrami operator of one fixed metric, while keeping every sign change that witnesses nodal measure, and to do this for infinitely many eigenvalues at once with corrections that converge in $C^\infty$ . A scalar potential or conductivity correction would be easy, but the operator must be a genuine metric Laplacian, which imposes a determinant identity between conductivity and density; the paper uses different, dimension-specific repairs in dimensions three and four. Also, the nodal set is not assumed regular, so its measure must be bounded below by a stable, lower semicontinuous count of sign changes.

Formalization scope

SmoothMetric E M is Mathlib's ContMDiffRiemannianMetric on the tangent bundle. Sphere 3 is the unit sphere of EuclideanSpace ℝ (Fin 4) with its standard charts; the four-manifold is Sphere 2 × (Circle × Circle).
laplaceBeltrami g u x is the coordinate formula above, in the chart at x with coordinates from Module.finBasis; only values in the open chart target are used.
IsSmoothNeighborhood g₀ N: some finite list of compact-chart derivative tests and one $\varepsilon>0$ such that every metric passing them lies in N. Quantifying over all such N is the $C^\infty$ topology.
nodalMeasure g d u is Measure.hausdorffMeasure d of $\{u=0\}$ for the path distance of g itself (EMetricSpace.ofRiemannianMetric), not the distance inherited from $\mathbb R^4$ .
HasUnboundedNodalRatio g d asks for smooth nonzero eigenfunctions with positive eigenvalues tending to $\infty$ , finite nodal measures, and ratio $\mathcal H^{d-1}/\sqrt\lambda\to\infty$ . Finiteness rules out the degenerate reading where an infinite measure would become $0$ under toReal; it holds for every eigenfunction of a smooth metric on a compact manifold (Hardt–Simon).

A complete development needs elliptic regularity and perturbation theory for simple eigenvalues of metric Laplacians, WKB-type quasimode constructions, and Hausdorff-measure lower bounds from sign changes along segments. Contributions formalizing the named propositions (Proposition 2.6 spherical profiles, Proposition 3.6 simultaneous wave realization, Proposition 4.4 exactification, Proposition 6.2 one construction step) are welcome.

Selected references

OpenAI, Smooth counterexamples to Yau's nodal upper bound in dimensions three and four, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-counterexamples-to-Yaus-nodal-upper-bound-in-dimensions-three-and-four-September-23-2026/paper.pdf
S.-T. Yau, Problem section, Seminar on Differential Geometry, Annals of Mathematics Studies 102, 1982.
H. Donnelly, C. Fefferman, Nodal sets of eigenfunctions on Riemannian manifolds, Invent. Math., 1988. https://doi.org/10.1007/BF01393691
R. Hardt, L. Simon, Nodal sets for solutions of elliptic equations, J. Differential Geom., 1989. https://doi.org/10.4310/jdg/1214443599
A. Logunov, Nodal sets of Laplace eigenfunctions: polynomial upper estimates of the Hausdorff measure, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.4
A. Logunov, Nodal sets of Laplace eigenfunctions: proof of Nadirashvili's conjecture and of the lower bound in Yau's conjecture, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.5
A. Logunov, E. Malinnikova, Nodal sets of Laplace eigenfunctions: estimates of the Hausdorff measure in dimensions two and three, 2018. https://doi.org/10.1007/978-3-319-59078-3_17
H. Hezari, Upper bounds on the size of nodal sets for Gevrey and quasianalytic Riemannian manifolds, Commun. Math. Phys., 2023. https://doi.org/10.1007/s00220-023-04853-z
A. Enciso, D. Peralta-Salas, Eigenfunctions with prescribed nodal sets, J. Differential Geom., 2015. https://doi.org/10.4310/jdg/1442364650

20 thms2 active usersReviewed

Completed

Analysis Differential Geometry Partial Differential Equations·Captain: wurtle

Sharp nodal length on smooth surfacesResearch Paper

Motivation

The nodal set of a Laplace eigenfunction is the set where it vanishes. On a vibrating membrane these are the curves that stay at rest (Chladni patterns), and in quantum mechanics they are the points where a stationary wave function has zero amplitude. A basic question is how large the nodal set is as the frequency grows. Yau conjectured in 1982 that on a smooth closed $n$ -dimensional Riemannian manifold the $(n-1)$ -dimensional measure of the nodal set of an eigenfunction with eigenvalue $\lambda$ is comparable to $\sqrt\lambda$ , from above and below, with constants depending only on the manifold (Yau, Problem section, Annals of Math. Studies 102, 1982). The question is a test case for unique continuation and quantitative control of the zeros of solutions to elliptic equations.

Timeline

1978. Brüning proves the lower bound $\mathcal H^1(Z_u)\ge c\sqrt\lambda$ on smooth surfaces (doi:10.1007/BF01214561).
1982. Yau states the conjecture (upper and lower bounds of order $\sqrt\lambda$ in every dimension).
1988. Donnelly and Fefferman prove both bounds for real-analytic manifolds and metrics (doi:10.1007/BF01393691).
1990. Donnelly and Fefferman prove the upper bound $C\lambda^{3/4}$ for smooth surfaces (doi:10.1090/S0894-0347-1990-1035413-2); Dong gives a different proof of the same order in 1992 (doi:10.4310/JDG/1214448750).
2005. Nazarov, Polterovich and Sodin propose a statistical approach to local doubling and relate it to nodal length (doi:10.1353/ajm.2005.0030).
2015. Roy-Fortin establishes comparisons between local growth exponents and nodal length on surfaces (doi:10.2140/apde.2015.8.223, arXiv:1510.02376).
2018. Logunov proves the lower bound in every dimension (doi:10.4007/annals.2018.187.1.5); Logunov and Malinnikova improve the surface upper bound to $C\lambda^{3/4-\beta}$ for a universal $\beta\in(0,1/4)$ (doi:10.1007/978-3-319-59078-3_17).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the sharp upper bound $C\sqrt\lambda$ on every smooth closed surface, which together with Brüning's lower bound would settle Yau's conjecture in dimension two.

Setting

Let $(M,g)$ be a closed (compact, without boundary) connected smooth Riemannian surface. In local coordinates write $g=(g_{ij})$ , $|g|=\det(g_{ij})$ and $(g^{ij})$ for the inverse matrix. The Laplace–Beltrami operator is

\Delta_g u=|g|^{-1/2}\sum_{i,j}\partial_i\bigl(|g|^{1/2}g^{ij}\partial_j u\bigr).

A Laplace eigenfunction with eigenvalue $\lambda>0$ is a nonzero real function $u$ with $-\Delta_g u=\lambda u$ . Its nodal set is $Z_u=\{x\in M: u(x)=0\}$ , and its nodal length is $\mathcal H^1_g(Z_u)$ , the one-dimensional Hausdorff measure for the Riemannian distance $d_g$ .

Formalization targets

Goal: Theorem 1.1

\exists\,C=C(M,g)<\infty\ \ \forall\lambda>0\ \ \forall u\not\equiv0:\quad -\Delta_g u=\lambda u\ \Longrightarrow\ \mathcal H^1_g(Z_u)\le C\sqrt\lambda.

The constant depends only on the surface and its metric and is the same for every eigenfunction in every positive eigenspace. The Lean statement OAI.SharpNodal.Main asserts MainStatement M; it is open on the platform.

Significance

The order $\sqrt\lambda$ is optimal: Brüning's lower bound shows it cannot be improved, and on the round sphere spherical harmonics attain it. Before this work the best smooth-surface upper bound was $C\lambda^{3/4-\beta}$ . A sharp upper bound on every smooth surface, combined with the known lower bounds, would resolve Yau's conjecture for smooth closed surfaces; in dimensions three and higher the smooth upper bound remains a separate question (the companion missions in this family address it).

The theorem is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists. A formal proof would certify a long chain of quantitative estimates (Carleman inequalities, multiscale subdivision, packing), each of which is a natural target for reuse in other unique-continuation problems.

Difficulty

For a real-analytic metric, an eigenfunction extends holomorphically and its zeros can be counted by complex-analytic methods; this is how Donnelly and Fefferman obtain $\sqrt\lambda$ . For a merely smooth metric no such extension exists. The standard route bounds nodal length on each wavelength-sized square by the local doubling exponent (growth of the $L^2$ norm from a disk to a larger disk). The known bounds on individual doubling exponents are too weak: a square can have growth much larger than average, and summing worst-case local bounds loses a power of $\lambda$ . What is needed is control of the average growth over all wavelength-scale squares, while allowing large values on individual squares.

Formalization scope

The surface is a type M with [MetricSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] [IsManifold 𝓘(ℝ, Plane) ∞ M], a smooth RiemannianBundle on the tangent bundle, and [IsRiemannianManifold 𝓘(ℝ,Plane) M], so the metric-space distance is the Riemannian distance. CompactSpace and ConnectedSpace encode closed and connected; the model space has no boundary.
laplaceBeltrami is the coordinate formula above, computed through chartAt with the metric matrix obtained from mfderiv of the inverse chart. No orientability is assumed.
Eigenfunctions are assumed ContMDiff … ∞ and nonzero, with $-\Delta_g u=\lambda u$ at every point; smoothness is automatic by elliptic regularity, so this does not weaken the statement.
nodalLength u is Measure.hausdorffMeasure 1 of $\{u=0\}$ for the Borel structure of the metric, valued in ℝ≥0∞; the bound is ≤ ENNReal.ofReal (C * Real.sqrt lam) with $C\ge0$ fixed before $\lambda$ and $u$ .

A complete development needs local isothermal coordinates or a coordinate-free substitute, Carleman estimates, $L^2$ growth bounds, and a planar comparison between growth and nodal length (Roy-Fortin's theorem). Much of this, especially Hausdorff-measure estimates for zero sets of solutions of planar elliptic equations, is reusable. Contributions formalizing the paper's intermediate results (Theorem 2.2, Proposition 3.4, Theorem 5.5, Lemma 6.2) or Roy-Fortin's planar theorem are welcome.

Selected references

OpenAI, Sharp nodal length on smooth surfaces, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-nodal-length-on-smooth-surfaces-September-23-2026/paper.pdf
S.-T. Yau, Problem section, in Seminar on Differential Geometry, Annals of Mathematics Studies 102, Princeton University Press, 1982.
J. Brüning, Über Knoten von Eigenfunktionen des Laplace–Beltrami-Operators, Math. Z., 1978. https://doi.org/10.1007/BF01214561
H. Donnelly, C. Fefferman, Nodal sets of eigenfunctions on Riemannian manifolds, Invent. Math., 1988. https://doi.org/10.1007/BF01393691
H. Donnelly, C. Fefferman, Nodal sets for eigenfunctions of the Laplacian on surfaces, J. Amer. Math. Soc., 1990. https://doi.org/10.1090/S0894-0347-1990-1035413-2
R.-T. Dong, Nodal sets of eigenfunctions on Riemann surfaces, J. Differential Geom., 1992. https://doi.org/10.4310/JDG/1214448750
F. Nazarov, L. Polterovich, M. Sodin, Sign and area in nodal geometry of Laplace eigenfunctions, Amer. J. Math., 2005. https://doi.org/10.1353/ajm.2005.0030
G. Roy-Fortin, Nodal sets and growth exponents of Laplace eigenfunctions on surfaces, Anal. PDE, 2015. https://doi.org/10.2140/apde.2015.8.223
A. Logunov, Nodal sets of Laplace eigenfunctions: proof of Nadirashvili's conjecture and of the lower bound in Yau's conjecture, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.187.1.5
A. Logunov, E. Malinnikova, Nodal sets of Laplace eigenfunctions: estimates of the Hausdorff measure in dimensions two and three, Oper. Theory Adv. Appl. 261, 2018. https://doi.org/10.1007/978-3-319-59078-3_17

10 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: wurtle

Exact asymptotic moduli in a Daugavet subspace of L1Research Paper

Motivation

A norm is uniformly convex when midpoints of far-apart unit vectors are pushed strictly inside the unit ball. In infinite-dimensional Banach spaces the useful notions are asymptotic: one asks for a gain only in directions taken from a subspace of finite codimension, chosen after the center is fixed. Two such notions are compared here. Asymptotic uniform convexity (AUC) asks for growth of $\|x+ty\|$ in every far-out unit direction $y$ ; asymptotic midpoint uniform convexity (AMUC) asks only that the average of $\|x+ty\|$ and $\|x-ty\|$ grows. These properties control nonlinear embeddings (for instance of countably branching diamond graphs) and are standard tools in the asymptotic geometry of Banach spaces.

Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) asked whether AMUC and AUC are equivalent up to renorming. Baudier (2026) answered no, using subspaces of $L^1$ whose unit ball is compact in measure and the Daugavet-property example of Kadets and Werner. This mission asks for the exact values of both moduli in that setting.

Timeline

1980. Bourgain and Rosenthal construct a subspace of $L^1$ whose unit ball is relatively compact in measure but which fails the Radon–Nikodym property (doi:10.1007/BF02762868).
1983. Brézis and Lieb prove their splitting identity for pointwise convergent sequences in $L^p$ (doi:10.1090/S0002-9939-1983-0699419-3).
2000. Kadets, Shvidkoy, Sirotkin and Werner give the slice characterization of the Daugavet property (arXiv:math/9709216); Shvydkoy gives its weak-open form (doi:10.1006/jfan.2000.3626).
2004. Kadets and Werner refine the Bourgain–Rosenthal construction to obtain a space with the Schur and Daugavet properties (doi:10.1090/S0002-9939-03-07278-2).
2016. Dilworth et al. introduce AMUC and ask whether it is equivalent to AUC up to renorming (doi:10.1016/j.jmaa.2015.11.061).
2026. Baudier proves AMUC for measure-compact subspaces of $L^1$ and deduces a negative answer via the Kadets–Werner space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026, which computes both moduli exactly.

Setting

All spaces are real. For a Banach space $X$ with norm $N$ , let $\operatorname{cof}(X)$ be its closed linear subspaces of finite codimension. For $N(x)=1$ and $t>0$ ,

H_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)\ge1}}\Bigl(\frac{N(x+ty)+N(x-ty)}2-1\Bigr),\qquad D_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)=1}}\bigl(N(x+ty)-1\bigr).

The averaged midpoint modulus $\widehat\delta_N(t)$ and the one-sided modulus $\overline\delta_N(t)$ are the infima of $H_N(x,t)$ and $D_N(x,t)$ over unit $x$ . $N$ is AUC if $\overline\delta_N(t)>0$ for all $t>0$ . A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ with $a,b>0$ .

A space has the Daugavet property if $\|I+T\|=1+\|T\|$ for every rank-one bounded operator $T$ . On a probability space $(\Omega,\mathbb P)$ , convergence in measure is given by the metric

d(f,g)=\inf\{a>0:\ \mathbb P(|f-g|>a)<a\}.

A set is totally bounded in measure if for each $\varepsilon>0$ it is covered by finitely many $d$ -balls of radius $\varepsilon$ .

Formalization targets

Goal: Theorem 1.1

Let $E$ be an infinite-dimensional closed subspace of $L^1(\Omega,\mathbb P)$ , $\mathbb P$ a probability measure, whose unit ball is totally bounded in measure and whose norm has the Daugavet property. Then for every unit $x\in E$ and $t>0$

H_E(x,t)=\max\{t/2,\ t-1\},\qquad D_E(x,t)=\max\{0,\ t-2\},

so $\widehat\delta_E(t)=\max\{t/2,t-1\}$ and $\overline\delta_E(t)=\max\{0,t-2\}$ , and $E$ admits no equivalent AUC norm. Lean: OAI.ExactModuli.exact_main (open on the platform).

Milestone: Theorem 6.1 (Kadets–Werner construction)

On $([0,1]^{\mathbb N},\lambda^{\mathbb N})$ there is an infinite-dimensional closed subspace $E\subseteq L^1$ whose unit ball is totally bounded in measure and which has the Daugavet slice property. Lean: OAI.ExactModuli.kadets_werner_existence. The proposal also carries OAI.ExactModuli.exact_example, the combination of the two theorems for this space.

Significance

The formulas show how far apart the two moduli can be: the averaged modulus grows linearly from $0$ , while the one-sided modulus vanishes on the whole interval $(0,2]$ . They refine Baudier's qualitative AMUC statement and linear lower bound into exact curves at every unit center, and the renorming clause shows that no equivalent norm can repair the one-sided modulus. Together with Theorem 6.1, they give a concrete space realizing the separation.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists. The Daugavet slice characterization, Bourgain's lemma on slices and weak neighborhoods (Lemma 3.2), and the construction itself are reusable pieces of Banach space theory that a formalization would supply.

Difficulty

The lower bound for $H_E$ must hold uniformly over all directions in some finite-codimensional subspace, while the hypothesis only says that the unit ball is compact in a weak metric. A compactness argument along subsequences (Baudier's route via Brézis–Lieb) gives positivity but not the exact constant. The upper bounds need directions in a prescribed finite-codimensional subspace that are almost at distance $2$ from $x$ ; the Daugavet property supplies such vectors only in weak neighborhoods, and they must then be corrected into the subspace. The renorming clause must handle an arbitrary equivalent norm, for which neither formula is available.

Formalization scope

Cofinite F is a closed submodule with finite-dimensional quotient. H, D, averagedModulus, oneSidedModulus follow the displayed sup/inf order; H ranges over $N(y)\ge1$ , D over $N(y)=1$ .
EquivalentNorm N is a Seminorm with two-sided comparison constants $a,b>0$ ; AUC N is positivity of oneSidedModulus N t for every $t>0$ .
Daugavet X quantifies over rank-one operators written as ell.smulRight v.
measureDistance is the metric $d$ on Lp ℝ 1 μ; MeasurePrecompactBall μ E requires finite $\varepsilon$ -nets (centers in $L^1$ ) of the unit ball of $E$ ; μ is a probability measure.
kwMeasure is the product of Lebesgue measures on $\mathbb N\to[0,1]$ .
The moduli are real-valued sSup/sInf; for infinite-dimensional $E$ the relevant sets are nonempty and bounded, so the junk values are not used.

A full development needs the Daugavet slice characterization (Lemma 3.1), Bourgain's lemma (Lemma 3.2), the weak-neighborhood diameter-two property (Lemma 3.3), $L^1$ truncation estimates, and the Kadets–Werner iteration (Lemmas 6.2–6.3). Formalizations of these lemmas are welcome.

Selected references

OpenAI, Exact asymptotic moduli in a Daugavet subspace of $L^1$ , preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026/manuscript.pdf
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
V. Kadets, D. Werner, A Banach space with the Schur and the Daugavet property, Proc. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0002-9939-03-07278-2
J. Bourgain, H. P. Rosenthal, Martingales valued in certain subspaces of $L^1$ , Israel J. Math., 1980. https://doi.org/10.1007/BF02762868
V. M. Kadets, R. V. Shvidkoy, G. G. Sirotkin, D. Werner, Banach spaces with the Daugavet property, Trans. Amer. Math. Soc., 2000. https://arxiv.org/abs/math/9709216
R. V. Shvydkoy, Geometric aspects of the Daugavet property, J. Funct. Anal., 2000. https://doi.org/10.1006/jfan.2000.3626
H. Brézis, E. Lieb, A relation between pointwise convergence of functions and convergence of functionals, Proc. Amer. Math. Soc., 1983. https://doi.org/10.1090/S0002-9939-1983-0699419-3

4 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: wurtle

Midpoint lenses in segment spacesResearch Paper

Motivation

In a uniformly convex space, if $x$ is nearly as long as $R$ and both $x+y$ and $x-y$ have length at most $R$ , then the displacement $y$ must be short. The set of such displacements,

\mathcal L(x,R)=\{y:\ \|x+y\|\le R,\ \|x-y\|\le R\},

is a symmetric lens. In infinite dimensions the right question is asymptotic: is $y$ short after discarding finitely many directions? Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) characterized asymptotic midpoint uniform convexity (AMUC) through the measure of noncompactness of such lenses. AMUC is the property that, together with asymptotic uniform convexity (AUC), governs which countably branching graphs embed into a Banach space with bounded distortion.

This mission asks for an explicit lens estimate in two James-type tree spaces, with a bound depending only on the squared-radius deficit $R^2-\|x\|^2$ of the center and holding for every displacement simultaneously after one finite set of coordinates is removed.

Timeline

1974. James introduces the square-sum norm over disjoint segments of a tree (doi:10.1090/S0002-9904-1974-13580-9).
1985. Ghoussoub and Maurey study $G_\delta$ -embeddings in Hilbert space (doi:10.1016/0022-1236(85)90039-4); the coordinate predual $B_\infty$ used here is the Ghoussoub–Maurey–Schachermayer construction as presented by Banakh (2000).
2001. Girardi proves AUC of the canonical predual and of the full dual of the binary James tree space (doi:10.4064/sm147-2-2).
2016. Dilworth et al. introduce AMUC and characterize it by lenses (doi:10.1016/j.jmaa.2015.11.061).
2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of countably branching diamonds (arXiv:1612.01984).
2021. Perreau asks whether the canonical predual of the countably branching James tree space is AMUC (Question 6 of arXiv:2104.10494).
2026. Baudier shows that AMUC does not imply AUC renormability, via the Kadets–Werner modification of the Bourgain–Rosenthal space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

All scalars are real.

Finite-height forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the tree of words of length at most $h$ , ordered by extension (the root is the empty word). The forest $\mathcal F$ is the disjoint union of one copy $\{h\}\times T_h$ for each $h\ge1$ . Write $a\preceq b$ if $a$ is an ancestor of $b$ in the same component. A segment is a nonempty interval $[a,b]=\{v: a\preceq v\preceq b\}$ . For finitely supported $u$ put $u(S)=\sum_{v\in S}u(v)$ and

\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.

Let $J$ be the completion of $(c_{00}(\mathcal F),\rho)$ and $X=J^*$ with the dual norm. Coordinate evaluation gives functionals $e_v^*\in X$ .

Infinite tree. Let $T_\infty=\mathbb N^{<\omega}$ (all finite words, root included), $J_\infty$ the completion for the same norm, and $B_\infty=\overline{\operatorname{span}}\{e_v^*\}\subset J_\infty^*$ , closed in the dual norm.

A finite set $H$ of vertices is ancestral if it contains all ancestors of its elements. On either space,

P_Hx=\sum_{v\in H}x(e_v)\,e_v^*,\qquad Q_Hx=x-P_Hx.

Formalization targets

Goal: Theorem 1.1

For $Y\in\{X,\ B_\infty\}$ , every finite ancestral $H$ , every $x,y\in Y$ with $x=P_Hx$ , and every $R\ge0$ with $\|x+y\|\le R$ and $\|x-y\|\le R$ ,

\|Q_Hy\|\ \le\ 2\sqrt{R^2-\|x\|^2}.

The Lean statement OAI.SegmentLenses.midpoint_lens_main is the conjunction of the two cases. It is open on the platform. The displacement $y$ may have a nonzero head $P_Hy$ ; only its tail is controlled.

Significance

The estimate is uniform over the lens: one finite head $H$ controls every admissible displacement, which is exactly what is needed when a single center has infinitely many approximate midpoints. As a consequence (Corollary 7.1 of the source) both given norms are AMUC with $\widehat\delta(t)\ge(\sqrt{1+t^2/4}-1)/2$ , while Proposition 9.1 shows that neither space admits an equivalent AUC norm. In particular the infinite-height case answers Perreau's question for the specified real norm on $B_\infty$ , and the finite-height forest gives a reflexive space separating AMUC from AUC renormability. A companion preprint uses this theorem to force distortion $D^2\ge1+k/4$ for depth- $k$ countably branching diamonds.

The result is proved only in the OpenAI preprint; it is not peer reviewed and has no machine-checked proof. Formalizing it would certify the cancellation analysis that drives the constant $2$ .

Difficulty

The natural attempt is to represent a nearly norming functional for the center as a convex combination of disjoint segment functionals and read off the tail. The obstacle is cancellation: two atoms leaving the head $H$ through the same vertex can have segment sums of opposite sign, and a naive estimate loses all control. The bound must also hold for every displacement with the same $H$ , so compactness arguments that choose $H$ after $y$ do not suffice, and an independent radial approach in the source gives only the weaker $(\sqrt2+\sqrt6)\sqrt{R(R-\|x\|)}$ .

Formalization scope

Vertices: ForestVertex is the subtype of pairs $(h,w)$ with $1\le h$ and $|w|\le h$ ; InfiniteVertex := List ℕ. Ancestry is equality of heights plus List.IsPrefix (resp. prefix only).
Segments: IsInterval ancestor S asserts $S=[a,b]$ with $a\preceq b$ , so segments are nonempty. A test family is a finite set of pairwise disjoint segments, and segmentSeminorm is the supremum of the Euclidean norms of the vectors of segment sums.
Spaces: X := StrongDual ℝ (UniformSpace.Completion (Test ForestVertex)); BInfinite is the closed span of the coordinate functionals inside the full dual of the infinite-tree completion, carrying the subspace (dual) norm.
head H x = ∑ v ∈ H, x(e_v) • e_v^* and tail H x = x - head H x; ancestrality is Ancestral.
Trivialization check: $R\ge0$ is required as in the source, and since $\|x\|\le R$ follows from the lens condition, the square root argument is never negative.

A full development needs the James segment norm, its completion and dual, contractivity of coordinate projections, the $\ell_2$ decomposition of the tail over descendant cones (Lemma 2.2), and the atomic description of finite head balls (Section 4). This infrastructure is shared with the other missions in the same family. Formalizations of Lemma 2.1, Lemma 2.2, Corollary 7.1 and Proposition 9.1 are welcome as supporting results.

Selected references

OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494
F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
N. Ghoussoub, B. Maurey, $G_\delta$ -embeddings in Hilbert space, J. Funct. Anal., 1985. https://doi.org/10.1016/0022-1236(85)90039-4

12 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: wurtle

Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree spaceResearch Paper

Motivation

Uniform convexity of a norm says that the midpoint of two far-apart points of the unit sphere lies strictly inside the ball. In infinite dimensions there is an asymptotic version: one only asks for a gain in directions that lie far out, that is, inside some closed subspace of finite codimension. Asymptotic uniform convexity and its relatives control the large-scale geometry of a Banach space, and in particular which infinite graphs can be embedded into the space with bounded distortion.

Two such properties are compared here. Asymptotic uniform convexity (AUC) demands a gain in every far-out direction separately; asymptotic midpoint uniform convexity (AMUC), introduced by Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016), only asks for a gain when a direction and its opposite are tested together. Every AUC norm is AMUC. The question is how far apart the two notions are, both up to renorming and in terms of metric embeddings of the countably branching diamond graphs $D_k$ .

Timeline

1974. James introduces the square-sum norm over disjoint segments of a tree (the James tree space) (doi:10.1090/S0002-9904-1974-13580-9).
2001. Girardi proves that the coordinate predual and the full dual of the binary James tree space are AUC (doi:10.4064/sm147-2-2).
2004 and 2009. Lee and Naor obtain quantitative $L_p$ distortion bounds for finite binary diamonds; Johnson and Schechtman relate diamond embeddings to super-reflexivity (doi:10.1007/s00039-004-0473-8, doi:10.1142/S1793525309000114).
2016. Dilworth et al. define AMUC and construct an AMUC norm on $\ell_2$ that is not AUC (doi:10.1016/j.jmaa.2015.11.061).
2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of the countably branching diamonds, and that for reflexive spaces with unconditional asymptotic structure, failure of AUC renormability forces uniform diamond embeddings (arXiv:1612.01984).
2018 and 2021. Swift extends the embedding construction to countably branching bundle graphs under the same hypotheses (arXiv:1710.00877); Perreau treats duals of separable spaces with weak-star unconditional asymptotic structure (arXiv:2104.10494).
2025. Baudier and Lancien record, as Problem 39 of their monograph, whether the diamond implication holds for general reflexive spaces (arXiv:2512.00817).
2026. Baudier shows that AMUC renormability does not imply AUC renormability, using the Kadets–Werner modification of the Bourgain–Rosenthal space, which is not reflexive (arXiv:2609.21283).

The source of this mission, an OpenAI preprint dated September 27, 2026, gives a reflexive example that separates the two notions and answers the reflexive diamond question negatively.

Setting

All spaces are real. For a Banach space $Y$ with norm $N$ , let $\operatorname{cof}(Y)$ be the closed subspaces of finite codimension. For $t>0$ ,

\overline\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\bigl(N(x+ty)-1\bigr),

\widehat\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\Bigl(\tfrac{N(x+ty)+N(x-ty)}{2}-1\Bigr).

$N$ is AUC if $\overline\delta_N(t)>0$ for every $t>0$ , and AMUC if $\widehat\delta_N(t)>0$ for every $t>0$ . A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ for some $0<a\le b$ .

The forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the rooted tree of words of length at most $h$ , ordered by extension. The forest $\mathcal F$ is the disjoint union of one copy of $T_h$ for every $h\ge1$ . A segment is an interval $[a,b]$ of an ancestral chain. For a finitely supported $u:\mathcal F\to\mathbb R$ ,

\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2} : S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\},\qquad u(S)=\sum_{v\in S}u(v).

Let $J$ be the completion and $X=J^*$ with the dual norm.

Diamonds. $D_0$ is one edge; $D_{k+1}$ replaces every edge of $D_k$ by countably many internally disjoint two-edge paths. With the shortest-path metric $d_k$ , a map $f:D_k\to X$ has distortion at most $C$ if some scale $s>0$ gives $s\,d_k(u,v)\le\|f(u)-f(v)\|\le Cs\,d_k(u,v)$ for all $u,v$ .

Formalization targets

Goal: Theorem 1.1

X\ \text{is infinite dimensional, separable and reflexive, and admits no equivalent AUC norm;}

\widehat\delta_X(t)\ \ge\ \sqrt{1+t^2/12}-1\quad(t>0);

\text{every embedding of }D_k\text{ into }X\text{ has distortion}\ \ge\ \sqrt{1+k/12}\quad(k\ge0).

The Lean statement OAI.ForestSpace.main_theorem is the conjunction of these six clauses. It is open on the platform.

Significance

The theorem separates AMUC from AUC renormability inside the reflexive class, which Baudier's 2026 example (non-reflexive) does not. Because AMUC is a property of the given norm while the diamond obstruction is invariant under renorming, the theorem also shows that, for general reflexive spaces, failure of AUC renormability does not force the countably branching diamonds to embed uniformly. This answers Problem 39 of Baudier–Lancien negatively and shows that the unconditional asymptotic structure hypothesis in the 2017 embedding theorem cannot simply be dropped. The quantitative modulus and distortion bounds are explicit, not merely positivity statements.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify the full construction, including reflexivity of $J^*$ for a non-locally-finite forest and the square-sum distortion recursion.

Difficulty

Two points are delicate. First, reflexivity: the classical James tree space is not reflexive, and here reflexivity comes from using trees of finite but unbounded height together with countable branching; the full dual $J^*$ , not the coordinate completion, is the space. Second, the midpoint estimate: a segment test may cross from a finite ancestral set to its complement, and simply adding norming tests for the two parts produces uncontrolled positive cross terms. Non-renormability, by contrast, must be proved for every equivalent norm at once, so it cannot be read off from any computation with the given norm.

Formalization scope

The space is FullDual Vertex := StrongDual ℝ (J Vertex), where J V is the UniformSpace.Completion of TestVector V (finitely supported functions with norm rho). Vertex packs a height $h\ge1$ and a word in $\mathbb N^*$ of length $\le h$ ; the order is equality of heights plus prefix order.
Segments are finite order-convex chains (IsSegment); the empty segment is allowed and contributes zero.
Reflexive is surjectivity of the canonical map NormedSpace.inclusionInDoubleDual, not an abstract isomorphism with the bidual.
EquivalentNorm E α β stores a Seminorm with explicit constants $0<\alpha\le\beta$ ; the lower bound makes it a norm. The non-renormability clause quantifies over all such structures.
aucModulus and averageModulus take the inf/sup/inf order above, with sInf/sSup over real sets; for an infinite-dimensional space these sets are nonempty and bounded, so the Lean defaults are not triggered.
Diamond.diamond k iterates the edge replacement starting from one edge; distances are SimpleGraph.dist of the undirected graph, and EmbeddingBound is the scaled bi-Lipschitz condition above.

A complete development needs the James-type segment norm, its completion and dual, coordinate projections onto ancestral sets, and graph distances on the diamonds. The segment-norm and diamond infrastructure is shared with the other missions of this family. Contributions formalizing Lemma 2.1 (structure and reflexivity), Lemma 3.2 (bounded trees exclude AUC renorming), Lemma 4.1 (paired head–tail estimate) and Lemma 5.1 (lens lemma) are welcome.

Selected references

OpenAI, Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026/manuscript.pdf
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
F. P. Baudier, G. Lancien, Asymptotic and nonlinear geometries of Banach spaces and their interactions, Cours Spécialisés, SMF, 2026. https://arxiv.org/abs/2512.00817
F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
A. Swift, A coding of bundle graphs and their embeddings into Banach spaces, Mathematika, 2018. https://arxiv.org/abs/1710.00877
Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494

27 thms2 active usersReviewed

Completed

Analysis Functional Analysis·Captain: wurtle

A positive solution to Tingley’s problemResearch Paper

Motivation: isometries of unit spheres

The Mazur–Ulam theorem (1932) says that every surjective isometry between real normed spaces is affine. The whole space is not always available, though: often only distances between unit vectors are known. Tingley's problem (1987) asks whether the metric of the unit sphere alone already determines the linear structure, that is, whether every surjective isometry between the unit spheres of two real Banach spaces extends to a real-linear isometry of the spaces (Tingley 1987). The question has been studied for almost four decades, mostly class by class: for sequence spaces, $L^p$ spaces, operator algebras and two-dimensional spaces. Nearly all known positive results depend on the structure of the particular spaces involved.

Timeline

1932 — Mazur and Ulam: surjective isometries between real normed spaces are affine.
1972 — Mankiewicz extends isometries between convex sets with nonempty interior. A unit sphere has empty interior, so this does not apply.
1987 — Tingley poses the problem and shows that surjective isometries between spheres of finite-dimensional spaces preserve antipodal points (Tingley 1987).
1994 — Wang treats spheres of $C_0(\Omega)$ -type spaces (Wang 1994).
2003 — Ding handles $\ell^p(\Gamma)$ -type spaces, $p>1$ , $p\ne 2$ (Ding 2003).
2011 — Cheng and Dong formulate the Mazur–Ulam property (sphere isometries from a given space into an arbitrary target extend linearly) (Cheng–Dong 2011).
2012 — Tan proves the Mazur–Ulam property for real $L^p(\mu)$ , $1<p<\infty$ , $p\neq 2$ (Tan 2012).
2014 — Tanaka: sphere isometries preserve maximal convex subsets of the sphere (Tanaka 2014).
2018 — Fernández-Polo and Peralta (von Neumann algebras, JMAA 2018); Mori (preduals, JMAA 2018).
2020 — Mori and Ozawa: Mazur–Ulam property for unital $C^*$ -algebras and real von Neumann algebras (Studia Math. 2020).
2022 — Banakh: every two-dimensional real Banach space has the Mazur–Ulam property (Banakh 2022).
2025–2026 — Further class results: Schreier spaces (Fakhoury 2025); Haagerup noncommutative $L_p$ and Schatten classes (Huang–Zhu, arXiv:2608.30131; arXiv:2607.11244).
2026 — An OpenAI preprint, A positive solution to Tingley's problem (OpenAI Math Release, September 23, 2026), claims the general affirmative answer for all real Banach spaces. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Let $X$ and $Y$ be real Banach spaces, both nonzero. The unit sphere is $S_X=\{x\in X:\|x\|=1\}$ with the metric inherited from $X$ . A map $f:S_X\to S_Y$ is an isometry if $\|f(x)-f(y)\|=\|x-y\|$ for all $x,y\in S_X$ , and it is surjective if every point of $S_Y$ is attained.

Any linear extension of $f$ is forced to be the radial extension

T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\frac{x}{\|x\|}\right)\quad(x\neq 0).

In Lean, UnitSphere X is the subtype $\{x : X \mid \|x\|=1\}$ and normalize x hx is $x/\|x\|$ as an element of it.

Formalization targets

Goal: Tingley's problem (Theorem 1.1)

For nonzero real Banach spaces $X,Y$ and every surjective isometry $f:S_X\to S_Y$ there is a surjective real-linear isometry $T:X\to Y$ such that

T|_{S_X}=f,\qquad T(0)=0,\qquad T(x)=\|x\|\,f\!\left(\tfrac{x}{\|x\|}\right)\ (x\neq0),

and $T$ is the only real-linear map $X\to Y$ that agrees with $f$ on $S_X$ . This is the full statement of Theorem 1.1 of the source. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. An affirmative answer turns a forty-year class-by-class programme into a single theorem: the metric of the unit sphere of any real Banach space determines the space up to linear isometry. Every space then has the Mazur–Ulam property in the sense of Cheng and Dong, with no separability, reflexivity, smoothness or strict convexity assumptions. For complex Banach spaces viewed as real spaces the conclusion is real-linearity only; complex-linearity is not claimed.

Formalizing it. The claimed proof combines classical tools (supporting functionals, Banach-space ultrapowers, Darbo's fixed-point theorem with the Kuratowski measure of noncompactness, the Mazur–Ulam theorem) with new geometric estimates on aligned chords. A machine-checked proof would certify a result whose proof has not yet been refereed. The Mazur–Ulam theorem itself is already in Mathlib (IsometryEquiv.toRealLinearIsometryEquiv); ultrapowers of Banach spaces and Darbo's theorem are not.

Difficulty

The radial map $T$ preserves norms and preserves distances between points of the same radius. What has to be shown is that it preserves distances between points on different spheres, $\|f(x)-qf(y)\|=\|x-qy\|$ for $0<q<1$ , using only distances measured on a single sphere. Once this holds, $T$ is a surjective isometry fixing $0$ and Mazur–Ulam gives linearity. The obvious attempt (extend the isometry to a neighbourhood, or use convex-set extension theorems such as Mankiewicz's) fails because the sphere has empty interior. Structural arguments (smoothness, facial structure, explicit duals) cover only special classes of spaces. In general, the maximal defect $\sup|\|f(x)-qf(y)\|-\|x-qy\||$ need not be attained, and no compactness is available in infinite dimensions.

Formalization scope

$X$ and $Y$ are arbitrary types with NormedAddCommGroup, NormedSpace ℝ and CompleteSpace, and Nontrivial (the source's "nonzero"). Universe levels are independent, and no separability or dimension hypothesis is imposed.
The sphere is UnitSphere X := {x // ‖x‖ = 1} with the subtype metric; Isometry f and Function.Surjective f are the hypotheses.
The conclusion is an existential over X ≃ₗᵢ[ℝ] Y (a bijective real-linear isometry) with the five clauses: agreement on the sphere, $T0=0$ , the radial formula, surjectivity, and uniqueness among all X →ₗ[ℝ] Y that agree with $f$ on the sphere. No hypothesis assumes any distance between different radii, so the statement is not trivialized.
Infrastructure a full development needs: Hahn–Banach supporting functionals, Banach-space ultrapowers (or another attainment device), the Kuratowski measure of noncompactness and Darbo's fixed-point theorem, together with Mathlib's Mazur–Ulam theorem. Ultrapowers and Darbo's theorem would be reusable well beyond this mission.

Selected references

D. Tingley, Isometries of the unit sphere, Geom. Dedicata 22 (1987), 371–378. https://doi.org/10.1007/BF00147942
S. Mazur and S. Ulam, Sur les transformations isométriques d'espaces vectoriels normés, C. R. Acad. Sci. Paris 194 (1932), 946–948.
P. Mankiewicz, On extension of isometries in normed linear spaces, Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 20 (1972).
R. S. Wang, Isometries between the unit spheres of $C_0(\Omega)$ type spaces, Acta Math. Sci. 14 (1994), 82–89. https://doi.org/10.1016/S0252-9602(18)30093-6
G. G. Ding, The isometric extension problem in the unit spheres of $\ell^p(\Gamma)$ $(p>1)$ type spaces, Sci. China Ser. A 46 (2003), 333–338. https://doi.org/10.1360/03ys9035
L. Cheng and Y. Dong, On a generalized Mazur–Ulam question, J. Math. Anal. Appl. 377 (2011), 464–470. https://doi.org/10.1016/j.jmaa.2010.11.025
D.-N. Tan, Extension of isometries on the unit sphere of $L^p$ spaces, Acta Math. Sin. (Engl. Ser.) 28 (2012), 1197–1208. https://doi.org/10.1007/s10114-011-0302-6
R. Tanaka, A further property of spherical isometries, Bull. Aust. Math. Soc. 90 (2014), 304–310. https://doi.org/10.1017/S0004972714000185
F. J. Fernández-Polo and A. M. Peralta, On the extension of isometries between the unit spheres of von Neumann algebras, J. Math. Anal. Appl. 466 (2018), 127–143. https://doi.org/10.1016/j.jmaa.2018.05.062
M. Mori, Tingley's problem through the facial structure of operator algebras, J. Math. Anal. Appl. 466 (2018), 1281–1298. https://doi.org/10.1016/j.jmaa.2018.06.050
M. Mori and N. Ozawa, Mankiewicz's theorem and the Mazur–Ulam property for $C^*$ -algebras, Studia Math. 250 (2020), 265–281. https://doi.org/10.4064/sm180727-14-11
T. Banakh, Every 2-dimensional Banach space has the Mazur–Ulam property, Linear Algebra Appl. 632 (2022), 268–280. https://doi.org/10.1016/j.laa.2021.09.020
G. Darbo, Punti uniti in trasformazioni a codominio non compatto, Rend. Sem. Mat. Univ. Padova 24 (1955), 84–92.
OpenAI, A positive solution to Tingley's problem, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-positive-solution-to-Tingleys-problem-September-23-2026/paper.pdf

63 thms2 active usersReviewed

Completed

Algebraic Topology Category Theory·Captain: wurtle

Thomason Model Structures in Every Strict Higher DimensionResearch Paper

Motivation

A model structure on a category specifies weak equivalences, fibrations and cofibrations so that the category carries a homotopy theory. Thomason showed that the category $\mathbf{Cat}$ of small categories carries a model structure Quillen equivalent to simplicial sets, so that ordinary categories model all homotopy types of spaces (Thomason 1980). Its weak equivalences are the functors whose nerves are weak homotopy equivalences.

Strict higher categories have a nerve too: Street's orientals $\mathcal O_m$ give the Street nerve $N_n$ of a strict $n$ -category (Street 1987). The higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis asks for the analogue of Thomason's theorem for strict globular $n$ -categories for every $1\le n\le\infty$ (Ara–Maltsiniotis 2014; Ara 2023, §§9.2.5–9.2.6; Guetta–Maltsiniotis 2024). Strict higher categories are already known to describe the homotopy category of spaces after localization (Gagna, below); the conjecture asks for the full model structure, with lifting and factorization on all strict $n$ -categories.

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims the conjecture in every dimension. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Timeline

1980 — Thomason constructs the model structure on $\mathbf{Cat}$ by transfer along $c\,\mathrm{Sd}^2\dashv\mathrm{Ex}^2N$ , introducing Dwyer maps (Cahiers 1980).
1987 — Street defines orientals and the nerve of strict $\omega$ -categories (JPAA 1987).
1999 — Cisinski corrects the retract argument in Thomason's properness proof (Cahiers 1999).
2007/2016 — Worytkiewicz, Hess, Parent and Tonks propose the 2-dimensional structure (JPAA 2007), with a later corrigendum (JPAA 2016).
2010 — Fiore and Paoli construct a Thomason structure on $n$ -fold categories (AGT 2010).
2014 — Ara and Maltsiniotis develop the transfer theorem, settle dimension 2, and isolate sufficient conditions for all $n$ (Adv. Math. 2014).
2018 — Gagna shows that strict $n$ -categories model homotopy types after localizing at nerve weak equivalences (Adv. Math. 2018).
2023–2024 — Ara's habilitation records the remaining pushout condition and the conjecture; Guetta and Maltsiniotis state the $\omega$ -dimensional conjecture.
2026 — The OpenAI preprint claims the conjecture for every $1\le n\le\infty$ (Theorem 1.1, p. 2).

Setting

A strict globular $\omega$ -category has a set of cells, source and target operations $s_k,t_k$ in each dimension, and associative, unital compositions $\ast_k$ along $k$ -dimensional boundaries satisfying the interchange law; every cell has finite dimension. A strict $n$ -category is one whose cells above dimension $n$ are identities; $n\mathbf{Cat}$ denotes the category of small strict $n$ -categories and strict functors ( $n=\infty$ means $\omega\mathbf{Cat}$ ). No invertibility is assumed.

The Street nerve $N_n:n\mathbf{Cat}\to\mathbf{sSet}$ has $(N_nX)_m=\mathrm{Hom}(\mathcal O_m,X)$ , with left adjoint $c_n$ . With barycentric subdivision $\mathrm{Sd}\dashv\mathrm{Ex}$ set

L_n=c_n\mathrm{Sd}^2,\qquad R_n=\mathrm{Ex}^2N_n .

Let $W_{KQ}$ and $\mathrm{Fib}_{KQ}$ be the weak homotopy equivalences and Kan fibrations, $I=\{\partial\Delta[m]\hookrightarrow\Delta[m]\}_{m\ge0}$ and $J=\{\Lambda^k[m]\hookrightarrow\Delta[m]\}_{m\ge1}$ . Define

W_n=R_n^{-1}(W_{KQ}),\qquad F_n=R_n^{-1}(\mathrm{Fib}_{KQ}),\qquad C_n={}^{\perp}(F_n\cap W_n).

Formalization targets

Milestone: Equation (7.1), p. 24 — nerve detection

$W_n=N_n^{-1}(W_{KQ})=R_n^{-1}(W_{KQ})$ : a functor of strict $n$ -categories is a weak equivalence exactly when its Street nerve is a weak homotopy equivalence. This follows from $\mathrm{id}\to\mathrm{Ex}$ being a natural weak equivalence.

Goal: Theorem 1.1 (p. 2)

For every $n\in\{1,2,3,\dots\}\cup\{\infty\}$ , $(C_n,W_n,F_n)$ is a proper combinatorial model structure on $n\mathbf{Cat}$ , cofibrantly generated by $(L_nI,L_nJ)$ , and

L_n:\mathbf{sSet}_{KQ}\rightleftarrows(n\mathbf{Cat},C_n,W_n,F_n):R_n

is a Quillen equivalence.

Significance

The result itself. The theorem says that strict higher categories, in every dimension, model the homotopy theory of spaces through a genuine model structure, not only after localization. It provides functorial factorizations and lifting on arbitrary strict $n$ -categories, including those that are not freely generated, which is what the small-object argument needs. The key new input is a couniversality theorem: pushouts of $c_nN(A)\to c_nN(E)$ along sieves with a right adjoint retraction are Street weak equivalences (Theorem 5.2, p. 18), which is the remaining sufficient condition of Ara–Maltsiniotis.

Formalizing it. Mathlib has simplicial sets and model-category foundations but no strict $\omega$ -categories, orientals or Street nerve. A complete development adds these, Steiner's directed complexes, Gray cylinders and local presentability of $n\mathbf{Cat}$ , all reusable in higher category theory.

Difficulty

The transfer theorem reduces the model structure to a pushout condition, and that is the hard part: categorical pushouts of strict $n$ -categories can create many new composites, so the nerve of a pushout is not the pushout of nerves. Thomason controlled this in dimension 1 with Dwyer maps, but that method does not extend directly. The preprint builds explicit stationary directed prisms (Lemma 3.1, p. 10) that are constant on the old part, so contractions glue across any attachment, and then reduces general posets to finite ones via sieve covers (Corollary 4.5, p. 16; Lemma 4.6, p. 17). Properness (Proposition 7.3, p. 26) and the unit comparison after two subdivisions (Proposition 7.4, p. 27) are separate arguments.

Formalization scope

OmegaCategory is a structure with a type of cells, source/target maps indexed by ℕ, partial compositions, the globular, unit, associativity and interchange laws, and finite dimension of each cell. Finite $n$ uses a full subcategory NCategory n.
FullMain asserts: the Kan–Quillen model structure on SSet exists with the standard classes; and, for $\omega$ and every finite $n\ge1$ , an ExactModelEndpoint for $L_n\dashv R_n$ : a ModelCategory whose weak equivalences, fibrations and cofibrations are exactly $W_n,F_n,C_n$ ; $(L_nI)^{\pitchfork}=F_n\cap W_n$ and $(L_nJ)^{\pitchfork}=F_n$ ; both weak factorization systems; completeness, cocompleteness and local presentability; left and right properness; $L_n$ left Quillen; and the Quillen-equivalence criterion at fibrant targets.
The classes are fixed by equations, so the goal cannot be met by an unrelated model structure.
The milestone quantifies over every n : ℕ, including $n=0$ , which the source does not consider; the identity holds there by the same argument.

Selected references

OpenAI, Thomason Model Structures in Every Strict Higher Dimension, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026/paper.pdf
R. W. Thomason, Cat as a closed model category, Cahiers Topologie Géom. Différentielle 21 (1980). https://www.numdam.org/item/CTGDC_1980__21_3_305_0/
R. Street, The algebra of oriented simplexes, J. Pure Appl. Algebra (1987). https://doi.org/10.1016/0022-4049(87)90137-X
D.-C. Cisinski, La classe des morphismes de Dwyer n'est pas stable par rétractes, Cahiers (1999). https://www.numdam.org/item/CTGDC_1999__40_3_227_0/
D. Ara, G. Maltsiniotis, Vers une structure de catégorie de modèles à la Thomason sur la catégorie des n-catégories strictes, Adv. Math. (2014). https://doi.org/10.1016/j.aim.2014.03.013
A. Gagna, Strict n-categories and augmented directed complexes model homotopy types, Adv. Math. (2018). https://doi.org/10.1016/j.aim.2018.04.010
D. Ara, Théorie de l'homotopie des ∞-catégories strictes, habilitation (2023). https://www.normalesup.org/~ara/files/hdr.pdf
L. Guetta, G. Maltsiniotis, Homologie polygraphique des systèmes locaux, Adv. Math. (2024). https://doi.org/10.1016/j.aim.2024.109719
T. M. Fiore, S. Paoli, A Thomason model structure on the category of small n-fold categories, Algebr. Geom. Topol. 10 (2010). https://doi.org/10.2140/agt.2010.10.1933
P. G. Goerss, J. F. Jardine, Simplicial Homotopy Theory, Birkhäuser (1999). https://doi.org/10.1007/978-3-0348-8707-6

6 thms2 active usersReviewed

Functional Analysis·Captain: wurtle

Weak pure infiniteness and O-infinity absorptionResearch Paper

Motivation

Purely infinite $C^*$ -algebras are the infinite counterpart of the finite, tracial algebras: every positive element can absorb copies of itself. In the simple case they are the Kirchberg algebras, classified by K-theory. For non-simple algebras, Kirchberg and Rørdam introduced three versions of pure infiniteness (weak, ordinary, strong) and showed that the strongest one is equivalent, for separable nuclear algebras, to absorbing the Cuntz algebra $\mathcal O_\infty$ tensorially, the regularity property that underlies Kirchberg's classification of non-simple purely infinite algebras. Whether the three notions coincide is Kirchberg–Rørdam's Question 9.5, listed as Problem LXXII by Schafhauser, Tikuisis and White.

Timeline

1978. Cuntz introduces the comparison relation $\precsim$ on positive elements (doi:10.1007/BF01421922).
2000. Kirchberg and Rørdam define pure infiniteness for non-simple algebras (doi:10.1353/ajm.2000.0021).
2002. Kirchberg and Rørdam introduce weak and strong pure infiniteness, prove $\mathcal O_\infty$ -absorption equivalences, settle the simple, real-rank-zero and approximately divisible cases, and pose Question 9.5 (doi:10.1006/aima.2001.2041).
2004. Blanchard and Kirchberg prove ordinary implies strong when the primitive ideal space is Hausdorff (doi:10.1016/j.jfa.2003.06.008); Rørdam treats $\mathcal Z$ -absorbing algebras (arXiv:math/0408020).
2006. Kirchberg's central-sequence results extend absorption to general nonunital separable nuclear algebras (doi:10.1007/978-3-540-34197-0_10).
2007. Pasnicu and Rørdam settle algebras with the ideal property (arXiv:math/0606378).
2016. Kirchberg and Sierakowski give the formulation of strong pure infiniteness used here (arXiv:1503.08519).
2023. Thiel and Vilalta study the Global Glimm Property (doi:10.1090/tran/8880); Elliott and Rouzbehani prove weak implies ordinary in topological dimension zero.
2025–2026. Pasnicu and Rouzbehani prove ordinary implies strong in topological dimension zero (doi:10.5565/PUBLMAT6922506); Ng, Thiel and Vilalta recover weak-to-ordinary via the Global Glimm Property (arXiv:2507.16261); Schafhauser, Tikuisis and White record Problem LXXII (arXiv:2506.10902).

The source of this mission is an OpenAI preprint dated September 25, 2026, which proves ordinary $\Rightarrow$ strong in general and weak $\Rightarrow$ ordinary for exact algebras.

Setting

All $C^*$ -algebras are complex and may be nonunital or nonseparable. For positive $u,v$ in matrices over $C$ (or in $C\otimes\mathcal K$ ), write $u\precsim v$ (Cuntz subequivalence) if there are $x_j$ with $x_j^*vx_j\to u$ in norm; matrices of different sizes are compared after zero padding. A positive $h$ is properly infinite if $h\oplus h\precsim h$ (zero counts as properly infinite). The paper uses two conditions:

(P) every $h\in C_+$ is properly infinite (ordinary pure infiniteness, by Kirchberg–Rørdam);
( $F_n$ ) for one fixed $n\ge1$ , $h^{\oplus n}$ is properly infinite for every $h\in C_+$ (weak pure infiniteness).

$C$ is strongly purely infinite if for all $x,y\in C_+$ and $\varepsilon>0$ there are $s,t\in C$ with

\|s^*x^2s-x^2\|<\varepsilon,\qquad \|t^*y^2t-y^2\|<\varepsilon,\qquad \|s^*xyt\|<\varepsilon.

$C$ is exact if $C\otimes_{\min}-$ preserves short exact sequences of $C^*$ -algebras.

Formalization targets

Milestone: Theorem 1.1

If $C$ satisfies (P), then for all $a,b\in C_+$ , $c\in C$ , $\varepsilon>0$ there are $s,t$ with

\|s^*as-a\|<\varepsilon,\quad\|t^*bt-b\|<\varepsilon,\quad\|s^*ct\|<\varepsilon;

in particular $C$ is strongly purely infinite.

Milestone: Theorem 1.2, first conclusion

C\ \text{exact and }(F_n)\ \Longrightarrow\ (P).

Goal: Theorem 1.2

C\ \text{exact and }(F_n)\ \text{for some }n\ge1\ \Longrightarrow\ C\ \text{strongly purely infinite}.

The Lean statement OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite is open on the platform.

Significance

Theorem 1.1 answers the ordinary-to-strong part of Problem LXXII for arbitrary algebras, and Theorem 1.2 answers the whole comparison question for exact (hence for nuclear) algebras. With Kirchberg's results, every separable nuclear algebra satisfying ( $F_n$ ) absorbs $\mathcal O_\infty$ (Corollary 1.3), with no unitality or simplicity assumption: a single finite amplification test characterizes this tensorial regularity. The weak-to-ordinary implication for non-exact algebras remains open.

These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.

Difficulty

For non-simple algebras, comparing one positive element with itself and comparing two elements simultaneously are different demands: strong pure infiniteness must also kill a mixed entry $s^*xyt$ , and earlier proofs needed control of the ideal structure (Hausdorff primitive spectrum, ideal property, topological dimension zero). Removing a fixed amplification similarly needs enough orthogonal equivalent pieces in hereditary subalgebras, which earlier work extracted from Global Glimm-type hypotheses. The difficulty is to obtain this uniformly over primitive quotients when $\mathrm{Prim}(C)$ is not Hausdorff.

Formalization scope

Algebras are NonUnitalCStarAlgebra with the $C^*$ order (StarOrderedRing); no unit, separability or simplicity is assumed.
In the exact group, Cuntz subequivalence is between CStarMatrix blocks, witnessed by rectangular matrices $v$ with $\|v^*bv-a\|<\varepsilon$ for every $\varepsilon$ ; $h^{\oplus n}$ is diagonalCopies n h; WeaklyPurelyInfinite fixes one $n\ge1$ before quantifying over nonzero positives.
Exact is stated with minimal tensor products realized inside $\ell^\infty$ over all pairs of Hilbert-space representations, and tests surjections $q:C\to D$ in the same universe.
In the Theorem 1.1 group, Cuntz comparison is in the stabilization (completion of the union of matrix algebras, i.e. $C\otimes\mathcal K$ ), and PropertyP is (P).
StronglyPurelyInfinite is the three-inequality condition above, with no norm bound on $s,t$ .

A complete development needs Cuntz comparison, stabilizations, minimal tensor products and exactness, primitive ideal spaces and hereditary subalgebras; this is reusable for other regularity missions. Contributions formalizing Proposition 2.2-style transport lemmas and Corollary 1.3 (via Kirchberg's absorption theorem) are welcome.

Selected references

OpenAI, Weak pure infiniteness and $\mathcal O_\infty$ absorption, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026/paper.pdf
E. Kirchberg, M. Rørdam, Non-simple purely infinite $C^*$ -algebras, Amer. J. Math., 2000. https://doi.org/10.1353/ajm.2000.0021
E. Kirchberg, M. Rørdam, Infinite non-simple $C^*$ -algebras: absorbing the Cuntz algebra $\mathcal O_\infty$ , Adv. Math., 2002. https://doi.org/10.1006/aima.2001.2041
E. Kirchberg, A. Sierakowski, Filling families and strong pure infiniteness, 2016. https://arxiv.org/abs/1503.08519
E. Blanchard, E. Kirchberg, Non-simple purely infinite $C^*$ -algebras: the Hausdorff case, J. Funct. Anal., 2004. https://doi.org/10.1016/j.jfa.2003.06.008
C. Pasnicu, M. Rørdam, Purely infinite $C^*$ -algebras of real rank zero, J. Reine Angew. Math., 2007. https://doi.org/10.1515/CRELLE.2007.091
E. Kirchberg, Central sequences in $C^*$ -algebras and strongly purely infinite algebras, Abel Symposium, 2006. https://doi.org/10.1007/978-3-540-34197-0_10
C. Schafhauser, A. Tikuisis, S. White, Nuclear $C^*$ -algebras: 99 problems, 2026. https://arxiv.org/abs/2506.10902

30 thms2 active usersReviewed

Completed

Functional Analysis Probability Random Matrix Theory·Captain: wurtle

A finite-entropy separation of microstates and nonmicrostates free entropyResearch Paper

Motivation

Free probability treats bounded self-adjoint operators $X_1,\dots,X_n$ in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy $\chi(X)$ measures how large the set of matrix tuples imitating the joint moments of $X$ is (Voiculescu 1994). The nonmicrostates free entropy $\chi^*(X)$ is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does $\chi(X)>-\infty$ imply $\chi(X)=\chi^*(X)$ ? (Guionnet 2004, Conjecture 7.1).

The question matters because $\chi$ carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while $\chi^*$ is far more computable. Equality would let analytic computations of $\chi^*$ transfer to $\chi$ .

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with $-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty$ . The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

1991 — Voiculescu proves asymptotic freeness of independent GUE matrices (Invent. Math. 1991), the random-matrix input behind microstates.
1994 — Voiculescu defines the microstates free entropy $\chi$ (Invent. Math. 1994); Speicher develops the noncrossing cumulant calculus (Math. Ann. 1994).
1996 — Ge uses microstates entropy to prove that $L(F_2)$ is prime (PNAS 1996).
1998 — Voiculescu defines free Fisher information via conjugate variables and the nonmicrostates entropy $\chi^*$ (Invent. Math. 1998).
2002–2004 — Voiculescu's survey lists the unification problem (Bull. LMS 2002); Guionnet states the finite-entropy equality conjecture (Probab. Surv. 2004).
2003 — Biane, Capitaine and Guionnet prove $\chi\le\chi^*$ in general (Invent. Math. 2003).
2017–2020 — Equality is established for regular convex potentials by Dabrowski (arXiv:1604.06420) and Jekel (Anal. PDE 2020).
2024 — Jekel and Pi give an elementary proof of $\chi\le\chi^*$ , including the conditional version (Doc. Math. 2024).
2026 — The OpenAI preprint claims a strict gap with both entropies finite (Theorem 1.1, p. 2).

Setting

Let $M$ be a von Neumann algebra with a faithful normal tracial state $\tau$ , and $X=(X_1,\dots,X_n)$ a tuple of self-adjoint elements of $M$ .

Microstates. For $R>0$ , $m\in\mathbb N$ , $\varepsilon>0$ and a matrix size $d$ , let $\Gamma_R(X;m,d,\varepsilon)$ be the set of $n$ -tuples of self-adjoint $d\times d$ complex matrices with operator norms at most $R$ whose normalized traces $d^{-1}\mathrm{Tr}$ of all words of length $\le m$ are within $\varepsilon$ of the corresponding $\tau$ -moments of $X$ . Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then

\chi_R(X)=\inf_{m,\varepsilon}\ \limsup_{d\to\infty}\Bigl[d^{-2}\log\mathrm{Vol}\,\Gamma_R(X;m,d,\varepsilon)+\tfrac n2\log d\Bigr],\qquad \chi(X)=\sup_{R>0}\chi_R(X).

Free Fisher information. Vectors $\xi_1,\dots,\xi_n$ in the $L^2(\tau)$ -closure of polynomials in $X$ are conjugate variables if $\tau(\xi_i P(X))=(\tau\otimes\tau)((\partial_iP)(X))$ for every noncommutative polynomial $P$ , where $\partial_i$ is the free difference quotient. Then $\Phi^*(X)=\sum_i\|\xi_i\|_2^2$ , or $+\infty$ if no conjugate variables exist.

Nonmicrostates entropy. With $S=(S_1,\dots,S_n)$ a standard free semicircular family free from $X$ ,

\chi^*(X)=\frac n2\log(2\pi e)+\frac12\int_0^\infty\Bigl(\frac n{1+s}-\Phi^*(X+\sqrt s\,S)\Bigr)\,ds .

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist $n\ge2$ and a bounded self-adjoint tuple $X$ in a von Neumann algebra with faithful normal tracial state such that

-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty .

The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family $S$ required to lie in the same algebra.

Significance

The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of $\chi$ does not force $\chi=\chi^*$ , so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.

Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison $\chi\le\chi^*$ in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.

Difficulty

Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the $\limsup$ over matrix size in $\chi$ and the integral over noise time in $\chi^*$ . The preprint's tuple couples free semicirculars with a commuting discrete variable $Y$ that creates spectral blocks; after perturbing by small semicircular noise, $\chi$ is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes $\chi^*$ nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of $\chi\le\chi^*$ loses exactly the deficit being sought.

Formalization scope

The algebra is a VonNeumannAlgebra H on a complex Hilbert space $H$ ; the trace is a vector state given by a unit vector that is tracial on $M$ and separating for $M$ (so the state is faithful and normal).
$X$ and $S$ are Fin n-indexed self-adjoint elements of $M$ . FreeStandardNoise requires each $S_i$ to have the semicircle moments (Catalan numbers) and the unital algebras generated by $X$ and by each $S_i$ to be free.
Conjugate systems are vectors in the closed span of word vectors satisfying the derivative-moment identities; free Fisher information is an infimum in ℝ≥0∞, equal to $\infty$ when no conjugate system exists.
$\chi^*$ is an EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over $(0,\infty)$ .
$\chi$ uses explicit real coordinates for Hermitian matrices that make the Euclidean volume equal to Hilbert–Schmidt volume, matrix sizes $d+1$ to avoid $d=0$ , and EReal logarithms (volume zero gives $-\infty$ ).
The finiteness conditions are part of the conclusion, so a degenerate witness with $\chi=-\infty$ or $\chi^*=\infty$ does not satisfy the goal.

Selected references

OpenAI, A finite-entropy separation of microstates and nonmicrostates free entropy, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf
D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. II, Invent. Math. 118 (1994), 411–440. https://doi.org/10.1007/BF01231539
D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. V, Invent. Math. 132 (1998), 189–227. https://doi.org/10.1007/s002220050222
D. Voiculescu, Free entropy, Bull. London Math. Soc. 34 (2002), 257–278. https://doi.org/10.1112/S0024609301008992
A. Guionnet, Large deviations and stochastic calculus for large random matrices, Probab. Surv. 1 (2004), 72–172. https://doi.org/10.1214/154957804100000033
P. Biane, M. Capitaine, A. Guionnet, Large deviation bounds for matrix Brownian motion, Invent. Math. 152 (2003), 433–459. https://doi.org/10.1007/s00222-002-0281-4
D. Jekel, J. Pi, An elementary proof of the inequality χ ≤ χ for conditional free entropy*, Doc. Math. 29 (2024), 1085–1124. https://doi.org/10.4171/DM/969
D. Jekel, An elementary approach to free entropy theory for convex potentials, Anal. PDE 13 (2020), 2289–2374. https://doi.org/10.2140/apde.2020.13.2289
D. Voiculescu, Limit laws for random matrices and free products, Invent. Math. 104 (1991), 201–220. https://doi.org/10.1007/BF01245072

6 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Relative generation and the generator problem for finite factorsResearch Paper

Motivation

A von Neumann algebra is a unital algebra of bounded operators on a Hilbert space that is closed under adjoints and in the weak operator topology. For a set $S$ of operators, $W^*(S)$ denotes the smallest von Neumann algebra containing $S$ . The generator problem, going back to Kadison's 1967 list of problems, asks whether every von Neumann algebra with separable predual is singly generated, $M=W^*(x)$ for a single bounded operator $x$ ; equivalently, whether two self-adjoint operators always suffice. It is one of the oldest structural questions about von Neumann algebras, and by classical reductions everything comes down to type II $_1$ factors.

Timeline

1962–1969. Pearcy proves single generation for type I algebras (doi:10.2307/2034069); Suzuki and Saitô for hyperfinite algebras (1963, doi:10.2748/tmj/1178243811); Wogen for properly infinite algebras (1969, doi:10.1090/S0002-9904-1969-12157-9); Douglas and Pearcy develop matrix-generation techniques (1969, doi:10.1307/mmj/1029000161).
1972. Behncke treats tensor products of two II $_1$ factors (doi:10.2748/tmj/1178241478).
1974. Willig's direct-integral theorem reduces the general problem to II $_1$ factors (doi:10.2748/tmj/1178241231).
1981. Popa constructs irreducible hyperfinite subfactors (doi:10.1007/BF01389015).
1985–2002. Popa treats factors with Cartan subalgebras (doi:10.7146/math.scand.a-12110); Ge and Popa treat property $\Gamma$ factors (1998, doi:10.1215/S0012-7094-98-09405-4); Ge and Shen treat certain property (T) factors (2002, doi:10.1073/pnas.022593699).
2008–2009. Dykema, Sinclair, Smith and White study generator invariants and their amplification formula (arXiv:0706.1953); Shen's generator invariant unifies the positive classes (arXiv:math/0511327).
2012. Sherman shows that finite generation of every countably generated II $_1$ factor would suffice (arXiv:0908.4565).
2021. Popa studies tight decompositions and stable single generation (arXiv:1910.14653).
2025. Gao, Kunnawalkam Elayavalli, Patchell and Tan prove single generation under an internal sequential-commutation hypothesis (arXiv:2404.12380).

The source of this mission is an OpenAI preprint dated September 23, 2026, which claims single generation for every II $_1$ factor with separable predual.

Setting

Let $H$ be a complex Hilbert space and $M\subseteq B(H)$ a unital $*$ -subalgebra closed in the weak operator topology. $M$ is a factor if its centre is $\mathbb C1$ ; it is finite if every isometry $v\in M$ ( $v^*v=1$ ) is unitary; it is diffuse if every nonzero projection has a proper nonzero subprojection. A nonzero finite diffuse factor is a type II $_1$ factor; it carries a unique faithful normal tracial state $\tau$ , with $\|x\|_2=\tau(x^*x)^{1/2}$ . $M$ has separable predual if $M$ is isometrically the dual of a separable Banach space; this does not require $H$ or $M$ to be norm-separable.

An inclusion of factors $P\subseteq M$ is irreducible if $P'\cap M=\mathbb C1$ . $\mathcal U(M)$ denotes the unitary group.

Formalization targets

Milestone: Theorem 1.1 (relative generation)

For an irreducible inclusion $P\subset M$ of II $_1$ factors with $M$ of separable predual,

\{u\in\mathcal U(M):\ W^*(P,u)=M\}\ \text{ is a dense }G_\delta\text{ in }(\mathcal U(M),\|\cdot\|_2).

Goal: Theorem 1.2 (single generation)

M\ \text{a II}_1\text{ factor with separable predual}\ \Longrightarrow\ \exists\,x\in M:\quad W^*(x)=M.

The Lean statement OAI.Generator.single_generation_of_II1_separable_predual is open on the platform.

Significance

Combined with Willig's reduction and the known type I and properly infinite cases, Theorem 1.2 gives single generation of every von Neumann algebra with separable predual, an affirmative answer to the generator problem. The paper also deduces that the generator invariants $G$ and $G_{\mathrm{sa}}$ of Dykema–Sinclair–Smith–White vanish for every such factor, and that Voiculescu's free entropy dimensions $\delta,\delta_0$ are not invariants of the generated algebra (Corollary 6.1), since $L(\mathbb F_n)$ has both a free semicircular $n$ -tuple and a self-adjoint pair as generators. Theorem 1.1 is of independent interest: it shows that relative generators are generic, not merely existent.

These results are stated in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proofs exist.

Difficulty

Earlier positive results all relied on extra structure (Cartan subalgebras, property $\Gamma$ , tensor decompositions, sequential commutation) to build a generator. Without such structure one must show that a unitary $u$ generates $M$ over $P$ , which requires detecting every vector of $L^2(M)$ through words in $P$ and $u$ . Perturbing $u$ along a long word changes it many times, and operator-norm bounds on the accumulated perturbation grow with the word length; a length-uniform estimate is needed. The Baire-category step also needs the projection onto $L^2(W^*(P,u))$ to vary semicontinuously in $u$ .

Formalization scope

Algebras are concrete StarSubalgebra ℂ (H →L[ℂ] H); WOTClosed uses Mathlib's weak operator topology, and wstar s is the infimum of WOT-closed star-subalgebras containing $s$ (unital by construction).
IsII1Factor = nonzero Hilbert space, WOT-closed, trivial centre, finite (isometries are unitary), diffuse. No trace is assumed.
HasSeparablePredual asks for a separable Banach space $X$ in the same universe with a conjugate-linear isometric equivalence between its dual and the algebra; this is equivalent to the usual condition.
For Theorem 1.1, the trace is part of the conclusion (IsNormalizedTrace: normalized, positive, faithful, tracial, ultraweakly continuous), the topology on unitary large is generated by trace 2-distance balls, and the locus is $\{u: \mathrm{wstar}(P\cup\{u\})=M\}$ .

A complete development needs the standard theory of II $_1$ factors (trace, $L^2(M)$ , conditional expectations, ultrapowers), Popa's free independence in ultraproducts and irreducible hyperfinite subfactors, Haagerup's inequality for free groups, and the Baire category theorem on the unitary group. This infrastructure is reusable across operator-algebra missions. Contributions formalizing Proposition 3.2 (perturbation bounds) and Popa's irreducible hyperfinite embedding (Theorem 5.1) are welcome.

Selected references

OpenAI, Relative generation and the generator problem for finite factors, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf
P. Willig, Generators and direct integral decompositions of $W^*$ -algebras, Tohoku Math. J., 1974. https://doi.org/10.2748/tmj/1178241231
D. Sherman, On cardinal invariants and generators for von Neumann algebras, Canad. J. Math., 2012. https://arxiv.org/abs/0908.4565
K. Dykema, A. Sinclair, R. Smith, S. White, Generators of II $_1$ factors, Oper. Matrices, 2008. https://arxiv.org/abs/0706.1953
L. Ge, S. Popa, On some decomposition properties for factors of type II $_1$ , Duke Math. J., 1998. https://doi.org/10.1215/S0012-7094-98-09405-4
J. Shen, Type II $_1$ factors with a single generator, J. Operator Theory, 2009. https://arxiv.org/abs/math/0511327
S. Popa, Independence properties in subalgebras of ultraproduct II $_1$ factors, J. Funct. Anal., 2014. https://arxiv.org/abs/1308.3982
U. Haagerup, An example of a non nuclear $C^*$ -algebra, which has the metric approximation property, Invent. Math., 1979. https://doi.org/10.1007/BF01410082
D. Gao, S. Kunnawalkam Elayavalli, G. Patchell, H. Tan, Internal sequential commutation and single generation, IMRN, 2025. https://arxiv.org/abs/2404.12380

22 thms2 active usersReviewed

Dynamical Systems Functional Analysis·Captain: wurtle

Invariant-projection counterexamples for every irrational rotationResearch Paper

Motivation

The invariant subspace problem asks whether every bounded operator on a separable infinite-dimensional complex Hilbert space has a nontrivial closed invariant subspace. Inside a finite von Neumann algebra there is a sharper, algebra-relative version: given $T$ in a type $\mathrm{II}_1$ factor $M$ , is there a projection $p\in M$ with $0<\tau(p)<1$ and $(1-p)Tp=0$ , i.e. a nontrivial $T$ -invariant subspace whose projection lies in $M$ ? The Brown measure, built from the Fuglede–Kadison determinant, gives such projections whenever it is not a point mass (Haagerup–Schultz). The open territory is therefore operators whose Brown measure is a point mass, in particular quasinilpotent ones.

Zhu, Fang and Shi (2017) studied the weighted irrational rotations $T_f=Uf(V)$ in the hyperfinite $\mathrm{II}_1$ factor and asked whether $T_f$ must have a nontrivial invariant projection when $f$ is nonzero almost everywhere, $|f|$ is nonconstant and the determinant of $f(V)$ is zero. This mission formalizes a negative answer for every prescribed irrational angle.

Timeline

1952. Fuglede and Kadison introduce the determinant on finite factors (doi:10.2307/1969645).
1986. Brown defines the spectral distribution (Brown measure) of an operator in a $\mathrm{II}_1$ factor.
2004. Dykema and Haagerup construct nontrivial hyperinvariant subspaces for the quasinilpotent DT-operator, whose Brown measure is a point mass (doi:10.1016/S0022-1236(03)00167-8).
2008. Tucci constructs quasinilpotent generators of the hyperfinite factor that do have nontrivial invariant projections (doi:10.1016/j.jfa.2008.03.012).
2009. Haagerup and Schultz attach a hyperinvariant projection to each Borel set, with trace equal to its Brown mass (doi:10.1007/s10240-009-0018-7). Dykema and Schultz identify the Brown measure of weighted rotations as uniform measure on a circle of radius the determinant (arXiv:math/0512197).
2017. Zhu, Fang and Shi give a direct proof of that Brown-measure formula, exhibit continuous weights with one zero and determinant zero, and pose the question above (doi:10.7146/math.scand.a-25625).

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

Fix an irrational $\theta\in(0,1)$ . Let $R_\theta$ be the von Neumann algebra generated by unitaries $U,V$ with $VU=e^{2\pi i\theta}UV$ and trace $\tau(U^mV^n)=0$ for $(m,n)\ne(0,0)$ , $\tau(1)=1$ ; it is the hyperfinite $\mathrm{II}_1$ factor. Concretely, on $\mathcal H=L^2(\mathbb R/\mathbb Z;\ell^2(\mathbb Z))$ , $U$ shifts the $\ell^2(\mathbb Z)$ coordinate and $V$ multiplies the $k$ -th coordinate at $x$ by $e^{2\pi i(x+k\theta)}$ . For a continuous $f:\mathbb T\to[0,1]$ set $T_f=Uf(V)$ . A projection $p\in R_\theta$ is invariant for $T_f$ if $(1-p)T_fp=0$ ; it is nontrivial if $p\ne0,1$ . The Fuglede–Kadison determinant of $f(V)$ is $\exp\int_{\mathbb T}\log f\,dm$ , with $m$ the normalized Haar measure.

Formalization targets

Goal: Theorem 1.1 (with Corollary 6.2)

For every irrational $\theta\in(0,1)$ there is a continuous $f:\mathbb T\to[0,1]$ with

f^{-1}(0)=\{1\},\qquad \int_{\mathbb T}\log f\,dm=-\infty,

such that every projection $p\in R_\theta$ with $(1-p)\,Uf(V)\,p=0$ equals $0$ or $1$ ; moreover $T_f\ne0$ , $\|T_f^n\|^{1/n}\to0$ , and $\Delta(T_f)=0$ .

Milestones

Theorem 1.1 at some angle. The same conclusion for one irrational angle, in the abstract tracial model on $\ell^2(\mathbb Z^2)$ .
Theorem A.1 (product realization). A second model on $\mathbb T^{\mathbb N}$ : angles $\theta_i$ with $\sum\theta_i<\infty$ , rationally independent with $1$ , and $f(x)=\exp(-\sum c_i\lfloor x_i+\theta_i\rfloor)$ , giving a nonzero quasinilpotent $T=U\pi(f)$ in a $\mathrm{II}_1$ factor with only trivial invariant projections and the stated polar structure.
Abstract consequence. Some $\mathrm{II}_1$ factor with separable predual contains a nonzero quasinilpotent operator with no nontrivial invariant projection.

The goal OAI.Invariant233.Results.prescribed_irrational_counterexample is open on the platform.

Significance

Theorem 1.1 answers the Zhu–Fang–Shi question negatively, with the angle fixed in advance and no Diophantine condition. Combined with Dykema's observation that hyperinvariant subspaces of $T\in M$ have projections in $M$ , it yields (Corollary 1.4) a nonzero quasinilpotent operator on every separable infinite-dimensional Hilbert space with no nontrivial hyperinvariant subspace, so its commutant is a proper, strongly closed, transitive unital algebra. It also shows that, at determinant zero, the Haagerup–Schultz method cannot be supplemented by any invariant projection in the factor for these operators. The conclusion concerns projections in $R_\theta$ ; ordinary invariant subspaces of the Hilbert-space representation are not excluded.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Brown-measure methods give nothing here: at determinant zero the Brown measure is $\delta_0$ , so Haagerup–Schultz projections are trivial, and point-mass Brown measure does not by itself exclude invariant projections (Dykema–Haagerup, Tucci). One must show directly that a hypothetical invariant projection, viewed as a measurable field of projections, contradicts weighted orthogonality identities along rotation orbits. The weight's logarithmic drops must be rare enough to keep a finite window under control yet strong enough to suppress the infinite tail, and this must work at an arbitrary prescribed angle, which forces large divisible frequencies. Passing from a measurable weight to a continuous one with a single zero requires an intertwining multiplier that may be unbounded.

Formalization scope

The circle is AddCircle (1:ℝ) with Haar probability; the zero of $f$ is at $0\in\mathbb R/\mathbb Z$ , which corresponds to $1\in\mathbb T$ .
The Hilbert space is Lp (lp (fun _ : ℤ => ℂ) 2) 2 circleMeasure; Rotation.U is the fibrewise shift and Rotation.V θ multiplies by $e^{2\pi i(x+k\theta)}$ ; Rotation.algebra θ is the double commutant of $\{U,V\}$ .
HasOnlyTrivialInvariantProjections M T quantifies over self-adjoint idempotents $p\in M$ with $(1-p)Tp=0$ ; no commutation with $T$ is required.
NormQuasinilpotent T is $\|T^n\|^{1/n}\to0$ ; the determinant is the vector-state Fuglede–Kadison determinant $\inf_{\varepsilon>0}\exp\frac12\tau\log(T^*T+\varepsilon)$ , avoiding $\log0$ .

A complete development needs crossed-product (group-measure-space) von Neumann algebras, measurable fields of projections, the Fuglede–Kadison determinant, and uniform averaging under irrational rotation. Contributions formalizing Theorem 5.2 (the measurable-weight obstruction), Lemma 5.1 (conditional convolution obstruction), Corollary 6.2 (quasinilpotence) and Lemma A.4 (the product algebra is a $\mathrm{II}_1$ factor) are welcome.

Selected references

OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
Z. Zhu, J. Fang, R. Shi, On a class of operators in the hyperfinite II $_1$ factor, Math. Scand., 2017. https://doi.org/10.7146/math.scand.a-25625
B. Fuglede, R. V. Kadison, Determinant theory in finite factors, Ann. of Math., 1952. https://doi.org/10.2307/1969645
U. Haagerup, H. Schultz, Invariant subspaces for operators in a general II $_1$ -factor, Publ. Math. IHÉS, 2009. https://doi.org/10.1007/s10240-009-0018-7
K. Dykema, H. Schultz, Brown measure and iterates of the Aluthge transform for some operators arising from measurable actions, Trans. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0002-9947-09-04762-X
K. Dykema, U. Haagerup, Invariant subspaces of the quasinilpotent DT-operator, J. Funct. Anal., 2004. https://doi.org/10.1016/S0022-1236(03)00167-8
G. H. Tucci, Some quasinilpotent generators of the hyperfinite II $_1$ factor, J. Funct. Anal., 2008. https://doi.org/10.1016/j.jfa.2008.03.012
K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8

28 thms2 active usersReviewed

Completed

Functional Analysis·Captain: wurtle

Tracial projection methods and uniform property GammaResearch Paper

Motivation

The classification programme for simple nuclear $C^*$ -algebras identifies a class of algebras that are determined by K-theory and traces. Membership in that class is governed by regularity properties: finite nuclear dimension, absorption of the Jiang–Su algebra $\mathcal Z$ , and strict comparison. Uniform property $\Gamma$ , introduced by Castillejos, Evington, Tikuisis, White and Winter, is a central divisibility condition: it asks for projections in a central sequence algebra that cut every trace exactly in half, uniformly across the whole trace space, while preserving trace values against fixed coefficients. Together with strict comparison it is equivalent to $\mathcal Z$ -stability for simple separable unital nuclear algebras (Castillejos–Evington–Tikuisis–White). Schafhauser, Tikuisis and White asked (Problem XXI of their problem list) whether real rank zero of the uniform tracial ultrapower of the tracial completion already forces uniform property $\Gamma$ .

Timeline

1943, 1969, 1970. Murray and von Neumann introduce property $\Gamma$ for II $_1$ factors (doi:10.2307/1969107); Dixmier gives its central-projection formulation (doi:10.1007/BF01404306); McDuff studies central sequences and absorption of the hyperfinite factor (doi:10.1112/plms/s3-21.3.443).
1976. Connes classifies injective factors (doi:10.2307/1971057).
1991. Brown and Pedersen introduce real rank zero (doi:10.1016/0022-1236(91)90056-B).
1999. Jiang and Su construct the algebra $\mathcal Z$ (doi:10.1353/ajm.1999.0012).
2010–2012. Winter and Zacharias define nuclear dimension and the Toms–Winter conjecture is formulated (doi:10.1016/j.aim.2009.12.005); Winter proves finite nuclear dimension implies $\mathcal Z$ -stability (doi:10.1007/s00222-011-0334-7); Matui and Sato prove strict comparison implies $\mathcal Z$ -stability with finitely many extremal traces (doi:10.1007/s11511-012-0084-4).
2013. Ozawa introduces uniform tracial completions (J. Math. Sci. Univ. Tokyo).
2021–2022. Castillejos, Evington, Tikuisis, White and Winter introduce uniform property $\Gamma$ and prove $\mathcal Z$ -stability implies finite nuclear dimension (doi:10.1007/s00222-020-01013-1); CETW develop it systematically (doi:10.1093/imrn/rnaa282).
2023. Carrión et al. develop tracially complete $C^*$ -algebras (arXiv:2310.20594).
2025–2026. Schafhauser, Tikuisis and White list Problem XXI (arXiv:2506.10902); Vaccaro, Kessinger–Toms and Fu obtain related implications (arXiv:2604.24682, arXiv:2607.23817, arXiv:2605.21655); Toms constructs a simple separable unital AH algebra without uniform property $\Gamma$ (arXiv:2606.12188).

The source of this mission is an OpenAI preprint dated September 23, 2026, which answers Problem XXI affirmatively (and, by separate arguments, also treats the unital Toms–Winter conjecture).

Setting

Let $A$ be a unital $C^*$ -algebra with nonempty set $T(A)$ of tracial states. The uniform 2-seminorm is

\|a\|_{2,T(A)}=\sup_{\tau\in T(A)}\tau(a^*a)^{1/2}.

The uniform tracial completion $B=\overline A^{T(A)}$ consists of bounded sequences in $A$ that are Cauchy for $\|\cdot\|_{2,T(A)}$ , modulo those tending to zero; each $\tau\in T(A)$ extends to a designated trace $\bar\tau$ on $B$ . For a free ultrafilter $\omega$ on $\mathbb N$ , the uniform tracial ultrapower $B^\omega$ is the algebra of bounded sequences in $B$ modulo those whose uniform 2-norm tends to zero along $\omega$ . Its limit traces are

\lambda([(b_j)])=\lim_{j\to\omega}\bar\tau_j(b_j),\qquad \tau_j\in T(A),

and $\Lambda_\omega$ denotes the set of these. $B$ embeds in $B^\omega$ as constant sequences.

A unital $C^*$ -algebra has real rank zero if every self-adjoint element is a norm limit of self-adjoint elements with finite spectrum. $A$ is stably finite if every isometry in every matrix algebra over $A$ is unitary, and nuclear if its algebraic tensor product with any $C^*$ -algebra carries a unique $C^*$ -norm.

Formalization targets

Goal: Theorem 1.1

Let $A$ be unital, separable, simple, infinite-dimensional, nuclear and stably finite with $T(A)\neq\varnothing$ , and let $\omega$ be a free ultrafilter. If $B^\omega$ has real rank zero, then there is a projection $p\in B^\omega\cap B'$ with

\lambda(px)=\tfrac12\,\lambda(x)\qquad(x\in B,\ \lambda\in\Lambda_\omega).

This is the halving formulation of uniform property $\Gamma$ used in Problem XXI. The Lean statement OAI.ComparatorModel.CurrentMain.main is open on the platform.

Significance

The theorem shows that real rank zero at the level of the tracial ultrapower is enough to produce uniform property $\Gamma$ , with no restriction on the trace space; the paper also deduces that every trace on $B$ is a designated extension (Corollary 1.2). Since uniform property $\Gamma$ plus strict comparison gives $\mathcal Z$ -stability, this links projection structure in tracial ultrapowers to the Toms–Winter regularity theory. The equivalence between the halving formulation and the usual all- $m$ formulation is due to Carrión et al.

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

Difficulty

Real rank zero supplies many projections in $B^\omega$ , but nothing makes them central, and halving must hold simultaneously for every limit trace and every coefficient $x\in B$ . Divisibility results derived from real rank zero (Vaccaro) give tracially large order-zero maps without centrality; uniform property $\Gamma$ needs commutation with all of $B$ and exact coefficient identities. Equality of the scalar traces $\lambda(p)$ alone is not enough. Nuclearity by itself does not suffice either, as Toms' AH example shows, so the real rank zero hypothesis must be used in an essential way.

Formalization scope

TracialState A is a positive linear functional with $\tau(1)=1$ and $\tau(ab)=\tau(ba)$ ; the order on $A$ is the $C^*$ order (StarOrderedRing).
The uniform tracial completion is the quotient of the star-subalgebra of uniformly 2-Cauchy elements of $\ell^\infty(\mathbb N,A)$ by uniformly 2-null sequences; the ultrapower is the quotient of $\ell^\infty(\mathbb N,B)$ by sequences 2-null along U, computed with the designated traces $\bar\tau$ .
TopologicallySimple, StablyFinite (via CStarMatrix), IsNuclear (subsingleton of $C^*$ -norms on algebraic tensor products, in a fixed universe) and RealRankZero (finite-spectrum self-adjoint approximation) are defined directly.
UniformPropertyGammaAt A U asserts a star projection $p$ commuting with the image of $B$ and halving familyLimitTrace … s for every sequence of traces s : ℕ → TracialState A.
MainClaim existentially packages five auxiliary Prop classes (quotient $C^*$ -norm, closure properties of null and Cauchy sequences, existence of ultralimits, and vanishing of limit traces on null sequences). They are true general facts that a proof must establish; they are not assumptions.

A complete development needs ultrapowers and tracial completions of $C^*$ -algebras, nuclearity and completely positive approximation, and real rank zero; all of this is reusable for the other regularity missions of this family. Contributions formalizing Theorem 1.3 (finite-set central splitting) and Corollary 1.2 are welcome.

Selected references

OpenAI, Tracial projection methods and uniform property $\Gamma$ , preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Tracial-projection-methods-and-uniform-property-Gamma-September-23-2026/paper.pdf
J. Castillejos, S. Evington, A. Tikuisis, S. White, Uniform property $\Gamma$ , Int. Math. Res. Not., 2022. https://doi.org/10.1093/imrn/rnaa282
J. Castillejos, S. Evington, A. Tikuisis, S. White, W. Winter, Nuclear dimension of simple $C^*$ -algebras, Invent. Math., 2021. https://doi.org/10.1007/s00222-020-01013-1
C. Schafhauser, A. Tikuisis, S. White, Nuclear $C^*$ -algebras: 99 problems, 2026. https://arxiv.org/abs/2506.10902
J. R. Carrión et al., Tracially Complete $C^*$ -Algebras, 2023. https://arxiv.org/abs/2310.20594
L. G. Brown, G. K. Pedersen, $C^*$ -algebras of real rank zero, J. Funct. Anal., 1991. https://doi.org/10.1016/0022-1236(91)90056-B
W. Winter, J. Zacharias, The nuclear dimension of $C^*$ -algebras, Adv. Math., 2010. https://doi.org/10.1016/j.aim.2009.12.005
H. Matui, Y. Sato, Strict comparison and $\mathcal Z$ -absorption of nuclear $C^*$ -algebras, Acta Math., 2012. https://doi.org/10.1007/s11511-012-0084-4
A. Vaccaro, Stable rank one, tracial local homogeneity and uniform property $\Gamma$ , 2026. https://arxiv.org/abs/2604.24682

4 thms2 active usersReviewed

Completed

Information Theory Quantum Information·Captain: wurtle

Classical capacity and entropy inequalities for generalized amplitude dampingResearch Paper

Motivation: the classical capacity of a thermal qubit channel

A quantum channel models how a physical system, used to carry information, is corrupted by its environment. The classical capacity of a channel is the largest rate, in bits per use, at which classical messages can be sent with vanishing error when the sender may encode into arbitrary — possibly entangled — states of many uses and the receiver may measure all outputs jointly. The Holevo–Schumacher–Westmoreland coding theorem (Holevo 1998; Schumacher–Westmoreland 1997) expresses this capacity as a regularized limit of the Holevo information over ever larger blocks of uses. Since Holevo information is not additive in general (Hastings 2009), computing the capacity of any specific channel requires a channel-specific additivity argument, and exact formulas are known only for a few families.

Generalized amplitude damping is the standard model of a qubit relaxing toward a thermal state: it loses or gains an excitation with probabilities set by a damping strength $\gamma$ and a stationary excited population $\nu$ , and its coherences decay. It is one of the basic noise models of quantum information theory.

Background timeline

1996–1998 — Coding theorems for pure and mixed signals establish the regularized capacity formula (Hausladen et al. 1996; Schumacher–Westmoreland 1997; Holevo 1998).
2002 — Additivity for unital qubit channels (King 2002) and for entanglement-breaking channels (Shor 2002) settles some parameter regions of the family; Bennett, Shor, Smolin and Thapliyal describe the two-signal optimization for ordinary amplitude damping (BSST 2002).
2005 — Giovannetti and Fazio derive the optimized one-use expression for ordinary amplitude damping (Giovannetti–Fazio 2005); Berry studies qubit channels achieving capacity with two states (Berry 2005).
2007 — Hou and Fang characterize the one-use Holevo optimum of the generalized channel (Hou–Fang 2007).
2009 — Hastings shows that Holevo information is not additive in general (Hastings 2009).
2018 — Leditzky, Kaur, Datta and Wilde note that the unrestricted classical capacity of amplitude damping had not been determined (LKDW 2018).
2020 — Khatri, Sharma and Wilde collect upper bounds for the generalized family (KSW 2020).
2026 — Tang, Zhu, Bai and Wang prove additivity for qubit channels with a pure output, including ordinary amplitude damping (arXiv:2609.28592); Fang gives a close converse bound for the generalized family (arXiv:2609.14621).
2026 — An OpenAI preprint, Classical capacity and entropy inequalities for generalized amplitude damping (OpenAI Math Release, September 24, 2026), claims the capacity for all $(\gamma,\nu)\in[0,1]^2$ . The preprint has not been peer reviewed, and its results are not formally verified.

Setting

For $\gamma,\nu\in[0,1]$ the generalized amplitude-damping channel acts on a qubit density matrix by

\mathcal A_{\gamma,\nu}\begin{pmatrix}1-q&z\\\bar z&q\end{pmatrix}=\begin{pmatrix}1-t&\sqrt{1-\gamma}\,z\\\sqrt{1-\gamma}\,\bar z&t\end{pmatrix},\qquad t=(1-\gamma)q+\gamma\nu,

and $n$ independent uses act as $\mathcal A_{\gamma,\nu}^{\otimes n}$ on $2^n\times2^n$ matrices. With $S(P)=-\operatorname{Tr}P\ln P$ , the Holevo information in bits is

\chi(\mathcal N)=\frac1{\ln2}\sup_{\{q_a,\rho_a\}}\Bigl\{S\Bigl(\sum_aq_a\mathcal N(\rho_a)\Bigr)-\sum_aq_aS(\mathcal N(\rho_a))\Bigr\},

over all finite ensembles of input states (entangled across uses when $\mathcal N=\mathcal A^{\otimes n}$ ). The classical capacity $C(\mathcal N)$ is the supremum of rates $R$ for which there are $n$ -use codes — arbitrary input states for each of $M_n$ equiprobable messages and one joint measurement of all outputs — with average error tending to zero and $\liminf_n n^{-1}\log_2M_n\ge R$ ; there is no shared entanglement or feedback. Write $h$ for binary entropy in nats, $g(u)=h\bigl((1+\sqrt{1-4u})/2\bigr)$ and $v_{\gamma,\nu}(p)=\gamma\nu(1-\nu)+\gamma(1-\gamma)(p-\nu)^2$ .

Formalization targets

Goal: additivity and capacity formula (Theorem 1.1)

For all $\gamma,\nu\in[0,1]$ and every $n\ge1$ ,

\chi(\mathcal A_{\gamma,\nu}^{\otimes n})=n\,\chi(\mathcal A_{\gamma,\nu})=\frac n{\ln 2}\max_{0\le p\le1}\bigl\{h((1-\gamma)p+\gamma\nu)-g(v_{\gamma,\nu}(p))\bigr\},

the maximum is attained, $C(\mathcal A_{\gamma,\nu})=\chi(\mathcal A_{\gamma,\nu})$ , and for every maximizer $p$ the equiprobable independent products of the two signals $\phi_\pm=\sqrt{1-p}\,|0\rangle\pm\sqrt p\,|1\rangle$ attain $\chi(\mathcal A_{\gamma,\nu}^{\otimes n})$ at every block length. The goal is published on the platform with status Open.

Significance

The result itself. The theorem gives a closed one-variable formula for the classical capacity of every generalized amplitude-damping channel, removing the regularization over block lengths: entangled input signals across uses give no advantage, and a simple product code with two signals per use is optimal. This settles the ordinary amplitude-damping case listed as open by LKDW 2018 and extends beyond the pure-output criterion of Tang et al. to the thermal regime, where the channel has no pure output. The source further proves additivity of Holevo capacity, minimum output entropy and classical capacity when the channel is used in parallel with any finite-dimensional partner channel (Corollary 1.2); that corollary is not part of this goal.

Formalizing it. The goal ties together an operational capacity (codes and error probabilities), an entropic quantity (a supremum over unrestricted ensembles on $2^n$ -dimensional matrices), and a scalar optimization. A machine-checked proof would certify both the matrix entropy inequality at the heart of the argument and the converse direction of the coding theorem. Mathlib does not currently contain quantum channel capacity theory, so the definitions here are new infrastructure.

Difficulty

Optimizing a single use gives a lower bound on capacity; the difficulty is the matching upper bound for all $n$ simultaneously, where an input may be entangled across all uses. Holevo additivity is false for general channels, so no abstract argument applies, and for interior thermal occupation $0<\nu<1$ with $\gamma>0$ the channel has no pure output, which rules out the recent pure-output criterion. The proof needs a lower bound on the entropy of the output of an arbitrary entangled block input, i.e. a matrix entropy inequality for $2\times2$ block-structured states that is tight on product inputs. Identifying the capacity with the regularized Holevo quantity also requires the full coding theorem and a Fano-type converse.

Formalization scope

Matrices are indexed by Fin n → Fin 2; the $n$ -use channel is given by tensor products of the four standard Kraus operators of generalized amplitude damping, which reproduce the displayed action exactly.
Entropy is Tr (cfc negMulLog P) (nats, $0\ln0=0$ ); Holevo values are divided by $\ln 2$ (bits). holevo γ ν n is the sSup over all finite ensembles of arbitrary $2^n$ -dimensional states, with no product or purity restriction.
capacity is the sSup of operationally achievable rates: codes with any positive number of messages, arbitrary state encodings, an arbitrary POVM decoder, average error tending to $0$ , and the liminf rate condition. It is defined operationally, not by regularization, so the identity $C=\chi$ includes the coding theorem.
The scalar objective uses Real.binEntropy (nats); the maximizer is over $p\in[0,1]$ . The final clause also asserts that the phase-product signals are states.
Parameters range over the closed square $[0,1]^2$ , including boundary cases (identity channel at $\gamma=0$ , full replacement at $\gamma=1$ ).
Needed infrastructure: matrix entropy and its concavity, CPTP maps and Kraus representations, Holevo's bound, Fano's inequality, the HSW coding theorem for finite ensembles, and Fekete-type superadditivity. These are reusable for any quantum Shannon-theory mission.

Selected references

P. Hausladen, R. Jozsa, B. Schumacher, M. Westmoreland, W. K. Wootters, Classical information capacity of a quantum channel, Phys. Rev. A 54 (1996), 1869–1876. https://doi.org/10.1103/PhysRevA.54.1869
B. Schumacher and M. D. Westmoreland, Sending classical information via noisy quantum channels, Phys. Rev. A 56 (1997), 131–138. https://doi.org/10.1103/PhysRevA.56.131
A. S. Holevo, The capacity of the quantum channel with general signal states, IEEE Trans. Inf. Theory 44 (1998), 269–273. https://doi.org/10.1109/18.651037
C. King, Additivity for unital qubit channels, J. Math. Phys. 43 (2002), 4641–4653. https://doi.org/10.1063/1.1500791
P. W. Shor, Additivity of the classical capacity of entanglement-breaking quantum channels, J. Math. Phys. 43 (2002), 4334–4340. https://doi.org/10.1063/1.1498000
C. H. Bennett, P. W. Shor, J. A. Smolin, A. V. Thapliyal, Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem, IEEE Trans. Inf. Theory 48 (2002), 2637–2655. https://doi.org/10.1109/TIT.2002.802612
V. Giovannetti and R. Fazio, Information-capacity description of spin-chain correlations, Phys. Rev. A 71 (2005), 032314. https://doi.org/10.1103/PhysRevA.71.032314
D. W. Berry, Qubit channels that achieve capacity with two states, Phys. Rev. A 71 (2005), 032334. https://doi.org/10.1103/PhysRevA.71.032334
L.-Z. Hou and M.-F. Fang, The Holevo capacity of a generalized amplitude-damping channel, Chinese Physics 16 (2007), 1843–1847. https://doi.org/10.1088/1009-1963/16/7/006
M. B. Hastings, Superadditivity of communication capacity using entangled inputs, Nature Physics 5 (2009), 255–257. https://doi.org/10.1038/nphys1224
F. Leditzky, E. Kaur, N. Datta, M. M. Wilde, Approaches for approximate additivity of the Holevo information of quantum channels, Phys. Rev. A 97 (2018), 012332. https://doi.org/10.1103/PhysRevA.97.012332
S. Khatri, K. Sharma, M. M. Wilde, Information-theoretic aspects of the generalized amplitude-damping channel, Phys. Rev. A 102 (2020), 012401. https://doi.org/10.1103/PhysRevA.102.012401
Z. Tang, C. Zhu, G. Bai, X. Wang, Classical capacity and entanglement cost of the amplitude damping channel, arXiv:2609.28592 (2026). https://arxiv.org/abs/2609.28592v1
K. Fang, A pretty-tight converse on the classical capacity of generalized amplitude-damping channels, arXiv:2609.14621 (2026). https://arxiv.org/abs/2609.14621v1
OpenAI, Classical capacity and entropy inequalities for generalized amplitude damping, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf

37 thms2 active usersReviewed

Completed

Complexity Theory Quantum Information Theoretical Computer Science·Captain: wurtle

Product-projection localization and the QAC0 parity lower boundResearch Paper

Motivation

Parity, $\mathrm{PARITY}_n(x)=x_1\oplus\cdots\oplus x_n$ , is the standard test of whether a shallow circuit can aggregate information from all of its inputs. Classically, constant-depth circuits with unbounded fan-in AND/OR gates ( $\mathsf{AC}^0$ ) cannot compute it: Furst, Saxe and Sipser (Math. Systems Theory 1984) and Ajtai (APAL 1983) proved superpolynomial lower bounds, and Håstad's switching lemma gave nearly optimal exponential ones (STOC 1986). The quantum analogue $\mathsf{QAC}^0$ allows arbitrary one-qubit unitaries and Toffoli gates of unbounded arity, but gates in one layer must act on disjoint qubits, so a wire cannot control many simultaneous gates. Moore (arXiv:quant-ph/9903046, 1999) showed that coherent parity and quantum fanout are equivalent under Hadamard conjugation, and conjectured that neither is in $\mathsf{QAC}^0$ . Because fanout makes constant-depth quantum circuits very powerful (Høyer–Špalek, ToC 2005), whether $\mathrm{PARITY}\notin\mathsf{QAC}^0$ has been a central question about shallow quantum computation.

Background

1999 — Moore introduces the quantum circuit classes and the parity/fanout conjecture.
2002 — Green, Homer, Moore and Pollett develop quantum counting classes and modular-gate equivalences (QIC 2002).
2006 — Fang, Fenner, Green, Homer and Zhang: depth $\Omega(\log(n/(a+1)))$ for exact clean parity with $a$ ancillas (QIC 2006).
2020–2021 — Padé, Fenner, Grier and Thierauf rule out exact clean parity at entangling depth two (arXiv:2005.12169); Rosenthal bounds approximate parity unitaries (ITCS 2021).
2024–2025 — Pauli-spectrum lower bounds with restricted ancillas (Nadimpalli, Parham, Vasconcelos, Yuen, STOC 2024); no fixed parity advantage with barely superlinear ancillas (Anshu, Dong, Ou, Yao, STOC 2025), extended by Dong, Ou and Yao (arXiv:2510.00593).
2026 — Joshi, Tal, Vasconcelos and Wright: exact parity lower bounds at entangling depth three without size restriction (STOC 2026); Gretta, Gupta and Joshi relate the question to Fourier concentration (arXiv:2604.02793).
September 2026 — Two OpenAI preprints claim the lower bound for every fixed depth and every polynomial number of qubits, by independent arguments: product-projection localization (source) and regular trajectories with pruning (source).

This mission asks for a formal proof of the parity lower bound stated as Theorem 1 of 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.

Setting

A circuit acts on $N$ qubits, with state space $(\mathbb C^2)^{\otimes N}$ and computational basis indexed by bit strings $y\in\{0,1\}^N$ . The allowed gates are arbitrary one-qubit unitaries and generalized Toffoli gates $|z_1,\dots,z_t,b\rangle\mapsto|z_1,\dots,z_t,b\oplus z_1\cdots z_t\rangle$ on distinct control and target qubits. A layer is a set of gates with pairwise disjoint supports, and a depth- $d$ circuit is a product $W=L_d\cdots L_1$ of at most $d$ layers. Gates and their complex entries may depend on $n$ but not on the input.

On input $x\in\{0,1\}^n$ with $n\le N$ , the circuit starts in $|x\rangle\otimes|0\rangle^{\otimes(N-n)}$ . One designated output qubit is measured in the computational basis; all other qubits are discarded in arbitrary states, and the input need not be preserved. The success probability on $x$ is

\Pr[\text{output}=\mathrm{PARITY}_n(x)]=\sum_{y:\ y_{\mathrm{out}}=\mathrm{PARITY}_n(x)}\bigl|\langle y|W|x,0\rangle\bigr|^2 .

A circuit computes parity with worst-case advantage $\varepsilon$ if this probability is at least $1/2+\varepsilon$ for every $x$ .

Formalization targets

Goal: the parity lower bound (Theorem 1, p. 1)

Fix an integer $d\ge0$ , a real $c\ge1$ and $0<\varepsilon\le1/2$ . Then for all sufficiently large $n$ , for every $N$ with $n\le N\le n^c$ , every circuit of depth at most $d$ on $N$ qubits and every choice of output qubit, there is an input $x\in\{0,1\}^n$ with

\Pr[\text{output}=\mathrm{PARITY}_n(x)]<\tfrac12+\varepsilon .

With $\varepsilon=1/6$ this is the usual bounded-error statement $\mathrm{PARITY}\notin\mathsf{QAC}^0$ in the measured-output model.

Significance

The result itself. It answers Moore's question for every fixed depth and every polynomial bound on the total number of qubits, with arbitrary final garbage and any fixed positive advantage, whereas earlier results fixed the entangling depth or restricted the number of ancillas. Through Hadamard conjugation it also excludes constant-depth polynomial-size coherent fanout. The preprint derives further consequences (Section 7): state-preparation obstructions (Corollary 8, p. 14), a qualitative quantum LMN-type Fourier tail bound (Corollary 9, p. 16), and, via reductions of Xu and Li, lower bounds for majority and other symmetric functions (Corollaries 10–11, pp. 17–18). The structural Theorem 2 (p. 5), localization of conjugated product projections, is of independent interest.

Formalizing it. The statement is elementary (finite matrices, Born probabilities) while the proof is a two-level induction with polynomial approximation, so a formal proof would give a fully checked circuit lower bound in quantum complexity, an area with few machine-checked results. A companion OpenAI preprint gives an independent proof by regular trajectories and pruning.

Difficulty

Light-cone arguments fail at once: a single Toffoli gate may touch every qubit, so after one layer an output can depend on all inputs. Spectral and Pauli-weight methods previously needed ancilla bounds such as $\tilde O(n^{1+2^{-d}})$ . The preprint's route controls transitions from a product condition to states with many mismatches, $\bigl\|[M\ge N^t]\,U\,[D=0]\,U^\dagger\,[M=0]\bigr\|\le e^{-N^s}$ for all fixed $0\le s<t$ (Theorem 2, p. 5). The obstacle is that reflection expansions cost exponentially in the projection's support, and low-degree polynomial surrogates for a product projection are accurate only at low mismatch counts; the uncontrolled high-count error is handled by a second induction on thresholds that exchanges the roles of the two counts.

Formalization scope

Word N := Fin N → Fin 2; operators are complex matrices indexed by words. Gate.local q u is a one-qubit unitary tensored with identities; Gate.toffoli controls target is the permutation matrix flipping the target when all controls are $1$ (an empty control set gives a NOT gate, itself a one-qubit unitary).
PhysicalLayer N is a list of gates whose supports are pairwise disjoint; its matrix is the product of the gate matrices. physicalCircuitMatrix layers applies the layers in list order (rightmost matrix acts first).
inputWord x pads $x$ with zeros; successProbability W out x sums $|W_{y,(x,0)}|^2$ over all $y$ whose output bit equals the parity of $x$ , so final garbage is unrestricted.
The output qubit out : Fin N is arbitrary, including an input qubit. The quantifier order is: depth, size bound and advantage fixed first; then a threshold $n_0$ ; then every $n\ge n_0$ , every $N$ in range, every circuit and every output qubit.
No intermediate measurement, postselection or fanout gate is in the model; the statement is a pure statement about unitary matrices, with no complexity-class machinery.
ParityStatement takes the size bound as a real exponent: $N\le n^c$ with $c\ge1$ real, $n\le N$ , and depth layers.length ≤ d with $d\ge0$ , exactly as in Theorem 1. Its conclusion is the negation of "for every $x$ , success $\ge 1/2+\varepsilon$ ".

Welcome contributions: a reusable Lean model of unitary circuits on qubits, spectral projections of commuting count operators, and Chebyshev-type polynomial approximation with coefficient bounds (Lemma 3, p. 6).

Selected references

OpenAI, Product-projection localization and the QAC0 parity lower bound, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Product-projection-localization-and-the-QAC0-parity-lower-bound-September-24-2026/paper.pdf
OpenAI, Regular trajectories, pruning and quantum parity, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Regular-trajectories-pruning-and-quantum-parity-September-24-2026/paper.pdf
C. Moore, Quantum circuits: fanout, parity, and counting, arXiv:quant-ph/9903046 (1999). https://arxiv.org/abs/quant-ph/9903046v3
M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), 13–27. https://doi.org/10.1007/BF01744431
M. Ajtai, $\Sigma^1_1$ -formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), 1–48. https://doi.org/10.1016/0168-0072(83)90038-6
J. Håstad, Almost optimal lower bounds for small depth circuits, STOC 1986. https://doi.org/10.1145/12130.12132
F. Green, S. Homer, C. Moore, C. Pollett, Counting, fanout and the complexity of quantum ACC, QIC 2 (2002). https://doi.org/10.26421/QIC2.1-3
P. Høyer, R. Špalek, Quantum fan-out is powerful, Theory of Computing 1 (2005). https://doi.org/10.4086/toc.2005.v001a005
M. Fang, S. Fenner, F. Green, S. Homer, Y. Zhang, Quantum lower bounds for fanout, QIC 6 (2006). https://doi.org/10.26421/QIC6.1-3
G. Rosenthal, Bounds on the QAC0 complexity of approximating parity, ITCS 2021. https://doi.org/10.4230/LIPIcs.ITCS.2021.32
S. Nadimpalli, N. Parham, F. Vasconcelos, H. Yuen, On the Pauli spectrum of QAC0, STOC 2024. https://doi.org/10.1145/3618260.3649662
M. R. Joshi, A. Tal, F. Vasconcelos, J. Wright, Improved lower bounds for QAC0, STOC 2026. https://doi.org/10.1145/3798129.3800922
L. Gretta, M. Gupta, M. R. Joshi, Parity ∉ QAC0 ⟺ QAC0 is Fourier-concentrated, arXiv:2604.02793 (2026). https://arxiv.org/abs/2604.02793v2

32 thms2 active usersReviewed

Completed

Mathematical Physics Probability·Captain: wurtle

Spontaneous magnetization in the quantum Heisenberg ferromagnetResearch Paper

Motivation

The quantum Heisenberg ferromagnet is the basic quantum model of a magnet: a quantum spin sits at each site of the lattice $\mathbb Z^d$ and neighbouring spins prefer to align. Its Hamiltonian is invariant under simultaneous rotation of all spins, so at zero external field no direction is preferred. Spontaneous magnetization asks whether an infinite-volume equilibrium state at positive temperature can nevertheless choose a direction, giving a nonzero expected spin at a single site. For classical spins and for quantum antiferromagnets this was settled decades ago; for the quantum ferromagnet in $d\ge3$ it has been a standard open problem of mathematical physics, recorded by Lieb in 1999 and again by Seiringer in 2025.

Timeline

1928–1930. Heisenberg proposes the exchange model of ferromagnetism (doi:10.1007/BF01328601); Bloch's spin-wave picture predicts the low-temperature reduction of magnetization (doi:10.1007/BF01339661).
1956. Dyson develops the theory of interacting spin waves and its thermodynamics (doi:10.1103/PhysRev.102.1217, doi:10.1103/PhysRev.102.1230).
1966. Mermin and Wagner exclude positive-temperature ferro- and antiferromagnetism for finite-range isotropic Heisenberg models in $d=1,2$ (doi:10.1103/PhysRevLett.17.1133).
1967. Haag, Hugenholtz and Winnink formulate equilibrium of infinite systems through the KMS condition (doi:10.1007/BF01646342).
1976. Fröhlich, Simon and Spencer prove low-temperature ordering for classical continuous-spin models in $d\ge3$ via infrared bounds (doi:10.1007/BF01608557); Powers relates the Heisenberg model to random walks on the permutation group (doi:10.1007/BF00398374).
1978. Dyson, Lieb and Simon prove ordering for quantum antiferromagnets (spin $\ge1$ in $d\ge3$ , spin $\tfrac12$ in high dimension) and explain why reflection positivity gives no ferromagnetic infrared bound (doi:10.1007/BF01106729).
1988. Kennedy, Lieb and Shastry prove ground-state Néel order for the spin- $\tfrac12$ antiferromagnet on $\mathbb Z^3$ (doi:10.1007/BF01023854).
1991–1994. Conlon–Solovej random-walk representations and free-energy upper bound (doi:10.1007/BF01057876); Tóth's improved pressure bound (1993, doi:10.1007/BF00739568); Nachtergaele's general-spin stochastic-geometric representations (1994, doi:10.1007/978-94-015-8326-8_14).
1999. Lieb poses ferromagnetic long-range order as Problem A of the Mathematical Physics Open Problems list.
2015. Correggi, Giuliani and Seiringer prove the spin-wave free-energy asymptotics in $d=3$ (arXiv:1312.7873).
2020. Björnberg, Fröhlich and Ueltschi analyse the loop representation on the complete graph (arXiv:1811.12834).
2025–2026. Seiringer records the ordering problem in an Oberwolfach report; Klippel proves the free-energy asymptotics in $d=2$ (arXiv:2608.25506).

The source of this mission is an OpenAI preprint dated September 24, 2026, which claims a proof of spontaneous magnetization for every spin and every $d\ge3$ .

Setting

Fix $d\ge3$ and a spin $S\in\{\tfrac12,1,\tfrac32,\dots\}$ ; write $\ell=2S$ . Each site carries $\mathbb C^{2S+1}$ with basis $(e_m)_{m=-S}^{S}$ and

S^ze_m=me_m,\qquad S^+e_m=\sqrt{S(S+1)-m(m+1)}\,e_{m+1},\qquad S^-=(S^+)^*,

$S^x=(S^++S^-)/2$ , $S^y=(S^+-S^-)/(2i)$ . For finite $\Lambda\subset\mathbb Z^d$ the free-boundary Hamiltonian is

H_\Lambda=-\sum_{\{x,y\}\subset\Lambda,\ |x-y|_1=1}\ \bigl(S^x_xS^x_y+S^y_xS^y_y+S^z_xS^z_y\bigr),

each unordered edge counted once. The quasi-local algebra $\mathcal A$ is the norm completion of the local matrix algebras $\bigotimes_{x\in F}M_{2S+1}(\mathbb C)$ . The dynamics is $\tau_t(A)=\lim_n e^{itH_{\Lambda_n}}Ae^{-itH_{\Lambda_n}}$ along the boxes $\Lambda_n=[-n,n]^d$ .

A state is a positive linear functional $\omega$ on $\mathcal A$ with $\omega(1)=1$ . It is $\beta$ -KMS if for all $A,B\in\mathcal A$ there is a bounded function $F$ , continuous on $\{0\le\operatorname{Im}z\le\beta\}$ and analytic inside, with

F(t)=\omega(A\,\tau_t(B)),\qquad F(t+i\beta)=\omega(\tau_t(B)\,A)\qquad(t\in\mathbb R).

It is translation invariant if $\omega\circ T_x=\omega$ for all $x\in\mathbb Z^d$ .

Formalization targets

Goal: Theorem 1.1

\exists\,\beta_0>0\ \ \forall\,\beta\ge\beta_0\ \ \exists\,\omega\ \text{translation invariant, }\beta\text{-KMS for }\tau,\quad \omega(S_0^z)\ \ge\ \frac S4.

The Lean statement OAI.Heisenberg.spontaneous_magnetization also asserts that the box limits defining $\tau_t(A)$ converge for every $t$ and $A$ (the standing fact the theorem relies on). The goal is open on the platform.

Significance

The theorem gives an equilibrium state of the zero-field model, at every sufficiently low positive temperature, that breaks the rotation symmetry: a translation-invariant KMS state with one-site magnetization at least $S/4$ . It addresses the ordering problem in its spontaneous-magnetization formulation; the volume-averaged finite-volume two-point criterion in Seiringer's account is a different formulation that the paper does not use. For $S=\tfrac12$ the Matsubara–Matsuda correspondence turns the ordered state into a hard-core boson state with off-diagonal long-range order, a lattice analogue of Bose–Einstein condensation.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and there is no machine-checked proof. A formal proof would certify a long argument (loop representation, stable-polynomial pin test, Markov-walk return estimates, flow constructions and the KMS limit) whose individual steps are each delicate.

Difficulty

The classical route to continuous-symmetry breaking, infrared bounds from reflection positivity, fails for the quantum ferromagnet: as Dyson, Lieb and Simon explained, it does not yield the needed Duhamel bound. Spin-wave free-energy asymptotics, now known in $d=2,3$ , control correlations only on a temperature-dependent finite length scale, not at all scales at a fixed temperature. Loop representations give positive weights, but positivity alone does not imply ordering: one must show that an interior cycle rarely avoids pins placed on the boundary, uniformly in the volume. Finally, a KMS state must be produced for the zero-field dynamics itself, so the symmetry-breaking field used in finite volume has to be removed while both KMS boundary conditions survive.

Formalization scope

Sites are Fin d → ℤ; a spin level is Fin (ℓ+1) with magnetic quantum number $k-\ell/2$ . The Hilbert space is $\ell^2$ of finitely supported configurations Site d →₀ Fin (ℓ+1), and the quasi-local algebra is the norm closure of the star-algebra generated by single-site matrix units on it (a faithful copy of the abstract quasi-local algebra).
hamiltonian d ℓ Λ sums over nearest-neighbour pairs ( $\ell^1$ distance one) with one orientation per edge; box d n is $[-n,n]^d$ ; dynamics is the limUnder of the box dynamics, and DynamicsConverges asserts that these limits exist.
State packages a continuous linear functional with $\omega(1)=1$ and $\omega(A^*A)\ge0$ ; IsKMS β ω requires $0<\beta$ and, for every $A,B$ , a bounded $F$ continuous on the closed strip, complex-differentiable on the open strip, with the two boundary identities.
The conclusion reads $\operatorname{Im}\omega(S^z_0)=0$ and $\operatorname{Re}\omega(S^z_0)\ge\ell/8$ .

A complete development needs quantum spin systems on $\mathbb Z^d$ , Lieb–Robinson-type existence of infinite-volume dynamics, KMS states, and the probabilistic loop machinery. The quantum-spin and KMS infrastructure is reusable for other lattice models (including the Bloch-law missions of this family). Contributions formalizing the existence of the dynamics, Proposition 2.2 (spin-to-loop representation), Proposition 3.1 (simultaneous pin test) and Proposition 8.2 (vanishing-field limit) are welcome.

Selected references

OpenAI, Spontaneous magnetization in the quantum Heisenberg ferromagnet, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Spontaneous-magnetization-in-the-quantum-Heisenberg-ferromagnet-September-24-2026/paper.pdf
E. H. Lieb, Long Range Order for the Quantum Heisenberg Model, Mathematical Physics Open Problems, Problem A, 1999. https://web.math.princeton.edu/~aizenman/OpenProblems_MathPhys/9901.HeisenbergFerr.html
R. Seiringer, The Heisenberg Ferromagnet: A Dilute Bose Gas in Disguise, Oberwolfach Report 7/2025. https://doi.org/10.4171/OWR/2025/7
N. D. Mermin, H. Wagner, Absence of Ferromagnetism or Antiferromagnetism in One- or Two-Dimensional Isotropic Heisenberg Models, Phys. Rev. Lett., 1966. https://doi.org/10.1103/PhysRevLett.17.1133
J. Fröhlich, B. Simon, T. Spencer, Infrared Bounds, Phase Transitions and Continuous Symmetry Breaking, Comm. Math. Phys., 1976. https://doi.org/10.1007/BF01608557
F. J. Dyson, E. H. Lieb, B. Simon, Phase Transitions in Quantum Spin Systems with Isotropic and Nonisotropic Interactions, J. Stat. Phys., 1978. https://doi.org/10.1007/BF01106729
M. Correggi, A. Giuliani, R. Seiringer, Validity of the Spin-Wave Approximation for the Free Energy of the Heisenberg Ferromagnet, Comm. Math. Phys., 2015. https://arxiv.org/abs/1312.7873
B. Nachtergaele, Y. Ogata, R. Sims, Propagation of Correlations in Quantum Lattice Systems, J. Stat. Phys., 2006. https://arxiv.org/abs/math-ph/0603064
J. Borcea, P. Brändén, T. M. Liggett, Negative Dependence and the Geometry of Polynomials, J. Amer. Math. Soc., 2009. https://arxiv.org/abs/0707.2340
R. Haag, N. M. Hugenholtz, M. Winnink, On the equilibrium states in quantum statistical mechanics, Comm. Math. Phys., 1967. https://doi.org/10.1007/BF01646342

11 thms2 active usersReviewed

Completed

Functional Analysis Mathematical Physics Probability·Captain: wurtle

Ground-state condensation in the dilute hard-sphere gasResearch Paper

Motivation

Bose–Einstein condensation (BEC) means that a single one-particle state carries a macroscopic fraction of a many-boson system. It was predicted for the ideal gas by Bose and Einstein (1924–1925) and is observed in dilute atomic gases, but for interacting particles in the thermodynamic limit there was no rigorous proof, even in the ground state. The Penrose–Onsager criterion (Phys. Rev. 1956) identifies condensation with a macroscopic eigenvalue of the one-particle density matrix. Energy asymptotics of the dilute gas are now known to second order, but they do not determine single-orbital occupation, since the one-particle spectral gap closes as the volume grows. Lieb and Yngvason explicitly separated the condensation question from their energy theorem, and Solovej's 2025 survey lists fixed-density ground-state condensation as a major problem in the field (C. R. Physique 2025, Section 5).

This mission asks for a formal proof of ground-state condensation for the dilute three-dimensional hard-sphere Bose gas, 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

1924–1925 — Bose and Einstein predict condensation in the ideal Bose gas (Z. Phys. 1924).
1947 — Bogoliubov's theory assumes a macroscopically occupied zero mode.
1956 — Penrose and Onsager's density-matrix criterion for condensation.
1957 — Dyson's bounds on the hard-sphere ground-state energy (Phys. Rev. 1957); Lee, Huang and Yang predict depletion of order $\sqrt{\rho a^3}$ (Phys. Rev. 1957).
1998 — Lieb and Yngvason prove the leading dilute energy asymptotics $4\pi\rho a$ (PRL 1998).
2002 — Lieb and Seiringer prove BEC for trapped gases in the Gross–Pitaevskii limit (PRL 2002).
2020 — Deuchert and Seiringer: homogeneous Gross–Pitaevskii limit at positive temperature (ARMA 2020).
2021–2026 — Fournais's length scales for BEC (EMS 2021); Fournais–Solovej's Lee–Huang–Yang lower bound including hard cores (Invent. Math. 2023); Basti et al.'s matching upper bound for hard spheres (arXiv:2603.13084); results of Chong–Liang–Nam (JFA 2026) and Junge (arXiv:2603.20776) in joint dilute and large-volume limits.
September 2026 — The OpenAI preprint claims condensation at fixed density and fixed exclusion distance (Theorem 1.1, p. 3).

Setting

Let $\Lambda_L=(\mathbb R/L\mathbb Z)^3$ be the flat torus with torus distance $d_L$ . For $N$ particles and exclusion distance $a>0$ , the allowed configurations are

\Omega_{N,L,a}=\{X\in\Lambda_L^N:\ d_L(x_i,x_j)>a\ \text{for } i<j\}.

The hard-sphere Hamiltonian is the operator of the Dirichlet form $q[f]=\sum_{i=1}^N\int|\nabla_if|^2$ on $H^1_0(\Omega_{N,L,a})$ restricted to symmetric (bosonic) functions; wave functions vanish on forbidden configurations, and $a$ is the scattering length. A ground vector is a normalized bosonic minimizer of $q$ . For a normalized bosonic $\Psi$ , the condensate fraction in the constant orbital $\varphi_0=L^{-3/2}$ is

B(\Psi)=\frac{\langle\varphi_0,\Gamma^{(1)}_\Psi\varphi_0\rangle}{N}=\frac1{L^3}\int_{\Lambda_L^{N-1}}\Bigl|\int_{\Lambda_L}\Psi(x,Y)\,dx\Bigr|^2dY\in[0,1],

and for a density operator it is defined by linearity. The gas parameter is $\rho a^3$ with $\rho$ the density.

Formalization targets

Goal: Theorem 1.1 and Corollary 1.2 (p. 3)

There are absolute constants $\varepsilon_0,c_0>0$ such that, for all $a,\rho>0$ with $\rho a^3<\varepsilon_0$ and every sequence $N_k\to\infty$ , $L_k\to\infty$ with $N_k/L_k^3\to\rho$ :

for every choice of (possibly complex) bosonic ground vectors $\Psi_k$ , $\ \liminf_k B(\Psi_k)\ge c_0$ ;
for every sequence of density operators $T_k$ supported on the bosonic ground spaces, the same bound holds for the occupation of $T_k$ (in particular for the normalized ground-space projections).

The constant $c_0$ does not depend on the gas parameter in this range.

Significance

The result itself. It is a proof of macroscopic condensation in an interacting continuum Bose gas with fixed density and fixed hard core, in the thermodynamic limit, uniformly over all ground states including degenerate ground spaces. Previous rigorous results let the gas parameter tend to zero with the volume, or concerned traps, scaling limits, or positive-temperature settings with different potentials. The theorem gives a positive fraction only; it does not reach the Lee–Huang–Yang depletion law.

Formalizing it. The statement involves Sobolev spaces with Dirichlet conditions on a configuration space of the torus, bosonic symmetry, density operators, and partial traces, none of which are packaged in Mathlib; the Lean development builds them concretely. The proof uses killed Brownian motion, percolation-type path constructions, and second-moment arguments. No machine-checked statement of BEC for an interacting system is known.

Difficulty

Energy estimates alone cannot detect occupation of the constant orbital, because the cost of moving particles out of it is of order $L^{-2}$ per particle and vanishes in the limit. One must show directly that a typical ground state correlates distant parts of the box. The preprint compares a tagged particle's position in distant cells by moving trajectories along random lattice routes; multiplying local comparison costs along a route loses a factor at every step, so instead it averages over random routes and bounds the second moment of the averaged likelihood, where exact cancellation of normalizers leaves a cost depending only on mutual encounters of two routes (Introduction, pp. 4–5; Section 8). A separate phase argument passes from $|\Psi|$ to complex $\Psi$ (Lemma 2.3, p. 9).

Formalization scope

Configurations are Fin N → Fin 3 → AddCircle L; the allowed set uses the Euclidean torus distance with strict inequality a < dist.
The form domain dirichletDomain is the closure, in $L^2\times(L^2)^{3N}$ , of jets of smooth compactly supported test functions with support in the allowed set; energy is the sum of squared $L^2$ norms of the partial derivatives. IsGroundVector means: in the domain, bosonic (a.e. permutation invariant), normalized, and of minimal energy among such vectors.
occupation is exactly $B(\Psi)$ ; mixedOccupation T is the trace of $T$ compressed by the bounded map $\Psi\mapsto L^{-3/2}\int\Psi(x,\cdot)\,dx$ . GroundSupported T says every unit vector in $(\ker T)^\perp$ is (the first component of) a ground vector.
Density operators are positive bounded operators with trace one, computed in a fixed Hilbert basis.
Hypotheses on the sequences are only those of the source; the ground-vector hypothesis is required for every index $k$ , which loses nothing since $\liminf$ depends only on tails.

Selected references

OpenAI, Ground-state condensation in the dilute hard-sphere gas, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf
O. Penrose, L. Onsager, Bose–Einstein condensation and liquid helium, Phys. Rev. 104 (1956). https://doi.org/10.1103/PhysRev.104.576
F. J. Dyson, Ground-state energy of a hard-sphere gas, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.20
T. D. Lee, K. Huang, C. N. Yang, Eigenvalues and eigenfunctions of a Bose system of hard spheres and its low-temperature properties, Phys. Rev. 106 (1957). https://doi.org/10.1103/PhysRev.106.1135
E. H. Lieb, J. Yngvason, Ground state energy of the low density Bose gas, Phys. Rev. Lett. 80 (1998). https://doi.org/10.1103/PhysRevLett.80.2504
E. H. Lieb, R. Seiringer, Proof of Bose–Einstein condensation for dilute trapped gases, Phys. Rev. Lett. 88 (2002). https://doi.org/10.1103/PhysRevLett.88.170409
S. Fournais, J. P. Solovej, The energy of dilute Bose gases II: the general case, Invent. Math. (2023). https://doi.org/10.1007/s00222-022-01175-0
A. Deuchert, R. Seiringer, Gross–Pitaevskii limit of a homogeneous Bose gas at positive temperature, Arch. Ration. Mech. Anal. (2020). https://doi.org/10.1007/s00205-020-01489-4
J. P. Solovej, Mathematical physics of dilute Bose gases, C. R. Physique (2025). https://doi.org/10.5802/crphys.247
G. Basti, M. Brooks, S. Cenatiempo, A. Olgiati, B. Schlein, The Lee–Huang–Yang energy for a dilute gas of hard spheres: an upper bound, arXiv:2603.13084 (2026). https://arxiv.org/abs/2603.13084v2

11 thms2 active usersReviewed