Partial Differential Equations

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

Motivation: when are optimal transport maps continuous?

Given two probability densities $\rho_0,\rho_1$ on a compact Riemannian manifold, optimal transport with the quadratic cost $c(x,y)=d(x,y)^2/2$ seeks the map $T$ pushing $\rho_0\,\mathrm{vol}$ to $\rho_1\,\mathrm{vol}$ at least total cost. McCann proved that such a map exists and is unique almost everywhere (McCann 2001). Whether it is continuous when the densities are merely bounded above and below depends on the geometry of the cost: the Ma–Trudinger–Wang (MTW) condition, a sign condition on a fourth derivative of $c$, is the decisive curvature hypothesis, and its weak form is known to be necessary. The question is whether weak MTW is also sufficient on every compact manifold, with estimates that do not degenerate as transport graphs approach conjugate points.

Background

• 1992 — Caffarelli's regularity theory for maps with convex potentials, based on sections and contact-volume comparison (Caffarelli 1992).
• 2001 — McCann's polar factorization on Riemannian manifolds (McCann 2001).
• 2005 — Ma, Trudinger and Wang introduce the curvature condition (MTW 2005).
• 2009 — Loeper links MTW to supporting cost functions and shows its necessity for continuity (Loeper 2009).
• 2010 — Loeper and Villani: uniform estimates under strict MTW and nonfocality (Loeper–Villani 2010).
• 2011 — Figalli, Rifford and Villani: transport continuity implies convex injectivity domains and weak MTW; on surfaces continuity is equivalent to their conjunction, and the equivalence with weak MTW alone is posed (FRV 2011).
• 2013 — Figalli, Kim and McCann: Hölder continuity and injectivity of optimal maps under weak MTW with cost-convexity hypotheses (FKM 2013), and products of round spheres (FKM 2013).
• 2015 — Figalli, Gallouët and Rifford: weak MTW implies convex injectivity domains on nonfocal manifolds (FGR 2015).
• 2019 — Lebedeva, Petrunin and Zolotov list the convexity and continuity questions (LPZ 2019, Questions 8.6–8.7).
• 2026 — Two OpenAI preprints (OpenAI Math Release, September 25, 2026): a companion proving that weak MTW forces convex injectivity domains and global support, and Uniform Bi-Hölder Transport from Weak MTW (this mission), claiming uniform bi-Hölder optimal maps for every density-bounded class. Neither is peer reviewed, and the theorem is not formally verified.

Setting

Let $(M,g)$ be a smooth, connected, compact Riemannian manifold without boundary, of dimension $n\ge2$, with distance $d$ and volume $\mathrm{vol}$. Put $c(x,y)=\tfrac12 d(x,y)^2$ and let

$$I(x)=\{p\in T_xM:\ d(x,\exp_x(ap))=a|p| \text{ for some } a>1\}$$

be the open injectivity domain. Weak MTW: for every $p\in I(x)$ and $\xi\perp\eta$ in $T_xM$,

$$-\frac32\,\frac{\partial^4}{\partial s^2\partial t^2}\,c\big(\exp_x(t\xi),\exp_x(p+s\eta)\big)\Big|_{s=t=0}\ \ge 0 .$$

For $0<\lambda\le\Lambda$, the density class consists of measurable $\rho$ with $\int\rho\,d\mathrm{vol}=1$ and $\lambda\le\rho\le\Lambda$ almost everywhere. An optimal map from $\rho_0$ to $\rho_1$ is a measurable $T$ with $T_\#(\rho_0\mathrm{vol})=\rho_1\mathrm{vol}$ minimizing $\int c(x,T(x))\rho_0(x)\,d\mathrm{vol}$ among such maps.

In Lean, metricVolume n is the $n$-dimensional Hausdorff measure normalized to agree with Lebesgue measure on $\mathbb R^n$ (which equals Riemannian volume), riemannianExp is defined from complete geodesics, and WeakMTW uses iteratedDeriv 2 twice.

Formalization targets

Goal: uniform bi-Hölder optimal maps

Fix $(M,g)$ satisfying weak MTW and $0<\lambda\le\Lambda$ with a nonempty density class. There are $\alpha\in(0,1]$ and $C<\infty$, depending only on $(M,g),\lambda,\Lambda$, such that for all densities $\rho_0,\rho_1$ in the class, the almost-everywhere unique optimal map has a homeomorphic representative $\widetilde T$ with

$$d(\widetilde T x,\widetilde T x')\le C\,d(x,x')^\alpha,\qquad d(\widetilde T^{-1}y,\widetilde T^{-1}y')\le C\,d(y,y')^\alpha .$$

This is Theorem 1.1 of the source. The goal is published on the platform with status Open.

Significance

The result itself. The constants are common to the whole density class; they do not depend on the densities or their derivatives, and the theorem allows conjugate cut points without nonfocality, strict MTW, or cut avoidance. Combined with the necessity result of Figalli–Rifford–Villani it gives the equivalence of weak MTW with transport continuity for bounded densities on compact manifolds, with uniform estimates in the forward direction. No explicit exponent is obtained (the positive exponent comes from a contradiction argument).

Formalizing it. The Lean statement packages existence, almost-everywhere uniqueness, homeomorphic regularity and uniform bi-Hölder bounds in one assertion over all density pairs, making precise what "class-uniform" means. A proof requires the companion geometric results (convex injectivity domains, global support), McCann's theorem, and Caffarelli-type section estimates on manifolds — none currently in Mathlib.

Difficulty

Hölder estimates obtained after localizing near a smooth part of the cost give a density-dependent exponent and localization scale; they do not give a common scale or constant for a family whose transport graphs approach conjugate pairs, where the cost stops being smooth. Weak MTW constrains the cost only where it is smooth and only for orthogonal directions. Earlier uniform results needed strict MTW and nonfocality, or special geometry (products of spheres).

Formalization scope

• Volume is the normalized Hausdorff measure euclideanVolumeFactor n • μH[n]; densities are AEMeasurable, integrable, of mass one, and between lam and cap almost everywhere; nonemptiness of the class is a hypothesis, as in the source.
• IsOptimalMap requires measurability, the pushforward identity for withDensity measures, and minimality among all measurable maps with that pushforward; uniqueness is almost everywhere for $\rho_0\,\mathrm{vol}$.
• The conclusion requires one $\alpha\in(0,1]$ and one $C\ge0$ before quantifying over densities, and a homeomorphism M ≃ₜ M with the same exponent and constant for $T$ and $T^{-1}$; a trivializing choice is excluded because $T$ must itself be optimal.
• Weak MTW is a hypothesis only at $p\in I(x)$ and orthogonal $\xi,\eta$.
• Needed infrastructure: Riemannian geodesics and cut locus, semiconvex potentials, Kantorovich duality and McCann's theorem, Hausdorff measure versus Riemannian volume, Caffarelli-type sections.

Selected references

• L. A. Caffarelli, The regularity of mappings with a convex potential, J. Amer. Math. Soc. 5 (1992), 99–104. https://doi.org/10.1090/S0894-0347-1992-1124980-8
• R. J. McCann, Polar factorization of maps on Riemannian manifolds, Geom. Funct. Anal. 11 (2001), 589–608. https://doi.org/10.1007/PL00001679
• 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
• 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
• 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
• A. Figalli, Y.-H. Kim and R. J. McCann, Hölder continuity and injectivity of optimal maps, Arch. Ration. Mech. Anal. 209 (2013), 747–795. https://doi.org/10.1007/s00205-013-0629-5
• A. Figalli, Y.-H. Kim and R. J. McCann, Regularity of optimal transport maps on multiple products of spheres, J. Eur. Math. Soc. 15 (2013), 1131–1166. https://doi.org/10.4171/JEMS/388
• 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
• N. Lebedeva, A. Petrunin and V. Zolotov, Bipolar comparison, Geom. Funct. Anal. 29 (2019), 258–282. https://doi.org/10.1007/s00039-019-00481-9
• OpenAI, Global Support and Convex Injectivity Domains under Weak MTW, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Global-Support-and-Convex-Injectivity-Domains-under-Weak-MTW-September-25-2026/paper.pdf
• OpenAI, Uniform Bi-Hölder Transport from Weak MTW, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Uniform-Bi-Holder-Transport-from-Weak-MTW-September-25-2026/paper.pdf

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

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

Motivation: can every surface be realized locally in $\mathbb R^3$?

A Riemannian surface is abstract: it is given by a rule $g$ for measuring lengths and angles in local coordinates, not as a surface sitting in space. The local isometric realization problem asks whether every such surface can, near each point, be realized as an honest smooth surface in Euclidean three-space with the same lengths. The question goes back to the classical theory of surfaces. It is settled for real-analytic metrics and for smooth metrics with nonvanishing curvature, while the unrestricted smooth case is listed as open by Yau (Yau 2000, p. 236) and in Ghomi's problem survey (Ghomi 2019, §1.5, Problem 1.9).

Timeline

• 1926–1927 — Janet and Cartan: every real-analytic surface metric is locally realizable analytically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: $C^1$ isometric realizations exist with great flexibility (Nash 1954; Kuiper 1955). At $C^1$ regularity there is no curvature constraint.
• 1971 — Pogorelov constructs a $C^{2,1}$ metric with no local $C^2$ realization (Pogorelov 1971).
• 1985–1986 — C.-S. Lin: local realization for nonnegative curvature and for curvature changing sign cleanly, with finite differentiability (Lin 1985; Lin 1986).
• 1989 — Nakamura and Maeda: smooth local existence when the curvature changes sign cleanly (Trans. AMS 1989).
• 2002 — A Nadirashvili–Yuan preprint states a smooth counterexample with $K\le0$ (arXiv:math/0208127); their published 2008 paper instead proves a $C^{2,1}$ counterexample with $K\ge0$ and leaves the smooth question open (Calc. Var. PDE 2008).
• 2007–2009 — Khuri: counterexamples to local solvability for general Monge–Ampère equations (CPDE 2007), and work on Darboux's equation that leaves the needed curvature profile open (Khuri 2009).
• 2010–2016 — Positive results under finite-order conditions on the curvature zero set (Han–Khuri 2010; T.-Y. Lin 2016).
• 2026 — An OpenAI preprint, A Smooth Metric with No Local Isometric Immersion into Three-Space (OpenAI Math Release, September 24, 2026), claims a smooth metric on $(-1,1)^2$ that has no smooth isometric immersion on any neighborhood of the origin. It has not been peer reviewed, and the claim has not been formally verified.

Setting

Work in coordinates $p=(p_1,p_2)$ on the open square $Q=(-1,1)^2\subset\mathbb R^2$. A Riemannian metric on $Q$ is a map $p\mapsto g(p)$ to symmetric $2\times2$ real matrices that are positive definite; it is $C^\infty$ if every entry $g_{ij}$ is smooth. An isometric immersion of $(U,g)$, for an open set $U\subseteq Q$, is a map $F:U\to\mathbb R^3$ whose differential reproduces $g$:

$$\langle dF_p(v),\,dF_p(w)\rangle_{\mathbb R^3}=v^{\mathsf T} g(p)\,w\qquad(p\in U,\ v,w\in\mathbb R^2),$$

equivalently $\langle\partial_iF,\partial_jF\rangle=g_{ij}$. Positive definiteness forces $dF$ to have rank $2$. In Lean, Coord = Fin 2 → ℝ, Ambient = EuclideanSpace ℝ (Fin 3), square is $Q$, and LocalSmoothPositive packages smoothness of every entry and Matrix.PosDef at every point.

Formalization targets

Goal: a nonrealizable smooth metric (Theorem A)

$$\exists\, g\ \text{smooth, positive definite on } Q\ \text{ such that for every open } U\subseteq Q \text{ with } 0\in U,\ \text{there is no } C^\infty\ F:U\to\mathbb R^3 \text{ with } F^*\langle\cdot,\cdot\rangle=g .$$

This is Theorem A of the source (p. 1). Because a smooth isometric immersion restricts to an embedding near any point, it also rules out local smooth isometric embeddings. The stronger statement that $g$ can be chosen with the full Euclidean Taylor jet at the origin (Corollary 5.3) is not part of the goal. The goal is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem shows that smooth local isometric realization in $\mathbb R^3$ can fail, which answers negatively the unrestricted smooth problem recorded by Yau and Ghomi. It separates the smooth case from the analytic case (Janet–Cartan) and from finite regularity (Pogorelov, Nadirashvili–Yuan 2008). It also shows, by Corollary 5.3, that the infinite-order jet of the metric at a point does not decide realizability. It leaves open the same question under a sign condition $K\ge0$ or $K\le0$, since the construction uses both signs of curvature.

Formalizing it. The statement is short, but the claimed proof combines PDE estimates for Darboux's equation, hyperbolic propagation, a Baire-category argument and a boundary-saddle geometric step. The literature has disagreed about the status of the smooth question (NY2002 versus NY2008), so a machine-checked proof would remove the ambiguity. Mathlib has the manifold calculus needed to state the result (ContMDiff, mfderiv) but none of the PDE layer.

Difficulty

Where the Gaussian curvature $K$ is nonzero, the realization equations are elliptic or hyperbolic and can be solved locally, so any counterexample must exploit degeneracy where $K$ vanishes and changes type. Finite-regularity counterexamples (Pogorelov) do not carry over: existence at every finite order, on neighborhoods that shrink with the order, does not give one smooth map on a fixed neighborhood. Nonsolvable Monge–Ampère equations are also not enough by themselves, because the coefficients of the Darboux equation come from the same metric, so the obstruction has to be built into $g$ itself. Finally, the conclusion must hold for every neighborhood of the origin and every smooth immersion, with no a priori bounds on $F$.

Formalization scope

• The metric is a function on the subtype of the open set coordinateSquareOpen with values in Matrix (Fin 2) (Fin 2) ℝ. Each entry is ContMDiff … ∞ and each value is Matrix.PosDef, which includes symmetry (Hermitian over ℝ).
• The quantifier ranges over all U : Opens Coord with $U\subseteq Q$ and $0\in U$, and over all maps F : U → Ambient that are ContMDiff … ∞ on the open submanifold $U$. The isometry condition is stated with mfderiv and the Euclidean inner product: $\langle dF_p v, dF_p w\rangle = v\cdot(g(p)w)$.
• The conclusion is a negation of existence, so it is not trivialized by a junk value: $g$ must be genuinely smooth and positive definite, and an immersion on any neighborhood, however small, is excluded.
• Infrastructure needed: Gauss equation and second fundamental form in coordinates, Darboux's equation, energy and weighted elliptic estimates, hyperbolic propagation, and the Baire category theorem (available in Mathlib). The surface-theory layer is reusable for other isometric-embedding projects.

Selected references

• M. Janet, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 5 (1926), 38–43. https://rcin.org.pl/dlibra/publication/31746/edition/15034
• É. Cartan, Sur la possibilité de plonger un espace riemannien donné dans un espace euclidien, Ann. Soc. Polon. Math. 6 (1927), 1–7. https://rcin.org.pl/dlibra/publication/32955/edition/18106
• J. Nash, $C^1$ isometric imbeddings, Ann. of Math. 60 (1954), 383–396. https://doi.org/10.2307/1969840
• N. H. Kuiper, On $C^1$-isometric imbeddings. I, Nederl. Akad. Wetensch. Proc. Ser. A 58 (1955), 545–556.
• A. V. Pogorelov, An example of a two-dimensional Riemannian metric admitting no local realization in $E^3$, Dokl. Akad. Nauk SSSR 198 (1971), 42–43. https://www.mathnet.ru/eng/dan36135
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of 2-dimensional Riemannian manifolds with nonnegative curvature, J. Differential Geom. 21 (1985), 213–230. https://doi.org/10.4310/jdg/1214439563
• C.-S. Lin, The local isometric embedding in $\mathbb R^3$ of two-dimensional Riemannian manifolds with Gaussian curvature changing sign cleanly, Comm. Pure Appl. Math. 39 (1986), 867–887. https://doi.org/10.1002/cpa.3160390607
• G. Nakamura and Y. Maeda, Local smooth isometric embeddings of low-dimensional Riemannian manifolds into Euclidean spaces, Trans. Amer. Math. Soc. 313 (1989), 1–51. https://doi.org/10.1090/S0002-9947-1989-0992597-8
• N. Nadirashvili and Y. Yuan, Counterexamples for local isometric embedding, preprint (2002). https://arxiv.org/abs/math/0208127v1
• N. Nadirashvili and Y. Yuan, Improving Pogorelov's isometric embedding counterexample, Calc. Var. PDE 32 (2008), 319–323. https://doi.org/10.1007/s00526-007-0140-7
• M. A. Khuri, Counterexamples to the local solvability of Monge–Ampère equations in the plane, Comm. PDE 32 (2007), 665–674. https://doi.org/10.1080/03605300600635061
• M. A. Khuri, On the local solvability of Darboux's equation, Discrete Contin. Dyn. Syst. (2009, Supplement), 451–456. https://doi.org/10.3934/proc.2009.2009.451
• Q. Han and M. Khuri, Comm. Anal. Geom. 18 (2010), 649–704. https://doi.org/10.4310/CAG.2010.v18.n4.a2
• T.-Y. Lin, Comm. PDE 41 (2016), 1553–1592. https://doi.org/10.1080/03605302.2016.1227336
• S.-T. Yau, Review of geometry and analysis, Asian J. Math. 4 (2000), 235–278. https://doi.org/10.4310/AJM.2000.v4.n1.a16
• M. Ghomi, Open problems in geometry of curves and surfaces, survey (2019), §1.5. https://ghomi.math.gatech.edu/Papers/op.pdf
• OpenAI, A Smooth Metric with No Local Isometric Immersion into Three-Space, OpenAI Math Release preprint, September 24, 2026 (Theorem A, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf

Motivation

An isometric immersion realizes an abstract Riemannian manifold as a surface in Euclidean space whose induced lengths are exactly the prescribed ones. How many dimensions are needed is a classical question. Nash showed that every compact Riemannian $n$-manifold embeds smoothly and isometrically in some Euclidean space; for surfaces his bound is $\mathbb R^{17}$ (Nash 1956). Gromov lowered the immersion dimension for closed surfaces to $\mathbb R^5$ (Partial Differential Relations, 1986, §3.2.4). Three dimensions do not suffice even locally in the smooth category, and Gromov recorded the question whether every smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$ (Gromov 2000, §I, Remark (d)), later attributing it to Chern around 1950 (Gromov 2015, p. 4).

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 23, 2026 (source), which answers the compact, boundaryless form of that question: every closed smooth Riemannian surface admits a smooth isometric immersion into $\mathbb R^4$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Background

• 1926–1927 — Janet and Cartan: analytic Riemannian surfaces embed locally isometrically in $\mathbb R^3$ (Janet 1926; Cartan 1927).
• 1954–1955 — Nash and Kuiper: strictly short immersions in positive codimension can be uniformly approximated by $C^1$ isometric immersions (Nash 1954; Kuiper 1955).
• 1956 — Nash's smooth embedding theorem, dimension $n(3n+11)/2$, i.e. $17$ for surfaces.
• 1973 — Poznyak: $C^{3,\alpha}$ metrics on compact parts of simply connected planar domains admit $C^{2,\alpha}$ isometric immersions into $\mathbb R^4$ (Russ. Math. Surveys 1973).
• 1986 — Gromov: smooth isometric immersions of closed surfaces into $\mathbb R^5$.
• 2026 — Lewicka proves $C^{1,\alpha}$ flexibility in $\mathbb R^4$ for low-regularity metrics on disk-type planar domains (arXiv:2511.16305); a companion OpenAI preprint gives a smooth metric on a square with no local smooth isometric immersion into $\mathbb R^3$; the present preprint claims the closed-surface case in $\mathbb R^4$ (Theorem 1.1, p. 2).

Setting

A closed surface $M$ is a compact smooth two-dimensional manifold without boundary; it need not be orientable or connected. A Riemannian metric $g$ assigns to each $p\in M$ a positive definite inner product $g_p$ on $T_pM$, depending smoothly on $p$. A smooth map $F:M\to\mathbb R^4$ is an isometric immersion if

$$\langle dF_p(v),dF_p(w)\rangle=g_p(v,w)\qquad(p\in M,\ v,w\in T_pM).$$

Positive definiteness of $g$ forces $dF_p$ to be injective, so $F$ is an immersion; self-intersections are allowed.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every closed smooth Riemannian surface $(M,g)$ there is a $C^\infty$ map $F:M\to\mathbb R^4$ with $F^*\delta_4=g$, where $\delta_4=\sum_{i=1}^4dx_i^2$. In Lean this is OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_isometric_immersion.

Significance

The result itself. The theorem lowers Gromov's immersion dimension for closed surfaces from five to four, with no restriction on curvature or topology, and settles the closed case of the question Gromov attributes to Chern. Dimension four is the first codimension in which the smooth problem can have a global answer for all surfaces, since smooth metrics with no local isometric immersion into $\mathbb R^3$ exist. The open (noncompact) case of the question is not addressed.

Formalizing it. Mathlib now has smooth manifolds, tangent bundles and smooth Riemannian metrics, so the statement is expressible without custom geometry. A complete proof would add Whitney's immersion theorem, Sard's theorem in equal dimensions, metric decompositions into rank-one terms, Nash–Moser-type smoothing estimates, and oscillatory correction schemes; none of these are formalized at this level, and all are reusable in geometric analysis.

Difficulty

The isometric immersion equation $dF^{\mathsf T}dF=g$ is a nonlinear system of three equations in four unknown functions, and its linearization loses derivatives, so a direct implicit function argument fails. Convex integration in the Nash–Kuiper style produces only $C^1$ solutions. Poznyak's smooth theory works on planar domains with boundary, but on a closed surface the successive local corrections must remain compatible globally. The preprint keeps a nondegenerate normal geometry (a nonzero vector-valued second fundamental form) through every step, adds the metric deficit one positive rank-one term $a^2dx^2$ at a time via a velocity loop in a plane normal to $F_y$ and $F_{yy}$ (Proposition 3.1, p. 8; Proposition 7.1, p. 25), and then corrects the approximate metric exactly by a smoothing scheme that solves the linearized equation only on oscillatory modes (Proposition 5.1, p. 15). Nonorientable surfaces are handled by starting from an immersion into a small round $3$-sphere, whose radial direction is a global normal (Lemma 9.1, p. 35).

Formalization scope

• $M$ is a type with ChartedSpace (EuclideanSpace ℝ (Fin 2)) M and IsManifold 𝓘(ℝ, ℝ²) ∞ M, assumed compact, Hausdorff and second countable. Being modeled on $\mathbb R^2$ (not a half-space) encodes "without boundary"; no orientability or connectedness is assumed.
• The metric is Mathlib's Bundle.ContMDiffRiemannianMetric of class $C^\infty$ on the tangent bundle.
• The conclusion asks for ContMDiff … ∞ F and equality of the Euclidean inner product of mfderiv images with g.inner p v w for all tangent vectors; immersivity follows and is not stated separately.
• The statement is not trivialized: the conclusion is an exact pointwise identity for a smooth map, and the hypotheses are satisfied by every closed surface with any metric.

Selected references

• OpenAI, Smooth isometric immersions of closed surfaces into Euclidean four-space, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Smooth-isometric-immersions-of-closed-surfaces-into-Euclidean-four-space-September-23-2026/paper.pdf
• J. Nash, The imbedding problem for Riemannian manifolds, Ann. of Math. 63 (1956). https://doi.org/10.2307/1969989
• J. Nash, C¹-isometric imbeddings, Ann. of Math. 60 (1954). https://doi.org/10.2307/1969840
• M. Gromov, Partial Differential Relations, Springer (1986). https://doi.org/10.1007/978-3-662-02267-2
• M. Gromov, Spaces and questions, Geom. Funct. Anal. (2000). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/SpacesandQuestions.pdf
• M. Gromov, Geometric, algebraic and analytic descendants of Nash isometric embedding theorems (2015). https://www.ihes.fr/~gromov/wp-content/uploads/2018/08/nash-copy-Oct9.pdf
• E. G. Poznyak, Isometric immersions of two-dimensional Riemannian metrics in Euclidean space, Russian Math. Surveys (1973). https://doi.org/10.1070/RM1973v028n04ABEH001591
• M. Lewicka, Full flexibility of isometric immersions of metrics with low Hölder regularity in Poznyak theorem's dimension, arXiv:2511.16305v3 (2026). https://arxiv.org/abs/2511.16305v3
• H. Whitney, The singularities of a smooth n-manifold in (2n−1)-space, Ann. of Math. 45 (1944). https://doi.org/10.2307/1969266
• R. S. Hamilton, The inverse function theorem of Nash and Moser, Bull. AMS 7 (1982). https://doi.org/10.1090/S0273-0979-1982-15004-2

Motivation

Lieb–Thirring inequalities bound the negative eigenvalues of a Schrödinger operator $-\Delta-W$ by an integral of the potential. Lieb and Thirring introduced them in 1975 to give a short proof of the stability of matter, and they remain basic tools in mathematical physics, spectral theory and the analysis of many-fermion systems. The sharp constants are known only in a few cases. In one dimension, the Lieb–Thirring conjecture predicts the sharp constant for every exponent $\gamma$: for $1/2<\gamma<3/2$ it should be the constant of the best potential with a single bound state, given by an explicit $\operatorname{sech}^2$ profile.

Timeline

• 1961. Keller solves the one-bound-state variational problem (doi:10.1063/1.1703708).
• 1971, 1974. Inverse-scattering trace identities for the KdV equation give the sharp value $L_{3/2,1}=3/16$ (Zakharov–Faddeev, doi:10.1007/BF01086739; Gardner–Greene–Kruskal–Miura, doi:10.1002/cpa.3160270108).
• 1975–1976. Lieb and Thirring prove their inequalities and state the one-dimensional conjecture (doi:10.1103/PhysRevLett.35.687).
• 1978. Aizenman and Lieb extend semiclassical equality to all $\gamma\ge3/2$ (doi:10.1016/0375-9601(78)90385-7).
• 1996, 1998. Weidl proves finiteness of $L_{1/2,1}$ (doi:10.1007/BF02104912); Hundertmark, Lieb and Thomas obtain its sharp value $1/2$ (doi:10.4310/ATMP.1998.v2.n4.a2).
• 2000. Laptev and Weidl prove sharp semiclassical constants in all dimensions for $\gamma\ge3/2$ (doi:10.1007/BF02392782); Hundertmark, Laptev and Weidl prove $L_{\gamma,1}\le2L^{\rm cl}_{\gamma,1}$ for $1/2\le\gamma<3/2$ (doi:10.1007/s002220000077).
• 2008–2025. Improved constants at $\gamma=1$ by Dolbeault–Laptev–Loss (doi:10.4171/JEMS/142), Frank–Hundertmark–Jex–Nam (doi:10.4171/JEMS/1062) and Corso–Ried (doi:10.1007/s00220-024-05216-y); Levitt's numerics support the conjectured value (doi:10.4171/JST/65).
• 2026. Read and Schulz prove the sharp case $\gamma=1$ (arXiv:2609.10478).

The source of this mission, an OpenAI preprint dated September 23, 2026, proves the conjectured sharp constant for every $1/2<\gamma<3/2$.

Setting

For $0\le W\in L^{\gamma+1/2}(\mathbb R)$, let $H_{-W}$ be the self-adjoint operator of the quadratic form

$$h_{-W}[v]=\int_{\mathbb R}|v'|^2\,dx-\int_{\mathbb R}W|v|^2\,dx,\qquad v\in H^1(\mathbb R).$$

For $\gamma>1/2$ its negative spectrum is discrete; write $\operatorname{Tr}(H_{-W})_-^\gamma=\sum_{\lambda_j<0}|\lambda_j|^\gamma$ with multiplicity, possibly $+\infty$ a priori. The optimal constant is

$$L_{\gamma,1}=\sup_{0\le W\in L^{\gamma+1/2},\ W\not\equiv0}\frac{\operatorname{Tr}(H_{-W})_-^\gamma}{\int W^{\gamma+1/2}},$$

$L^{(1)}_{\gamma,1}$ is the same supremum with only the lowest eigenvalue retained, and the semiclassical constant is

$$L^{\rm cl}_{\gamma,1}=\frac{\Gamma(\gamma+1)}{2\sqrt\pi\,\Gamma(\gamma+3/2)}.$$

Formalization targets

Goal: Theorem 1.1

For $1/2<\gamma<3/2$ and every $0\le W\in L^{\gamma+1/2}(\mathbb R)$,

$$\operatorname{Tr}(H_{-W})_-^\gamma\ \le\ 2\Bigl(\frac{\gamma-1/2}{\gamma+1/2}\Bigr)^{\gamma-1/2}L^{\rm cl}_{\gamma,1}\int_{\mathbb R}W^{\gamma+1/2};$$

the constant equals $L_{\gamma,1}=L^{(1)}_{\gamma,1}$, and with $r=(\gamma-1/2)^{-1}$ equality holds for $W(x)=(r+1)\operatorname{sech}^2(rx)$. The Lean statement OAI.SharpLiebThirring.sharp_lieb_thirring is open on the platform.

Significance

The theorem settles the one-dimensional Lieb–Thirring conjecture on the whole interval $1/2<\gamma<3/2$, extending the case $\gamma=1$ of Read and Schulz: allowing many bound states never beats a single optimally shaped well. Combined with the known endpoint results ($\gamma=1/2$ and $\gamma\ge3/2$), it completes the sharp one-dimensional constants. It also gives the corresponding bound for signed potentials (Corollary 7.3), and through the Laptev–Weidl lifting method one-dimensional sharp constants feed into higher-dimensional estimates.

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 a proof whose key step is a finite-interval action inequality established by a continuation and degree argument for matrix fields.

Difficulty

Single-state bounds and numerical evidence say nothing about potentials with many bound states, and the conjecture requires a bound uniform over all orthonormal families of eigenfunctions. Methods that work at $\gamma=1$ (where the inequality is dual to a kinetic-energy bound for orthonormal families) do not directly apply at other exponents, since the moment $\sum|\lambda_j|^\gamma$ is not linear in the density matrix. The proof must keep track of the individual eigenvalue scales.

Formalization scope

• H1 packages $u\in L^2(\mathbb R;\mathbb C)$ with a weak derivative in $L^2$, tested against smooth compactly supported functions.
• A negative eigenvalue $-k^2$ ($k>0$) is a weak eigenvalue of the form: $h_{-W}(v,u)=-k^2\langle v,u\rangle$ for all $v\in H^1$.
• negativeMoment γ W is the supremum, in $[0,\infty]$, over all finite orthonormal families of such eigenfunctions of $\sum_ik_i^{2\gamma}$; this counts multiplicity and does not presuppose finiteness. oneStateMoment retains one eigenfunction.
• Admissible γ W is $W\ge0$ a.e. and $W\in L^{\gamma+1/2}$; potentialMass is the lower Lebesgue integral of $W^{\gamma+1/2}$; the optimal constants are suprema over admissible $W$ with positive mass.
• For admissible $W$ the integral $\int W\bar uv$ converges for $u,v\in H^1$, so the form is correctly defined.

A complete development needs Sobolev space $H^1(\mathbb R)$ and form methods, the variational characterization of negative eigenvalues, Gamma-function identities for $L^{\rm cl}_{\gamma,1}$, the explicit $\operatorname{sech}^2$ eigenvalue computation, and the paper's action inequality. Contributions formalizing Theorem 2.1 (action inequality) and the equality computation for the $\operatorname{sech}^2$ potential are welcome.

Selected references

• OpenAI, Sharp one-dimensional Lieb–Thirring constants, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-One-Dimensional-Lieb-Thirring-Constants-September-23-2026/paper.pdf
• E. H. Lieb, W. E. Thirring, Bound for the kinetic energy of fermions which proves the stability of matter, Phys. Rev. Lett., 1975. https://doi.org/10.1103/PhysRevLett.35.687
• J. B. Keller, Lower bounds and isoperimetric inequalities for eigenvalues of the Schrödinger equation, J. Math. Phys., 1961. https://doi.org/10.1063/1.1703708
• D. Hundertmark, E. H. Lieb, L. E. Thomas, A sharp bound for an eigenvalue moment of the one-dimensional Schrödinger operator, Adv. Theor. Math. Phys., 1998. https://doi.org/10.4310/ATMP.1998.v2.n4.a2
• A. Laptev, T. Weidl, Sharp Lieb–Thirring inequalities in high dimensions, Acta Math., 2000. https://doi.org/10.1007/BF02392782
• D. Hundertmark, A. Laptev, T. Weidl, New bounds on the Lieb–Thirring constants, Invent. Math., 2000. https://doi.org/10.1007/s002220000077
• R. L. Frank, D. Hundertmark, M. Jex, P. T. Nam, The Lieb–Thirring inequality revisited, J. Eur. Math. Soc., 2021. https://doi.org/10.4171/JEMS/1062
• A. Levitt, Best constants in Lieb–Thirring inequalities: a numerical investigation, J. Spectr. Theory, 2014. https://doi.org/10.4171/JST/65
• L. Read, M. R. Schulz, The sharp one-dimensional Lieb–Thirring inequality for the sum of eigenvalues, preprint, 2026. https://arxiv.org/abs/2609.10478

Motivation

A random conductance model puts a random conductivity on every edge of the lattice $\mathbb Z^d$. It is the simplest discrete model of diffusion in a heterogeneous medium, and its generator is the generator of a random walk in a random environment. Classical stochastic homogenization shows that on large scales the random operator behaves like a constant-coefficient elliptic operator whose homogenized coefficient $A_{\mathrm{hom}}$ is deterministic. The characterization of $A_{\mathrm{hom}}$, however, involves an equation on the whole lattice for every realization of the coefficients. In practice one computes a spatial average over a box of size $L$ of the energy density of an approximate corrector, as in Gloria and Otto (arXiv:1104.1291, §1). The random part of the error of this procedure is a variance. Its size as a function of $L$ determines how large a computational box must be.

Timeline:

• 1979–1981: Kozlov (MR542557) and Papanicolaou–Varadhan (MR712714) prove qualitative homogenization for continuum elliptic equations with random coefficients.
• 1983: Künnemann (MR714611) proves the discrete version, the diffusion limit of reversible jump processes on $\mathbb Z^d$ with ergodic bond conductivities. It provides the corrector and the approximate corrector used here.
• 1986: Yurinskii (MR867870) gives the first quantitative rates, far from optimal.
• 1998: Naddaf and Spencer (preprint, Estimates on the variance of some homogenization problems) introduce the spectral-gap approach and obtain optimal variance bounds under a small-contrast assumption on the conductivities.
• 2011: Gloria and Otto (DOI 10.1214/10-AOP571) prove the optimal variance estimate without any small-contrast assumption, with a logarithmic loss in $d = 2$. This mission formalizes that estimate.

Setting

Fix $d \ge 2$ and $0 < \alpha \le \beta$. Sites are $x \in \mathbb Z^d$ and $e_1,\dots,e_d$ is the canonical basis. An edge $[z, z+e_i]$ carries a conductivity $a(z,i) \in [\alpha,\beta]$; such a field $a$ belongs to the class $\mathcal A_{\alpha\beta}$. The discrete gradients are $\nabla_i u(x) = u(x+e_i) - u(x)$ and $\nabla^*_i u(x) = u(x) - u(x-e_i)$, and $A(x) = \mathrm{diag}[a(x,1),\dots,a(x,d)]$.

The conductivities are i.i.d.: they are distributed according to the product $\nu^{\otimes E}$ over all edges of one probability law $\nu$ on $[\alpha,\beta]$. No density is assumed, so atomic laws are allowed. $\langle\cdot\rangle$ is the expectation and $\operatorname{var}$ the variance.

For a direction $\xi \in \mathbb R^d$ with $|\xi| = 1$ and a cut-off $T > 0$, the approximate corrector $\phi_T$ solves

$$T^{-1}\phi_T(x) - \nabla^*\cdot A(x)\big(\nabla\phi_T(x) + \xi\big) = 0 \qquad (x \in \mathbb Z^d).$$

The zero-order term introduces the length scale $\sqrt T$. The Green's function $G_T(x,y;a)$ is the $\ell^2$ solution of $(T^{-1} - \nabla^*\cdot A\nabla)G_T(\cdot,y) = \delta_y$ in weak form.

A mask $\eta_L : \mathbb Z^d \to [0,1]$ is supported in the box $(-L,L)^d$, sums to $1$ and satisfies $|\nabla\eta_L| \le C_\eta L^{-d-1}$. The averaged energy density is

$$\xi\cdot A_{L,T}\xi = \sum_{x\in\mathbb Z^d}\Big(T^{-1}\phi_T(x)^2 + \big(\nabla\phi_T(x)+\xi\big)\cdot A(x)\big(\nabla\phi_T(x)+\xi\big)\Big)\eta_L(x).$$

Formalization targets

Goal: Theorem 2.1, estimate (2.5)

There are an exponent $q > 0$ and a threshold $T_0$, depending only on $d, \alpha, \beta$, and for each mask constant $C_\eta$ a constant $C$, such that for every law $\nu$ on $[\alpha,\beta]$, every unit $\xi$, every $T \ge T_0$, every $L > 0$ and every mask $\eta_L$:

$$\operatorname{var}[\xi\cdot A_{L,T}\xi] \le \begin{cases} C\,L^{-2}(\ln T)^q, & d = 2,\\ C\,L^{-d}, & d > 2.\end{cases}$$

The statement fixes the shape of the bound, not the value of $q$ or $C$, which is why it is the goal.

Milestones

The milestones follow the paper's proof:

• well-posedness: the Green's function (Definition 2.7) and the approximate corrector (Lemma 2.2, pathwise form);
• the variance estimate Lemma 2.3 for functions of countably many i.i.d. variables;
• deterministic Green's-function bounds: Lemma 2.8 (BMO and decay on dyadic annuli), Lemma 2.9 (Meyers-type higher integrability), Corollaries 2.2 and 2.3;
• susceptibility formulas: Lemmas 2.4 and 2.5, which give $\partial\phi_T/\partial a(e)$ and $\partial G_T/\partial a(e)$;
• measurability: Lemma 2.6;
• a Caccioppoli inequality in probability: Lemma 2.7;
• a convolution estimate: Lemma 2.10;
• moment bounds: Proposition 2.1, which gives $\langle|\phi_T(0)|^q\rangle \lesssim 1$ for $d > 2$ and $\lesssim(\ln T)^{\gamma(q)}$ for $d = 2$;
• the two steps of §3.2: the derivative formula (3.17) and its uniform bound (3.22).

Significance

The result. The estimate says that smooth averages of the energy density fluctuate as if the density were independent from site to site, at the rate $L^{-d/2}$. That rate is the best possible, since the coefficients themselves are independent. In the error analysis of approximations of $A_{\mathrm{hom}}$, this controls the random error and separates it from the systematic error caused by the cut-off $T$. Proposition 2.1, a byproduct, shows that the approximate corrector has all moments bounded uniformly in $T$ when $d > 2$, which yields a stationary corrector (Corollary 2.1 of the paper).

Formalizing it. The theorem has been proved since 2011, and no machine-checked version is known. A formal proof would combine three components that are reusable well beyond this paper:

• a variance inequality for functions of countably many independent variables, in the infinite product measure;
• quantitative regularity of discrete elliptic Green's functions, uniform in the coefficients;
• the sensitivity calculus of solutions with respect to a single coefficient.

Difficulty

The obvious argument fails because the energy density is not independent from site to site: the corrector couples all conductivities through the inverse of a random elliptic operator. Bounding the variance needs the sensitivity of $\xi\cdot A_{L,T}\xi$ to each single conductivity, and that sensitivity is expressed through gradients of the Green's function. Pointwise bounds on $\nabla G_T$ that are uniform in the coefficients do not exist: the continuum counterpart fails, by examples from quasi-conformal mappings. Only averaged decay on dyadic annuli and a small gain of integrability are available, which is why the proof needs the moment bounds of Proposition 2.1. In $d = 2$ the Green's function does not decay, so only BMO-type control is available, and a logarithm of $T$ is lost.

Formalization scope

Statements follow the arXiv v1 reprint (arXiv:1104.1291v1) of the Annals of Probability article; theorem and page numbers refer to it.

• The lattice is Fin d → ℤ. An edge $[z,z+e_i]$ is the pair (z, i), and a coefficient field is a real function on edges; the theorems assume it takes values in $[\alpha,\beta]$.
• The i.i.d. law is Measure.infinitePi of one probability measure $\nu$ on $\mathbb R$ with $\nu([\alpha,\beta]^c) = 0$.
• $\phi_T$ is the unique bounded solution of (2.3) and $G_T(\cdot,y)$ the unique $\ell^2$ solution of (2.11). The definitions file explains why the bounded solution is the paper's stationary $\phi_T$.
• Norms are Euclidean. The mask's gradient bound is componentwise with an explicit constant $C_\eta$.
• Every $\lesssim$ becomes an explicit constant chosen before the law, the coefficients and the spatial variables, and every $\gg 1$ becomes an explicit threshold.
• Variances, lower integrals and infinite sums that could otherwise default to $0$ are either taken in $[0,\infty]$ or come with square-integrability in the conclusion.

Ruling out a trivial formalization. If the constant $C$ were allowed to depend on the law $\nu$ or on the mask, the goal would follow from the boundedness of the energy average alone. If the variance were taken of a function that is not square-integrable, it would be $0$ by convention. The goal fixes $C$ before $\nu$ and $\eta_L$ and requires square-integrability as part of the conclusion.

Not formalized:

• the last sentence of Theorem 2.1, the variance estimate for the corrector $\phi$ itself when $d > 2$. It needs the stationary corrector of Lemma 2.1, whose existence is quoted from Künnemann;
• Lemma 2.8 (ii);
• the stochastic part of Lemma 2.2 (stationarity and zero mean of $\phi_T$), which follows from the pathwise statement as explained in the definitions file.

Welcome contributions are proofs of any milestone and reusable infrastructure: infinite-product variance inequalities, discrete integration by parts, and discrete maximum principles.

Selected references

• A. Gloria, F. Otto, An optimal variance estimate in stochastic homogenization of discrete elliptic equations, Ann. Probab. 39(3) (2011) 779–856. arXiv:1104.1291, DOI 10.1214/10-AOP571
• R. Künnemann, The diffusion limit for reversible jump processes on $\mathbb Z^d$ with ergodic random bond conductivities, Comm. Math. Phys. 90 (1983) 27–68. MR714611
• S. M. Kozlov, The averaging of random operators, Mat. Sb. 109(151) (1979) 188–202. MR542557
• G. C. Papanicolaou, S. R. S. Varadhan, Boundary value problems with rapidly oscillating random coefficients, Colloq. Math. Soc. János Bolyai 27 (1981) 835–873. MR712714
• V. V. Yurinskii, Averaging of symmetric diffusion in a random medium, Sibirsk. Mat. Zh. 27 (1986) 167–180. MR867870
• N. G. Meyers, An $L^p$ estimate for the gradient of solutions of second order elliptic divergence equations, Ann. Scuola Norm. Sup. Pisa 17 (1963) 189–206. MR0159110

Motivation

Nguyen and Tang study the irreversible catalytic network $\mathcal A+\mathcal B\to\mathcal B+\mathcal C$, $\mathcal B+\mathcal C\to\mathcal A+\mathcal B$, a simple reaction–diffusion system with both a positive and a boundary equilibrium (catalyst used up). They settle every mass regime but one and leave it as a conjecture (AIM problem 416).

Timeline. 2021: Fellner–Morgan–Tang give global classical solutions with uniform bounds. 2026: Nguyen–Tang prove convergence for $M_1<M_2$ and $M_1\ge2M_2$ and local results in between, conjecturing global attraction there.

Setting

On a bounded connected smooth domain $\Omega\subset\mathbb R^n$ with $|\Omega|=1$ and $d_1,d_2,d_3>0$:

$$a_t-d_1\Delta a=b(c-a),\quad b_t-d_2\Delta b=b(c-a),\quad c_t-d_3\Delta c=-b(c-a),$$

with homogeneous Neumann conditions and strictly positive $C^2$ compatible initial data. The masses $M_1=\int_\Omega(a_0+c_0)$, $M_2=\int_\Omega(b_0+c_0)$ are conserved. The equilibria are the positive one $(\frac{M_1}2,\,M_2-\frac{M_1}2,\,\frac{M_1}2)$ and the boundary one $(M_1-M_2,\,0,\,M_2)$.

Formalization target

If $M_2\le M_1<2M_2$, every classical solution converges uniformly on $\Omega$ to the positive equilibrium (no rate required).

Significance

This is the last open regime of Nguyen–Tang's stability analysis. Strict positivity is essential: with $b_0\equiv0$ the solution stays away from the positive equilibrium.

Difficulty

For $M_1\ge M_2$ there is no positive lower bound on $\int_\Omega b$, so entropy dissipation can degenerate near the boundary equilibrium ($b=0$), and the local results do not exclude trajectories approaching it.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and $\Delta$ is Mathlib's Laplacian. The domain is $\Omega=\{\varphi<0\}$ for a $C^\infty$ function $\varphi$ with $\nabla\varphi\ne0$ on $\{\varphi=0\}$; the Neumann condition is the derivative within $\overline\Omega$ in the direction $\nabla\varphi$. Solutions are continuous on $[0,\infty)\times\overline\Omega$ and $C^{1,2}$ for $t>0$, and $L^\infty$ convergence is TendstoUniformlyOn. The goal quantifies over classical solutions; their existence is proved in the literature (Fellner–Morgan–Tang; Nguyen–Tang, Theorem 2.1) but is not part of this statement.

Selected references

• T. L. Nguyen, B. Q. Tang, Stability analysis of irreversible chemical reaction-diffusion systems with boundary equilibria, Z. Angew. Math. Phys. 77, 2026, 199. DOI
• K. Fellner, J. Morgan, B. Q. Tang, Uniform-in-time bounds for quadratic reaction-diffusion systems with mass dissipation in higher dimensions, DCDS-S 14, 2021, 635–651. DOI
• AIM open problems list, problem 416. github.com/MColbrook/AIM

Motivation

The ground-state energy of a mixed $p$-spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$, converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$. Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$. This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$, with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$. Its derivatives $\xi'$, $\xi''$ are nonnegative and nondecreasing on $[0,1]$.

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

$$\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .$$

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$.

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

$$\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .$$

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$, for $t\in[t_{i-1},t_i)$,

$$\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.$$

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$.

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$, progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$, with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$. The value is

$$\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}$$

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$,

$$V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .$$

Formalization targets

Goal: Proposition 4.1

$$\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .$$

Milestones

1. Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$, with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$, it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$.
2. Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$, where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$.
3. Lemma 7.3: $V$ solves the HJB equation

$$\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .$$

4. Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$.
5. Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$.

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$, which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ($M_1\in(-1,1)$), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$.

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$, where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$. The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

• Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
• Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$; its value at $t=1$ never matters.
• Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$, the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
• Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
• Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$, where it is bounded below.
• Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$, with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$.
• Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$.
• Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as "$v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
• Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$, and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
• Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$, which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
• N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).