Partial Differential Equations

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).

Motivation

The mixed $p$-spin model is a random polynomial on the hypercube $\{-1,+1\}^N$: a centered Gaussian process $H_N(\boldsymbol\sigma)$ with covariance $\mathbb E\{H_N(\boldsymbol\sigma)H_N(\boldsymbol\sigma')\} = N\xi(\langle\boldsymbol\sigma,\boldsymbol\sigma'\rangle/N)$. Its maximum $\mathrm{OPT}_N = \max_{\boldsymbol\sigma} H_N(\boldsymbol\sigma)/N$ is a canonical random optimization problem; for $\xi(t) = c_2^2t^2$ it is the ground state of the Sherrington–Kirkpatrick model. Auffinger and Chen (AC17) proved that $\mathrm{OPT}_N$ converges almost surely to the infimum of the zero-temperature Parisi functional $\mathsf P$ over a space $\mathscr U$ of non-decreasing order parameters.

El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) characterize what a class of message-passing algorithms achieves on this problem. The answer is the infimum of the same functional over a larger space $\mathscr L$ of order parameters that need not be monotone. Whether these algorithms reach the true optimum is therefore the question whether $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$. The paper proves this equality under the no-overlap gap assumption, that the Parisi minimizer over $\mathscr U$ can be taken strictly increasing (Assumption 2, p. 8). This is believed to hold for the Sherrington–Kirkpatrick model and to fail for pure $p$-spin models with $p \ge 3$. This mission formalizes that equality, stated as a property of the minimizer.

Timeline. Parisi's formula (1979) was proved by Talagrand (2006) and Panchenko (2013). Auffinger and Chen (2017) gave its zero-temperature form (1.7). Jagannath and Tobasco (JT16) gave a PDE and variational treatment of the Parisi functional at positive temperature, including its convexity. Montanari (Mon19) gave a message-passing algorithm for the Sherrington–Kirkpatrick model under no overlap gap. El Alaoui, Montanari and Sellke (2020) extended it to mixed $p$-spin models and introduced the extended principle over $\mathscr L$.

Setting

A mixture is $\xi(t) = \sum_{k\ge2} c_k^2 t^k$ with $\xi(1+\varepsilon) < \infty$ for some $\varepsilon > 0$, with derivatives $\xi'$ and $\xi''$ given by the termwise series. Order parameters are functions $\gamma : [0,1) \to \mathbb R_{\ge0}$, in one of two spaces:

$$\mathscr U = \Big\{\gamma \text{ non-decreasing},\ \int_0^1\gamma(t)\,dt < \infty\Big\},\qquad \mathscr L = \Big\{\|\xi''\gamma\|_{TV[0,t]} < \infty\ \forall t<1,\ \int_0^1\xi''(t)\gamma(t)\,dt < \infty\Big\}.$$

Here $\|\cdot\|_{TV[0,t]}$ is total variation on $[0,t]$, and $\mathscr U \subseteq \mathscr L$.

For a step function $\gamma = \sum_i \gamma_i \mathbb I_{[t_{i-1},t_i)}$ with $\gamma_i \ge 0$ (the space $\mathrm{SF}_+$), the Parisi PDE

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

is solved explicitly by the Cole–Hopf recursion (7.3). It is a Gaussian log-moment-generating step on each piece, and a heat-semigroup step where $\gamma_i = 0$. For general $\gamma \in \mathscr L$, $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n \to \gamma$ in the weighted norm $\int_0^1\xi''|\gamma_n - \gamma|$. The Parisi functional is

$$\mathsf P(\gamma) = \Phi^\gamma(0,0) - \frac12\int_0^1 t\,\xi''(t)\gamma(t)\,dt .$$

The process $X$ is the strong solution of $dX_t = \xi''(t)\gamma(t)\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$, $X_0 = 0$ (Eq. (6.3)), driven by a standard Brownian motion $B$.

Formalization targets

Goal: the monotone minimizer is a minimizer over $\mathscr L$ (Section 6.3, p. 34)

If $\gamma_* \in \mathscr U$ is strictly increasing on $[0,1)$ and $\mathsf P(\gamma_*) \le \mathsf P(\gamma)$ for every $\gamma \in \mathscr U$, then

$$\mathsf P(\gamma_*) \le \mathsf P(\gamma)\qquad\text{for every }\gamma \in \mathscr L .$$

Since $\mathscr U \subseteq \mathscr L$, this is the paper's main result 2 (p. 4), $\inf_{\mathscr U}\mathsf P = \inf_{\mathscr L}\mathsf P$ under no overlap gap.

Milestones

1. Lemma 6.7 (p. 27): for $\gamma\in\mathscr L$, $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$.
2. Proposition 6.8 (p. 27): the right derivative of $s\mapsto\mathsf P(\gamma+s\delta)$ at $0$ is $\frac12\int_0^1\xi''(t)\delta(t)\big(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t\big)\,dt$, for admissible directions $\delta$ that vanish near $t = 1$.
3. Lemma 6.15 (p. 33): under no overlap gap, $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\} = t$ for every $t\in[0,1)$.
4. Convexity (Section 6.3, p. 34): $\mathsf P$ is convex on $\mathscr L$.

Significance

The result. The goal identifies the value reached by the paper's message-passing algorithm with the ground-state energy whenever the Parisi minimizer is strictly increasing. Combined with the paper's algorithmic theorem, it yields a $(1-\varepsilon)$-approximation of $\mathrm{OPT}_N$ in time linear in the input size, for the Sherrington–Kirkpatrick model and any other mixture with no overlap gap (Corollary 2.2). It also gives a structural fact about the variational problem: when the minimizer is strictly increasing, the monotonicity constraint in $\mathscr U$ is not binding.

Formalizing it. The result is proved in the paper, but the proof leans on an external citation ([JT16, Theorem 20]) for convexity of $\mathsf P$ on $\mathscr L$. It also applies the first-variation formula in a direction that does not meet that formula's stated hypotheses. A machine-checked development closes both gaps. No part of this theory (the Parisi PDE, its Cole–Hopf solution, or the extended functional) has been formalized before, to our knowledge.

Difficulty

The obvious argument is: convexity plus stationarity gives a global minimum. Both inputs are hard. Stationarity (Lemma 6.15) needs the first variation of $\mathsf P$ in directions that keep $\gamma_*+s\delta$ monotone. That variation is a derivative of the solution of a nonlinear PDE with respect to its coefficient, expressed through an SDE driven by that solution's own gradient. Convexity of $\mathsf P$ on $\mathscr L$ is not visible from the formula: $\Phi^\gamma(0,0)$ is defined through a limit of nested Cole–Hopf recursions, and the paper does not prove it, citing a positive-temperature argument instead. Finally, the goal needs the first variation in the direction $\gamma - \gamma_*$, which is generally non-zero near $t = 1$, where $\xi''\gamma$ may blow up. Proposition 6.8 as stated excludes such directions.

Formalization scope

• Mixture. A coefficient sequence c : ℕ → ℝ with $c_0 = c_1 = 0$ and $\sum_k c_k^2(1+\varepsilon)^k < \infty$ for some $\varepsilon>0$. $\xi'$ and $\xi''$ are explicit power series.
• Order parameters. Functions $\mathbb R\to\mathbb R$; membership in $\mathscr U$ and $\mathscr L$ reads only $[0,1)$. Total variation is eVariationOn; finiteness of integrals is IntegrableOn (which includes measurability).
• Cole–Hopf. Step-function data $(m,t,a)$ with $m\ge1$. The $\gamma_i = 0$ pieces use the heat semigroup, the limit of (7.3). The terminal condition is $|x|$. Gaussian expectations are integrals against gaussianReal 0 1.
• $\Phi^\gamma$ on $\mathscr L$. limUnder of the Cole–Hopf values along step-function data converging to $\gamma$ in the weighted $L^1$ distance. $\partial_x$ is deriv in $x$.
• SDE. The published definition EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by $0$ after time $1$. Brownian motion is Mathlib's IsBrownianReal, and expectations are Bochner integrals.
• Minimality. Always attainment, $\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma$ in the space, never a real infimum (which Lean sets to $0$ on unbounded sets).
• Disclosed hypothesis. Lemma 6.15 assumes that some $c_k \ne 0$. For $\xi\equiv0$ it is false: $\mathsf P\equiv0$, $X\equiv0$, and the left side is constant in $t$. The goal does not need it.
• Ruled out. A formalization that defines $\Phi^\gamma$ as an arbitrary weak solution of the PDE, or via a choice from an unproved existence statement, would make $\mathsf P$ unconstrained. It is not acceptable. Encoding the hypothesis on $\gamma_*$ as minimality over $\mathscr L$ would make the goal trivial.
• Proof gaps in the source. Convexity of $\mathsf P$ on $\mathscr L$ is cited, not proved. The step from stationarity to the goal applies Proposition 6.8 outside its stated hypotheses. The statements are the paper's and are believed true.
• Out of scope. The paper's algorithmic results (Theorems 2–4, Corollary 2.2) assert algorithms with complexity bounds in an informal computation model, and rest on a long state-evolution analysis. They are not part of this mission.

Contributions welcome: Cole–Hopf regularity (smoothness and the bound $|\partial_x\Phi|\le1$), the Lipschitz estimate in $\gamma$ that makes $\Phi^\gamma$ well defined, well-posedness of the SDE, and Itô calculus for the first variation. The Cole–Hopf layer and the SDE well-posedness are reusable for the companion missions on the full-support theorem and the stochastic-control duality of the same paper.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904v1
• 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(7), 2016. https://arxiv.org/abs/1502.04398
• A. Montanari, Optimization of the Sherrington–Kirkpatrick Hamiltonian, FOCS 2019. https://arxiv.org/abs/1812.10897
• M. Talagrand, The Parisi formula, Ann. Math. 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
• D. Panchenko, The Parisi ultrametricity conjecture, Ann. Math. 177(1), 2013. https://arxiv.org/abs/1112.1003

Motivation

Feedback laws that damp vibrations in elastic structures are implemented by sensors and actuators, and a physical loop always reacts with some time delay $\tau>0$: the damping force at time $t$ is computed from the velocity measured at time $t-\tau$. Datko, Lagnese and Polis showed in 1986 that an arbitrarily small delay in a boundary feedback can destroy the stability of a one-dimensional wave equation (Datko–Lagnese–Polis, SIAM J. Control Optim. 24 (1986)), and Datko showed that such fragility is common to a broad class of feedback-stabilized hyperbolic systems (Datko, SIAM J. Control Optim. 26 (1988)). Delay-robustness is therefore a genuine question for every stabilizing feedback, not a technicality.

Nicaise and Pignotti (SIAM J. Control Optim. 45 (2006) 1561–1585) identified a simple sufficient condition in several space dimensions: if the feedback contains an undelayed velocity term with gain $\mu_1$ and a delayed one with gain $\mu_2$, and $\mu_2<\mu_1$, the energy still decays exponentially; if $\mu_2\ge\mu_1$, instabilities appear for some delays. This mission formalizes the stability half for internal (distributed) damping, localized near the Neumann part of the boundary.

Timeline.

• 1986: Datko, Lagnese, Polis — small delays destabilize a boundary-damped 1D wave equation.
• 1988: Datko — many feedback-stabilized hyperbolic systems are not robust with respect to small delays.
• 1990: Zuazua — exponential decay for the semilinear wave equation with locally distributed damping, without delay (Comm. PDE 15 (1990)); Liu (1997) treats locally distributed damping for general conservative systems (SIAM J. Control Optim. 35 (1997)).
• 2006: Nicaise, Pignotti — exponential decay with a delayed boundary or internal feedback under $\mu_2<\mu_1$ (Theorems 1.1 and 1.3), and instability examples when $\mu_2\ge\mu_1$ (Theorems 1.2 and 1.4).

Setting

Let $\Omega\subset\mathbb{R}^n$, $n\ge1$, be a bounded open set with boundary $\Gamma$ of class $C^2$, split as $\Gamma=\Gamma_D\cup\Gamma_N$ with $\overline{\Gamma_D}\cap\overline{\Gamma_N}=\emptyset$ and $\Gamma_D\neq\emptyset$. Write $\nu$ for the outer unit normal, $d\Gamma$ for the surface measure, $u_t,u_{tt}$ for time derivatives and $\Delta$ for the Laplacian in $x$.

Geometric hypothesis (1.6)–(1.7): there are a $C^2$ function $v$ and $\alpha>0$ with $\langle D^2v(x)\xi,\xi\rangle\ge2\alpha|\xi|^2$ for all $x\in\overline\Omega$, $\xi\in\mathbb{R}^n$, and $\nabla v(x)\cdot\nu(x)\le0$ on $\Gamma_D$.

Damping coefficient. $\omega\subset\Omega$ is an open neighbourhood of $\Gamma_N$ (in $\Omega$), and $a\in L^\infty(\Omega)$ satisfies

$$a(x)\ge0\ \text{a.e. in }\Omega\quad(1.17),\qquad a(x)>a_0>0\ \text{a.e. in }\omega\quad(1.18).$$

The system (1.12)–(1.16): for gains $\mu_1,\mu_2>0$ and delay $\tau>0$,

$$u_{tt}(x,t)-\Delta u(x,t)+a(x)\big[\mu_1u_t(x,t)+\mu_2u_t(x,t-\tau)\big]=0\quad\text{in }\Omega\times(0,\infty),$$

with $u=0$ on $\Gamma_D$, $\partial u/\partial\nu=0$ on $\Gamma_N$, initial data $u(\cdot,0)=u_0$, $u_t(\cdot,0)=u_1$, and history $u_t(x,t-\tau)=g_0(x,t-\tau)$ for $t\in(0,\tau)$.

The energy. Assume $\mu_2<\mu_1$ (1.8) and fix $\xi$ with $\tau\mu_2<\xi<\tau(2\mu_1-\mu_2)$ (1.10). Then

$$\mathcal F(t)=\frac12\int_\Omega\big\{u_t^2(x,t)+|\nabla u(x,t)|^2\big\}dx+\frac\xi2\int_\Omega a(x)\int_0^1u_t^2(x,t-\tau\rho)\,d\rho\,dx\qquad(1.19).$$

The first summand is the standard energy $\mathcal E(t)$; the second accounts for the velocity history on the delay window.

Formalization targets

Goal: Theorem 1.3

There exist $C_1,C_2>0$, depending on the data but not on the solution, such that every solution satisfies

$$\mathcal F(t)\le C_1\,\mathcal F(0)\,e^{-C_2t}\qquad\forall t\ge0.$$

The constants are left existential, as in the paper, so no later sharpening of rates invalidates the goal.

Milestones (in the order of the proof)

1. (4.4) The energy identity

$$\mathcal F'(t)=-\mu_1\!\int_\Omega a u_t^2(t)-\mu_2\!\int_\Omega a u_t(t)u_t(t-\tau)+\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t)-\frac{\xi\tau^{-1}}2\!\int_\Omega a u_t^2(t-\tau).$$

2. Proposition 4.1 $\mathcal F$ is nonincreasing and $\mathcal F'(t)\le-C\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx$ with $C>0$.
3. Proposition 4.2 Observability for the undamped mixed problem: for $T$ larger than some $T_0$, $\mathcal E_w(0)\le C_1\int_0^T\int_\omega w_t^2\,dx\,dt$.
4. Proposition 4.3 Observability for the delayed system: for $T$ larger than some $\overline T$, $\mathcal F(0)\le C_0\int_0^T\int_\Omega a\{u_t^2(t)+u_t^2(t-\tau)\}dx\,dt$.
5. Contraction step (p. 1579): some $T>0$ and $\widetilde C\in[0,1)$ with $\mathcal F(T)\le\widetilde C\,\mathcal F(0)$ for every solution.

Significance

The result. Theorem 1.3 shows that a localized viscous damping acting only near the Neumann boundary keeps its exponential stabilizing effect when part of the feedback is delayed, provided the delayed gain is dominated by the undelayed one. Together with Theorem 1.4 of the same paper (instability for $\mu_2\ge\mu_1$ and suitable delays) it gives a sharp threshold in terms of the gains. The energy $\mathcal F$ with its history term became the standard Lyapunov functional for delayed wave and plate equations in the literature that followed.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any exponential decay result for a multidimensional wave equation, is known to exist. A complete development would produce reusable Lean infrastructure: energy identities for the wave equation on $C^2$ domains via the divergence theorem, the delay-energy calculus, and an observability inequality for the wave equation with mixed boundary conditions. Each milestone has value on its own; Proposition 4.2 in particular is a classical control-theoretic result.

Difficulty

The energy estimates (milestones 1 and 2) are calculus once the divergence theorem is available. The central difficulty is observability. Energy dissipation alone gives only $\mathcal F$ nonincreasing; exponential decay needs the energy at time $0$ to be controlled by the energy dissipated on $[0,T]$ (Proposition 4.3), and that needs the conservative wave equation to be observable from $\omega$ (Proposition 4.2). The observability inequality does not follow from energy identities: the paper relies on Carleman estimates of Lasiecka–Triggiani–Yao (1999) and a compactness–uniqueness argument, neither of which is available in Mathlib. The obvious attempt, a multiplier identity with $\nabla v\cdot\nabla u$ alone, leaves boundary terms on $\Gamma_N$ that cannot be absorbed without a localization near $\Gamma_N$ and a lower-order compactness step.

Formalization scope

• Points are EuclideanSpace ℝ (Fin n) with 1 ≤ n; solutions are real valued.
• The $C^2$ boundary is given by a global $C^2$ defining function $\psi$ with $\Omega=\{\psi<0\}$, $\partial\Omega=\{\psi=0\}$, $\nabla\psi\ne0$ on $\partial\Omega$; $\nu=\nabla\psi/|\nabla\psi|$.
• The surface measure $d\Gamma$ is a finite measure carried by $\partial\Omega$ for which the Gauss–Green formula holds for every $C^1$ vector field; this determines it uniquely. It is not Mathlib's unnormalized Hausdorff measure.
• Solutions are classical: $u$ is $C^2$ on $\mathbb{R}^n\times\mathbb{R}$, the equation holds for every $t>0$ and almost every $x\in\Omega$ (because $a$ is only $L^\infty$), and the initial data and history are the values of $u$ and $u_t$ at $t\le0$. This is a subclass of the paper's solutions, so the formal theorems are consequences of the paper's.
• $a$ is measurable and essentially bounded on $\Omega$; (1.17) and (1.18) are almost-everywhere conditions. "Open neighbourhood of $\Gamma_N$" means $\omega\supseteq O\cap\Omega$ for some open $O\supseteq\Gamma_N$ (a subset of $\Omega$ cannot contain $\Gamma_N$ itself).
• Added hypothesis (Propositions 4.2, 4.3, the contraction step and Theorem 1.3): the closure of every connected component of $\Omega$ meets $\Gamma_D$; this holds whenever $\Omega$ is connected. The proof of Proposition 4.2 uses Poincaré's inequality for functions vanishing on $\Gamma_D$, and its compactness–uniqueness step concludes that a harmonic function vanishing on $\Gamma_D$ with zero normal derivative on $\Gamma_N$ is zero; both need this condition.
• "Decreasing" in Proposition 4.1 is read as nonincreasing; its constant $C>0$ is existential, chosen before the solution.
• Printed slips on p. 1575: the last line of (4.3) integrates with $d\Gamma$ where $dx$ is meant, and its first line repeats $u_\rho(x,t-\tau)$ for $u_\rho(x,t-\tau\rho)$. Neither affects any formal statement; (4.4) itself is correct.
• A formalization in which the $a$-weighted integrals are Lean's junk value $0$ (non-measurable $a$), in which $\omega$ is required to contain $\Gamma_N$ (unsatisfiable), or in which the surface measure is arbitrary, would trivialize or falsify the targets; all three are excluded by the definitions.

Needed infrastructure: the divergence theorem on $C^2$ domains (assumed here as a structure field), differentiation under the integral sign for the energies, Carleman estimates or another route to observability for the mixed wave problem, and a compactness argument (Rellich). Contributions of any of these as standalone lemmas are welcome.

Selected references

• S. Nicaise, C. Pignotti, Stability and instability results of the wave equation with a delay term in the boundary or internal feedbacks, SIAM J. Control Optim. 45(5):1561–1585, 2006. https://doi.org/10.1137/060648891
• R. Datko, J. Lagnese, M. P. Polis, An example on the effect of time delays in boundary feedback stabilization of wave equations, SIAM J. Control Optim. 24:152–156, 1986. https://doi.org/10.1137/0324007
• R. Datko, Not all feedback stabilized hyperbolic systems are robust with respect to small time delays in their feedbacks, SIAM J. Control Optim. 26:697–713, 1988. https://doi.org/10.1137/0326040
• E. Zuazua, Exponential decay for the semilinear wave equation with locally distributed damping, Comm. Partial Differential Equations 15:205–235, 1990. https://doi.org/10.1080/03605309908820684
• K. Liu, Locally distributed control and damping for the conservative systems, SIAM J. Control Optim. 35:1574–1590, 1997. https://doi.org/10.1137/S0363012995284928
• I. Lasiecka, R. Triggiani, P. F. Yao, Inverse/observability estimates for second-order hyperbolic equations with variable coefficients, J. Math. Anal. Appl. 235:13–57, 1999 (reference [14] of the paper; the Carleman estimates used in Proposition 4.2). https://doi.org/10.1006/jmaa.1999.6348