Mathematical Physics

Motivation

Random planar maps are graphs embedded in the sphere, chosen at random; they are the discrete models of two-dimensional quantum gravity. Decorating a map with a Fortuin–Kasteleyn (FK) random-cluster configuration with parameter $q$ couples the geometry of the map to a statistical-mechanics model (percolation, Ising, Potts), and the coupling changes the large-scale shape of the map. For $0<q<4$ the maps are expected to converge to Liouville quantum gravity surfaces; for $q>4$ the cluster weight is so strong that the map is predicted to become tree-like at large scales. This mission concerns that tree-like regime.

Timeline

• 1963. Tutte decomposes planar maps into nonseparable blocks (doi:10.4153/CJM-1963-029-x).
• 1967. Mullin enumerates tree-rooted maps (doi:10.4153/CJM-1967-010-x).
• 1972. Fortuin and Kasteleyn introduce the random-cluster model (doi:10.1016/0031-8914(72)90045-6).
• 1993. Aldous introduces the Brownian continuum random tree (CRT) as the limit of finite-variance conditioned Galton–Watson trees (doi:10.1214/aop/1176989404).
• 2007–2008. Bernardi gives bijective encodings of tree-rooted maps and connects them to the Tutte polynomial (doi:10.37236/928).
• 2016. Sheffield's inventory-accumulation (hamburger–cheeseburger) bijection encodes FK-decorated maps and identifies the transition at $q=4$; his appendix predicts a CRT limit for $q>4$ (doi:10.1214/15-AOP1061). Panagiotou, Stufler and Weller prove CRT limits for subcritical graph classes (doi:10.1214/15-AOP1048).
• 2026. Feng proves an infinite-volume counterpart: an infinite FK map with $q>4$ converges to an infinite CRT in the local Gromov–Hausdorff–Prokhorov topology (doi:10.1007/s00440-025-01424-2); Stufler proves degree-measure CRT limits for maps whose block weights depend only on block size (arXiv:2608.21063).

The source of this mission, an OpenAI preprint dated September 24, 2026, proves the finite-volume CRT prediction for every $q>4$.

Setting

A rooted planar map is a connected graph embedded in the oriented sphere, up to orientation-preserving homeomorphism, with a distinguished dart (oriented edge); loops and multiple edges are allowed. For an edge subset $A\subseteq E(M)$, $k_M(A)$ is the number of connected components of $(V(M),A)$, isolated vertices included. For $q>4$ and $n\ge1$, sample $(M_n,A_n)$ with $|E(M_n)|=n$ according to

$$\mathbb P\bigl((M_n,A_n)=(M,A)\bigr)=\frac{1}{Z_{n,q}}\,q^{\,k_M(A)+(|A|-|V(M)|)/2}.$$

Let $d_n$ be graph distance on $V(M_n)$ using all edges and $\mu_n(\{v\})=\deg(v)/(2n)$.

For a standard normalized Brownian excursion $e$ on $[0,1]$, $d_e(s,t)=e(s)+e(t)-2\min_{[s\wedge t,\,s\vee t]}e$; the quotient by $d_e=0$ with the pushforward $\mu_e$ of Lebesgue measure is the Brownian CRT $(\mathcal T_e,d_e,\mu_e)$.

The Gromov–Hausdorff–Prokhorov (GHP) distance between compact metric probability spaces is the infimum, over isometric embeddings into a common space, of the maximum of the Hausdorff distance of the images and the Lévy–Prokhorov distance of the pushed-forward measures.

Formalization targets

Goal: Theorem 1.1

$$\forall q>4\ \exists c(q)\in(0,\infty):\qquad \bigl(V(M_n),\ c(q)\,n^{-1/2}d_n,\ \mu_n\bigr)\ \Longrightarrow\ (\mathcal T_e,d_e,\mu_e)$$

in distribution for the GHP topology, as $n\to\infty$ through all positive integers. The Lean statement OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt is open on the platform.

Significance

The theorem establishes the tree side of the geometric phase transition of FK planar maps at $q=4$ in the natural finite-volume setting: the law is conditioned on the total size, the metric uses every edge, and the measure is the degree measure. Feng's infinite-volume result does not imply it, and a limit of an unconditioned encoding walk gives neither conditioning nor metric control. Together with companion results for $0<q\le4$, it completes the picture surface versus tree.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would also build reusable infrastructure: combinatorial maps as rotation systems, the GHP topology, and the Brownian CRT, none of which is in Mathlib.

Difficulty

The FK weight of a nonseparable block depends on its shape, not only on its size, so the block-weighted map results with uniform blocks do not apply, and exponential moments of block sizes are not available. The proof must show that the block tree is a critical Galton–Watson tree with finite offspring variance, and that graph distance along every ancestral path is asymptotically a constant times the depth, uniformly over all paths, using only a second moment.

Formalization scope

• A map with $n+1$ edges is a pair of permutations of Fin (2*(n+1)) (edge involution without fixed points, vertex rotation), connected, with $|V|+|F|=n+3$ (genus zero), modulo isomorphisms fixing dart 0. The Lean index $n$ corresponds to $n+1$ edges, and the scale is $c/\sqrt{n+1}$.
• The FK law sums over all Finsets of edge orbits; clusterCount counts components including isolated vertices; loops are omitted from adjacency only.
• MetricMeasureData packages a carrier, a distance and a measure; Valid means a compact metric probability space with Borel σ-algebra. ghpEDist is the infimum over pseudometrics on the disjoint union extending both distances.
• Convergence in distribution is expressed by expectations of bounded tests F continuous for ghpEDist at valid objects.
• The normalized excursion is realized as $\lvert B(t)-tB(1)\rvert$ for a three-dimensional Brownian motion $B$, and the statement holds for every such realization. The limit expectation is a Bochner integral, so measurability of the integrand is part of what must be proved.

A complete development needs Sheffield's inventory bijection or an equivalent finite word identity, Tutte's block decomposition, conditioned Galton–Watson tree limits with finite variance (Aldous; Broutin–Marckert), and GHP comparison lemmas. Contributions formalizing Proposition 2.2 (finite word identity), Proposition 4.3 (exact finite representation), Theorem 5.5 (uniform marked path sums) and Lemma 6.3 (metric and mass comparison) are welcome.

Selected references

• OpenAI, Brownian continuum random tree limits of finite Fortuin–Kasteleyn maps above four, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Brownian-continuum-random-tree-limits-of-finite-Fortuin-Kasteleyn-maps-above-four-September-24-2026/main.pdf
• S. Sheffield, Quantum gravity and inventory accumulation, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1061
• Y. Feng, Triviality of critical Fortuin–Kasteleyn decorated planar maps for $q>4$, Probab. Theory Related Fields, 2026. https://doi.org/10.1007/s00440-025-01424-2
• D. Aldous, The continuum random tree III, Ann. Probab., 1993. https://doi.org/10.1214/aop/1176989404
• C. M. Fortuin, P. W. Kasteleyn, On the random-cluster model I, Physica, 1972. https://doi.org/10.1016/0031-8914(72)90045-6
• W. T. Tutte, A census of planar maps, Canad. J. Math., 1963. https://doi.org/10.4153/CJM-1963-029-x
• N. Broutin, J.-F. Marckert, Asymptotics of trees with a prescribed degree sequence and applications, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20463
• K. Panagiotou, B. Stufler, K. Weller, Scaling limits of random graphs from subcritical classes, Ann. Probab., 2016. https://doi.org/10.1214/15-AOP1048
• B. Stufler, Non-bijective scaling limits and phase transitions of planar maps, preprint, 2026. https://arxiv.org/abs/2608.21063

Motivation

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

Timeline

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

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

Setting

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

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

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

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

Formalization targets

Milestone: Theorem 1.2 (sharp Gaussian minorants)

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

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

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

Goal: Theorem 1.1 (universal energy minimum)

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

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

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

Belief propagation (BP) is the message-passing algorithm used throughout artificial intelligence, coding theory and statistical physics to approximate marginals of graphical models. On graphs with cycles it is a heuristic: it may fail to converge, and when it converges its output need not be the true marginal. Rigorous guarantees had mostly been confined to the high-temperature regime, as a consequence of a uniform decay of correlations (spatial mixing) under which any boundary condition is forgotten; see the works cited as [3, 23, 26] in §1 of the paper.

Dembo and Montanari (arXiv:0804.4726v3, Ann. Appl. Probab. 20 (2010)) proved that for the ferromagnetic Ising model with a positive external field, BP converges exponentially fast on every graph of bounded degree, at every temperature, and that on locally tree-like graphs its fixed point computes local marginals accurately. The low-temperature regime, where the Gibbs measure on the limiting infinite tree is not unique, is the point: the field breaks the $\pm$ symmetry, and monotonicity replaces spatial mixing.

Setting

Let $G=(V,E)$ be a finite graph in which every vertex has at most $\Delta$ neighbours, $\beta\ge0$ an inverse temperature and $B$ a magnetic field. The Ising model on $G$ is the distribution on spin configurations $\underline x\in\{+1,-1\}^V$

$$\mu(\underline x)=\frac1{Z(\beta,B)}\exp\Big\{\beta\sum_{(i,j)\in E}x_ix_j+B\sum_{i\in V}x_i\Big\}.$$

More generally one allows a field $B_i$ at each vertex, and $B_i=+\infty$ (a vertex pinned to $+1$).

A message $\nu_{i\to j}$ is a distribution on $x_i\in\{+1,-1\}$ attached to the directed edge $i\to j$. The BP iteration is

$$\nu^{(t+1)}_{i\to j}(x_i)=\frac1{z^{(t)}_{i\to j}}\,e^{Bx_i}\prod_{l\in\partial i\setminus j}\ \sum_{x_l}e^{\beta x_ix_l}\,\nu^{(t)}_{l\to i}(x_l),$$

with $\partial i$ the neighbours of $i$ and $z^{(t)}_{i\to j}$ a normalization. An initial condition is positive if $\nu^{(0)}_{i\to j}(+1)\ge\nu^{(0)}_{i\to j}(-1)$ on every directed edge. Distances between distributions are in total variation, $\|p-q\|_{\mathrm{TV}}=\tfrac12\sum_x|p(x)-q(x)|$.

For $i_*\in V$, $U=\mathsf B_{i_*}(r)$ is the ball of radius $r$, $\partial U$ its vertices at distance exactly $r$, and $j(i)$ a neighbour in $U$ of each $i\in\partial U$. Given a BP fixed point $\nu^*$, the BP estimate of the marginal on $U$ is

$$\nu_U(\underline x_U)=\frac1{z_U}\exp\Big\{\beta\sum_{(i,j)\in E_U}x_ix_j+B\sum_{i\in U\setminus\partial U}x_i\Big\}\prod_{i\in\partial U}\nu^*_{i\to j(i)}(x_i).$$

The proofs run through Ising models on rooted trees $\mathsf T$: $\mathsf T(\ell)$ is the tree of the first $\ell$ generations, $\partial\mathsf T(\ell)$ the $\ell$-th generation, and $\mu^{\ell,0}$, $\mu^{\ell,+}$ the Ising models on $\mathsf T(\ell)$ with free and plus boundary conditions (the latter pins $\partial\mathsf T(\ell)$ to $+1$). A random tree is conditionally independent with average offspring bounded by $\Delta$ if, given the first $k$ generations, the offspring numbers of generation $k$ are independent with conditional means at most $\Delta$ (Definition 2.5).

Formalization targets

Goal: Theorem 2.6

For $\beta\ge0$, $B>0$ and $\Delta$, there are $A<\infty$ and $\lambda>0$ depending only on $(\beta,B,\Delta)$ such that every finite graph of maximal degree $\Delta$ has a BP fixed point $\nu^*$ with

$$\sup_{(i,j)\in E}\big\|\nu^{(t)}_{i\to j}-\nu^*_{i\to j}\big\|_{\mathrm{TV}}\le A\exp(-\lambda t)$$

for every positive initial condition and every $t\ge0$. The constants are uniform over graphs; this uniformity is the content of the theorem.

Companion: Theorem 2.7

With $c=c(\beta,B,\Delta)$ and $\lambda>0$: if $\mathsf B_{i_*}(t)$ is a tree, then $\|\mu_U-\nu_U\|_{\mathrm{TV}}\le\exp\{c^{r+1}-\lambda(t-r)\}$.

Milestones

The tree estimates of §3–§4, in the order the proofs use them: Griffiths' inequality (Theorem 3.1); the GHS inequality (Theorem 3.2); the reweighting bound in total variation (Lemma 3.3); marginals on subtrees (Lemma 4.1); the $M/\ell$ bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le M/\ell$ on root magnetizations (Lemma 4.3); its extension to marginals near the root (Theorem 4.2); a Simon-type factorization of tree correlations (Lemma 4.4); and Corollary 4.5: exponential decay of correlations (4.13), Theorem 4.2 with rate $Ae^{-\lambda t}$, and the root-magnetization bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le Ae^{-\lambda\ell}$.

Significance

The theorem gives an unconditional convergence guarantee for BP on a nontrivial class of models with cycles, valid deep in the low-temperature phase, with a rate independent of the number of vertices. Theorem 2.7 adds that the fixed point is accurate on locally tree-like graphs such as random regular graphs and sparse Erdős–Rényi graphs, so BP is a polynomial-time algorithm for local marginals there. The tree estimates of §4, in particular the insensitivity of the root to plus versus free boundary conditions on conditionally independent trees, are also the engine of the free-entropy theorem of the same paper (mission 1 of this series).

The results are proved in the paper; none of them, nor Griffiths' or the GHS inequality, has a machine-checked proof known to this mission. Formalizing them produces a reusable library for ferromagnetic Ising models on finite graphs and trees (correlation inequalities, pinned boundary conditions, marginals on subtrees) and a formal account of BP as an operator on message families.

Difficulty

The obvious argument is a contraction: show that one BP step shrinks the distance between message families, uniformly over the graph. At low temperature this fails: the BP map is not a contraction, the infinite-tree Ising model has several Gibbs measures, and without a field BP has several fixed points. Uniform decay of correlations, the tool behind high-temperature results, is false in this regime. What has to be controlled instead is a single, weaker quantity: how much the root of a tree of depth $t$ feels a plus boundary condition compared with a free one, with a bound that is uniform over all trees of bounded average offspring and over all depths. The difficulty is concentrated in that estimate (Lemma 4.3), and in upgrading its $1/\ell$ rate to an exponential one (Corollary 4.5), which is where the positive field enters quantitatively.

Formalization scope

Spins are Booleans (true $=+1$); the edge sum counts each unordered edge once; a field $+\infty$ is a pinned vertex, never a large real number. Graphs are finite (Fintype V) with all degrees at most $\Delta$. Messages are functions on ordered vertex pairs whose values on directed edges are distributions on $\{+1,-1\}$; the BP iterates are computed from the update, not posited. Total variation is $\tfrac12\ell^1$. Trees are encoded by offspring functions on finite words (Ulam–Harris), random trees by probability measures on offspring functions with the product $\sigma$-algebra; conditional independence uses Mathlib's iCondIndepFun, with integrable offspring numbers. Fields on trees are nonrandom functions of the vertex. Expectations that may be infinite, such as $\mathbb E\{C^{|\mathsf T(r)|}\}$, are lower Lebesgue integrals in $[0,\infty]$, and every expectation of a tree functional comes with a measurability conclusion, so that no integral can take a junk value. Constants are quantified before the graph, the tree law and the field, and, where the paper names their dependence (Theorem 4.2's $M(\beta_{\max},B_{\min},\Delta)$ and $C(\beta_{\max},B_{\max})$), as functions of exactly those parameters.

Two readings are fixed explicitly. Theorem 2.7 is stated for every positive BP fixed point, which by Theorem 2.6 is the paper's fixed point. Corollary 4.5's clause (4.13) carries the hypotheses of Theorem 4.2 ($B_i\le B_{\max}$ on $\mathsf T(r-1)$). A fixed point that is not a family of distributions, a "zero message" family, or a bound that holds only because an integral defaults to $0$ does not satisfy these statements.

The computation tree of §5, through which the paper derives Theorems 2.6–2.7 from Corollary 4.5, is a proof device and is not part of any statement; building it is welcome as supporting work. Proofs of the classical inequalities (Griffiths, GHS) are independently reusable.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. arXiv:0804.4726v3, doi:10.1214/09-AAP627
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. MR0266507
• T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). MR776231
• B. Simon, Correlation inequalities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980) 111–126. MR589426

Motivation

The ferromagnetic Ising model is the basic model of statistical mechanics for interacting binary variables. On a finite graph it is a probability distribution over spin configurations, and its normalizing constant, the partition function, encodes the thermodynamics: the free entropy per vertex determines the magnetization, the correlations, and the location of phase transitions. On lattices this quantity is understood only in special cases. On sparse random graphs, such as random regular graphs and Erdős–Rényi graphs with bounded average degree, physicists predicted it with the cavity method (Mézard and Parisi, The Bethe lattice spin glass revisited, 2001): locally these graphs look like trees, and on trees the model can be solved by a recursion. The same recursion underlies belief propagation, the message-passing algorithm used in coding theory and machine learning.

Timeline:

• Dembo and Montanari (2008/2010), Ising models on locally tree-like graphs, Ann. Appl. Probab. 20 (2010) 565–592: for every uniformly sparse graph sequence converging locally to a Galton–Watson tree whose offspring law has finite mean, the free entropy density converges at every temperature $\beta \ge 0$ and every field $B$, and for $B > 0$ the limit is the Bethe prediction. Earlier rigorous results covered special cases, among them Erdős–Rényi graphs in a restricted range of parameters (reference [7] of the paper) and random regular graphs (reference [11]).
• Dembo, Montanari and Sun (2013), Factor models on locally tree-like graphs, extended the approach to a class of factor models on locally tree-like graphs.

Setting

Let $G_n = (V_n = [n], E_n)$ be a sequence of finite graphs. The Ising measure at inverse temperature $\beta \ge 0$ and magnetic field $B \in \mathbb R$ is

$$\mu(\underline x) = \frac{1}{Z_n(\beta,B)} \exp\Big\{\beta \sum_{(i,j)\in E_n} x_i x_j + B \sum_{i \in V_n} x_i\Big\}, \qquad x_i \in \{+1,-1\},$$

each edge counted once, and the free entropy density is $\phi_n(\beta,B) = \frac1n \log Z_n(\beta,B)$.

A degree distribution is a law $P = \{P_k\}$ on $\{0,1,2,\dots\}$ with $0 < \bar P = \sum_k k P_k < \infty$; its size-biased version is $\rho_k = k P_k/\bar P$, and $\bar\rho = \sum_k (k-1)\rho_k$. The Galton–Watson tree $T(P,\rho,\infty)$ has a root with $k$ children with probability $P_k$, and every other vertex independently has $k-1$ children with probability $\rho_k$; $T(P,\rho,t)$ is its first $t$ generations.

The ball $B_i(t)$ is the subgraph induced by the vertices within distance $t$ of $i$, rooted at $i$. The sequence converges locally to $T(P,\rho,\infty)$ if, for every $t$ and every rooted tree $T$, the fraction of vertices $i$ with $B_i(t) \simeq T$ (root-preserving isomorphism) tends to $\mathbb P\{T(P,\rho,t) \simeq T\}$. It is uniformly sparse if $\lim_{l\to\infty}\limsup_n \frac1n\sum_i |\partial i|\,\mathbb I(|\partial i| \ge l) = 0$.

The cavity recursion acts on laws of a real random variable $h$:

$$h \overset{d}{=} B + \sum_{i=1}^{K-1} \xi(\beta, h_i), \qquad \xi(\beta,h) = \operatorname{atanh}[\tanh\beta \tanh h],$$

with $K \sim \rho$ and $h_i$ i.i.d. copies of $h$ independent of $K$. For $B > 0$ it has a unique fixed point $h^*$ supported on $[0,\infty)$. The Bethe functional of a law of $h$ is

$$\varphi_h(\beta,B) = \frac{\bar P}{2}\log\cosh\beta - \frac{\bar P}{2}\mathbb E\log[1+\tanh\beta\tanh h_1\tanh h_2] + \mathbb E\log\Big\{e^B\prod_{i=1}^L[1+\tanh\beta\tanh h_i] + e^{-B}\prod_{i=1}^L[1-\tanh\beta\tanh h_i]\Big\},$$

with $L \sim P$ independent of the $h_i$.

Formalization targets

Goal: Theorem 2.4

Assume $\{G_n\}$ is uniformly sparse, converges locally to $T(P,\rho,\infty)$, and $\sum_k k\rho_k < \infty$. Then for every $\beta \ge 0$:

$$\lim_{n\to\infty}\phi_n(\beta,B) = \varphi_{h^*}(\beta,|B|) \quad (B \ne 0),$$

and $\varphi_{h^*}(\beta,B)$ has a limit $L_0$ as $B \downarrow 0$, with $\phi_n(\beta,0) \to L_0$. This is the paper's statement that the limit exists for every $B$, equals (2.9) for $B > 0$, is even in $B$, and is continuous at $B = 0$.

Milestones

1. Tools on Ising models: Griffiths' inequality (Theorem 3.1), the GHS inequality (Theorem 3.2), the subtree-marginal identity (Lemma 4.1).
2. Trees: the boundary effect on the root magnetization, $\mathbb E\{m^{\ell,+}-m^{\ell,0}\} \le M/\ell$ (Lemma 4.3); the correlation factorization (Lemma 4.4); exponential decay of root-to-generation correlations (Corollary 4.5, (4.13)).
3. The recursion: monotone convergence to the unique nonnegative fixed point (Lemma 2.3) and its Lipschitz dependence on $\beta$ in Monge–Kantorovich distance (Lemma 4.6).
4. The Bethe functional: the second-order perturbation bound (Lemma 6.1, Remark 6.2) and its consequence, stationarity of $\varphi_h$ at fixed points (Corollary 6.3, with corrected constant).
5. From trees to graphs: edge averages converge to averages over the edge-rooted tree $\bar T(\rho,t)$ (Lemma 6.4), and $\partial_\beta\phi_n = \frac1n\sum_{(i,j)\in E_n}\langle x_ix_j\rangle_n$ (6.10).

Significance

The result. Theorem 2.4 establishes the replica-symmetric (Bethe) formula for the ferromagnetic Ising model on the standard sparse random graph ensembles at all temperatures, including below the critical temperature $\tanh\beta_c = 1/\bar\rho$ where the Gibbs measure on the limiting tree is not unique. It identifies the free energy of random regular graphs, Erdős–Rényi graphs and configuration models with arbitrary degree distributions of finite variance, and the derivative identities that follow give the limiting magnetization and energy per edge. The tree estimates of Section 4 also yield the convergence of belief propagation (the companion mission of this series).

Formalizing it. The theorem is proved; nothing in this mission has been machine-checked before. A formal proof requires infrastructure that Lean's Mathlib does not have: Ising measures with boundary conditions, correlation inequalities, Galton–Watson trees as laws of offspring functions, local weak convergence of graph sequences, distributional fixed-point equations, and the Monge–Kantorovich distance on the real line. While stating the milestones, Corollary 6.3 turned out to be false as printed (the constant $\bar P\bar\rho$ should be $\mathbb E[L^2]$; a counterexample is $P = \delta_1$); the mission states the corrected version, which is what the paper's proof gives.

Difficulty

The obvious route through uniqueness of the Gibbs measure on the tree fails below the critical temperature: different boundary conditions give different limits, so local quantities are not determined by the local graph structure alone. The paper replaces uniqueness by insensitivity to positive boundary conditions when $B > 0$ (Lemma 4.3), which rests on Griffiths and GHS monotonicity and on averaging over the random tree; the deterministic statement is false. Passing from derivatives to the free entropy itself requires that the Bethe functional be stationary in the cavity law (Corollary 6.3), so that the $\beta$-dependence of $h^*$ can be ignored. Finally, the case $B = 0$ at low temperature is reached only as a limit: there is no fixed-point characterization at $B = 0$.

Formalization scope

• Spins are Booleans ($+1$ = true); edges are unordered and counted once. Graphs $G_n$ live on Fin n.
• A field $B_i = +\infty$ (plus boundary) is encoded by pinning vertex $i$ to $+1$, never by a large real field.
• Rooted trees are offspring functions List ℕ → ℕ in Ulam–Harris form; random trees are laws of offspring functions under the product σ-algebra. Galton–Watson trees are infinite product measures. Fields on trees are nonrandom functions of the vertex.
• Laws of cavity fields are probability measures on $\mathbb R$; the recursion is a map on ProbabilityMeasure ℝ, and convergence in distribution is weak convergence. Expectations over $L \sim P$ are series $\sum_l P_l\,\mathbb E[\cdot]$ with product laws.
• The Monge–Kantorovich distance takes values in $[0,\infty]$. Uniform sparsity is computed in $[0,\infty]$ so that an unbounded sequence does not get a junk $\limsup$ of $0$.
• The fixed point $h^*$ in the goal is the one supported on $[0,\infty)$, selected by choice; Lemma 2.3 shows it exists and is unique, so an arbitrary fixed point cannot be substituted. Theorem 2.4 is stated with $\beta \ge 0$ and asserts convergence for $B > 0$, $B < 0$ and $B = 0$ separately; the $B = 0$ clause asserts the existence of the one-sided limit rather than assuming it.

A complete development needs: Griffiths and GHS inequalities for finite Ising models (reusable for any ferromagnetic model); Ulam–Harris random trees with conditional independence; local weak convergence of graph sequences (reusable for random graph theory); distributional recursions with stochastic ordering; and the coupling characterization of the Wasserstein-1 distance on $\mathbb R$. Contributions of any milestone are welcome, as are proofs of the classical inequalities of Section 3 independent of this paper.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. https://arxiv.org/abs/0804.4726v3 , https://doi.org/10.1214/09-AAP627
• M. Mézard, G. Parisi, The Bethe lattice spin glass revisited, Eur. Phys. J. B 20 (2001) 217–233. https://doi.org/10.1007/PL00011099
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. https://doi.org/10.1063/1.1665211
• T. M. Liggett, Interacting Particle Systems, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). https://doi.org/10.1007/978-1-4613-8542-4
• A. Dembo, A. Montanari, N. Sun, Factor models on locally tree-like graphs, Ann. Probab. 41(6) (2013) 4162–4213. https://doi.org/10.1214/12-AOP828

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 Ising mixed $p$-spin model assigns to each configuration $\sigma \in \{-1,+1\}^N$ the energy of a random polynomial whose covariance is $\mathbb E\{H_N(\sigma)H_N(\sigma')\} = N\xi(\langle\sigma,\sigma'\rangle/N)$. Its ground-state energy $\max_\sigma H_N(\sigma)/N$ converges to the value of a variational problem, the zero-temperature Parisi formula (Auffinger–Chen 2017), in which a functional $\mathsf P$ is minimized over non-decreasing order parameters $\gamma$. El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) ask how close a polynomial-time algorithm can get to this maximum. Their answer is an extended variational principle: the best value reachable by incremental approximate message passing is $\inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$, where the space $\mathscr L$ drops the monotonicity constraint.

The algorithm that reaches this value is built from a minimizer $\gamma_*$ of $\mathsf P$ over $\mathscr L$, and it runs along the set of times where $\gamma_*$ is positive. Theorem 5 of the paper (p. 30) shows that this set is dense: a minimizer has full support. This mission formalizes that theorem and the first- and second-order optimality conditions it rests on (Section 6.1, pp. 22–31).

Timeline. Parisi proposed the variational formula in 1979. Talagrand (2006) and Panchenko (2013) proved it at positive temperature. Auffinger and Chen (2017) established the zero-temperature version with $\Phi(1,x)=|x|$ and proved that a minimizer over the monotone space exists. Jagannath and Tobasco (2016) developed the PDE and SDE tools for the Parisi functional that Section 6.1 of the present paper adapts to non-monotone order parameters. Montanari (2019) gave the first message passing algorithm for the Sherrington–Kirkpatrick case; the present paper (2020) extended it to general mixtures and introduced $\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$; its derivatives $\xi'$, $\xi''$ are the termwise differentiated power series, non-negative and non-decreasing on $[0,1]$.

An order parameter is a function $\gamma : [0,1) \to \mathbb R_{\ge0}$. The extended space is

$$\mathscr L = \Bigl\{\gamma : [0,1)\to\mathbb R_{\ge0} : \|\xi''\gamma\|_{\mathrm{TV}[0,t]}<\infty\ \forall t\in[0,1),\ \int_0^1\xi''(t)\gamma(t)\,dt<\infty\Bigr\},$$

with the weighted distance $\|\gamma_1-\gamma_2\|_{1,\xi''} = \int_0^1\xi''(t)|\gamma_1(t)-\gamma_2(t)|\,dt$. The non-negative step functions $\mathsf{SF}_+$ are the finite sums $\sum_i a_i\mathbb I_{[t_{i-1},t_i)}$ with $0=t_0<\dots<t_m=1$ and $a_i\ge0$.

For a terminal condition $f_0$ (convex, continuous, even, non-negative, differentiable off $0$ with $0\le f_0'\le1$ on $(0,\infty)$) and $\gamma\in\mathsf{SF}_+$, the Parisi PDE

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

has the explicit Cole–Hopf solution $\Phi^\gamma$: on $[t_{i-1},t_i)$, $\Phi(t,x) = \gamma_i^{-1}\log\mathbb E\exp\{\gamma_i\Phi(t_i, x+\sqrt{\xi'(t_i)-\xi'(t)}\,G)\}$ with $G\sim\mathsf N(0,1)$. For $\gamma\in\mathscr L$, $\Phi^\gamma$ is the limit of $\Phi^{\gamma_n}$ along step functions $\gamma_n\to\gamma$ in the weighted distance. The Parisi functional is

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

Given a Brownian motion $B$, the process $X$ solves $dX_t = \xi''(t)\gamma(t)\,\partial_x\Phi^\gamma(t,X_t)\,dt + \sqrt{\xi''(t)}\,dB_t$, $X_0 = 0$. The support of $\gamma$ is $S(\gamma) = \{t\in[0,1):\gamma(t)>0\}$, and $\overline S(\gamma)$ is its closure in $[0,1)$.

Formalization targets

Goal: Theorem 5

With $f_0(x) = |x|$, if $\gamma_*\in\mathscr L$ satisfies $\mathsf P(\gamma_*) = \inf_{\gamma\in\mathscr L}\mathsf P(\gamma)$, then

$$\overline S(\gamma_*) = [0,1).$$

Milestones

The path to the goal, in attack order:

• Proposition 6.1(b),(c): on step functions, $\partial_x\Phi$ is non-decreasing with $|\partial_x\Phi|\le1$, and $\|\Phi^{\gamma_1}-\Phi^{\gamma_2}\|_\infty\le\|\xi''(\gamma_1-\gamma_2)\|_1$.
• Lemma 6.2: these properties pass to $\gamma\in\mathscr L$.
• Lemma 6.5: the SDE has a unique strong solution on $[0,1]$.
• Corollary 6.6: $\mathbb E\{\partial_x\Phi(t_2,X_{t_2})^2\}-\mathbb E\{\partial_x\Phi(t_1,X_{t_1})^2\}=\int_{t_1}^{t_2}\xi''(s)\,\mathbb E\{(\partial_x^2\Phi(s,X_s))^2\}\,ds$.
• Lemma 6.7: the map $t\mapsto\mathbb E\{\partial_x^2\Phi(t,X_t)^2\}$ is continuous on $[0,1)$.
• Proposition 6.8: the first variation $\frac{d}{ds}\mathsf P(\gamma+s\delta)|_{s=0+}=\frac12\int_0^1\xi''\delta\,(\mathbb E\{\partial_x\Phi(t,X_t)^2\}-t)\,dt$.
• Lemma 6.9: $S(\gamma)$ is a countable disjoint union of intervals.
• Corollary 6.10: $\mathbb E\{\partial_x\Phi^{\gamma_*}(t,X_t)^2\}=t$ on $\overline S(\gamma_*)$ and $\ge t$ off it.
• Corollary 6.11: $\xi''(t)\,\mathbb E\{\partial_x^2\Phi^{\gamma_*}(t,X_t)^2\}=1$ on $\overline S(\gamma_*)$.
• Lemma 6.12: the law of $X_t$ has a density, bounded below on compact sets, once $\gamma$ vanishes.

Significance

The result. Full support identifies the extended variational principle as one whose minimizers are "nowhere flat". The algorithm of Theorem 3 in the paper follows $\gamma_*$ through incremental steps whose size is set by $\gamma_*$, and it needs no special treatment of gaps where $\gamma_* = 0$. The stationarity conditions (Corollaries 6.10–6.11) also characterize minimizers over $\mathscr L$ the way the Auffinger–Chen conditions characterize minimizers over the monotone space. They are the starting point for comparing $\inf_{\mathscr L}\mathsf P$ with the Parisi value.

Formalizing it. The theorem is proved in the paper; nothing here is open mathematics. The paper's proofs rely on cited PDE regularity (Jagannath–Tobasco 2016) and on standard SDE theory, often in one line. The mission produces a machine-checked chain from the explicit Cole–Hopf formula to the support theorem. Along the way it builds the Parisi PDE solution on a non-monotone class, a first-variation formula, and stationarity conditions, none of which have a formal counterpart. No formal statement of the Parisi functional or the Parisi PDE exists on Prove2Me (index search, 2026-10-03).

Difficulty

Two steps resist a direct argument. The first is the first variation (Proposition 6.8): differentiating $\Phi^\gamma(0,0)$ in $\gamma$ requires comparing the SDE for $\gamma$ with the SDE for the perturbed parameter and controlling their difference uniformly, which needs bounds on $\partial_x^2\Phi$ that degenerate as $t\to1$. The second is the exclusion of gaps: on an interval where $\gamma_*=0$ the PDE is a time-changed heat equation, and the contradiction comes from a strict inequality, which requires the law of $X_t$ to charge every interval (Lemma 6.12). The obvious idea of perturbing $\gamma_*$ upward on a gap only yields the inequality (6.14), which is consistent with a gap; the second-order identity at the gap's endpoints is what closes the argument.

Formalization scope

Conventions committed to in Lean:

• The mixture is a coefficient sequence $c$ with $c_0=c_1=0$; $\xi,\xi',\xi''$ are explicit series.
• Order parameters are functions $\mathbb R\to\mathbb R$ read only on $[0,1)$. Membership in $\mathscr L$ uses eVariationOn for the total variation and IntegrableOn for the integral; the latter includes the a.e.-measurability that the paper takes for granted.
• $\Phi^\gamma$ for step functions is the Cole–Hopf recursion (7.3). For a piece with $\gamma_i = 0$ the formula's limit, the heat semigroup, is used instead of a division by zero. $\mathbb E$ over $G$ is integration against gaussianReal 0 1. For $\gamma\in\mathscr L$, $\Phi^\gamma$ is a limit along the filter of step functions converging in the weighted $L^1$ distance; it is never "some solution of the PDE".
• $\partial_x\Phi$ and $\partial_x^2\Phi$ are iterated derivs in $x$. Lemma 6.2's weak-derivative claim is stated as "convex and 1-Lipschitz", its equivalent.
• The SDE uses the published strong-solution concept EthierKurtz.SolvesBrownianSDE in dimension one, with coefficients extended by zero after time $1$. The driver is assumed to be a standard Brownian motion (IsBrownianReal). Statements about $X$ hold for every strong solution, which by Lemma 6.5 is unique.
• Section 6.1's results are stated for every admissible $f_0$; $\mathsf P$ is parametrized by $f_0$, and Theorem 5 fixes $f_0=|\cdot|$.
• Minimality is "$\mathsf P(\gamma_*)\le\mathsf P(\gamma)$ for all $\gamma\in\mathscr L$", never a real infimum. $\overline S(\gamma)$ is closure (S γ) ∩ Ico 0 1. Right-continuity of $\gamma_*$, the paper's convention from p. 28, is a hypothesis.
• Disclosed hypothesis $\xi\not\equiv0$ (some $c_k\neq0$) on Theorem 5, Corollaries 6.10–6.11 and Lemma 6.12. For $\xi\equiv0$ every $\gamma$ minimizes $\mathsf P$ and $X\equiv0$, so $\gamma_*\equiv0$ has empty support and each of those statements fails. When $c_2=0$ no minimizer exists (Corollary 6.11 at $t=0$), and Theorem 5 is vacuous, as in the paper.
• Lemma 6.12's density bound is stated without choosing density versions: $\varepsilon\,\mathrm{Leb}(A)\le\mathbb P(X_t\in A)$ for measurable $A\subseteq[-M,M]$.

A trivializing formalization is excluded: $\Phi^\gamma$ and $X$ are the paper's objects, built from the data, so the goal cannot be met by choosing a convenient solution, and minimality over $\mathscr L$ cannot be satisfied by a junk infimum.

Not formalized: the weak formulation (6.4) of Lemma 6.2, printed with a wrong boundary term; the stochastic-integral identity (6.7) of Lemma 6.5; the regularity Lemmas 6.3–6.4; Proposition 6.1(a). The paper's algorithmic Theorems 2–4 are out of scope, because they concern algorithms in an informal model of computation and an AMP state-evolution theory that is not part of this mission.

Useful infrastructure beyond this mission: the Cole–Hopf solution and its Lipschitz dependence on $\gamma$, the Parisi functional on $\mathscr L$, and the SDE (6.3). Contributions that formalize Itô's formula for these processes or the regularity of $\Phi^\gamma$ are welcome as supporting lemmas.

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, Annals of Probability, 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proceedings of the AMS, 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, Annals of Mathematics 163(1), 2006. https://doi.org/10.4007/annals.2006.163.221
• D. Panchenko, The Parisi ultrametricity conjecture, Annals of Mathematics 177(1), 2013. https://doi.org/10.4007/annals.2013.177.1.8

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