The Parisi formula
in Lean

What the Lean statement says

For inverse temperature β > 0 and external field h, the target is convergence of the free energy, F_N = E[log Z_N]/N, to the value given by the Parisi formula as N tends to infinity. This is a theorem about a Gaussian spin system, not a numerical approximation to the variational problem.

A finite replica-symmetry-breaking scheme consists of overlap levels and masses satisfying ordering and endpoint conditions. The Gaussian recursion defines the Parisi functional for each scheme; the Parisi formula takes its infimum over all schemes and all finite numbers of levels. The formalization already proves that this infimum is over a nonempty, bounded-below set, and that a minimizer exists for each fixed number of levels.

At finite N, a spin configuration is represented as a function from the N sites to two Boolean values, then interpreted as spins ±1. The random Hamiltonian is a centered Gaussian vector in the finite-dimensional space of energies indexed by these configurations. Its covariance is specified directly by the overlap formula above, so the proof uses exactly the normalization stated by the project rather than carrying an asymptotic covariance error.

The Parisi functional is represented by Talagrand’s finite backward Gaussian recursion. The zero-mass step is implemented separately as an expectation—the correct limit of the log-Laplace transform—so schemes with a zero mass are covered without division by zero. The final infimum ranges over every finite number of replica-symmetry-breaking levels; the proof does not replace this construction with a Parisi PDE.

Where the proof stands

The checked Guerra identity expresses the interpolation derivative as an explicit correction minus a nonnegative, mass-weighted squared-overlap remainder. Integrating this identity gives the upper bound. The proof includes Gaussian integration by parts, differentiation through the finite cascade and its outer expectation, and continuity at the interpolation endpoints.

The lower-bound route is now complete as well. Theorem 2.4 feeds the overlap-concentration and convergence argument in Theorem 2.2; combining Theorem 2.2 with Guerra’s upper bound proves convergence of F_N to the value given by the Parisi formula.

How the Lean proof is organized

1. Interpolation and upper bound. The core module defines Talagrand’s interpolating Hamiltonian and the finite cascade. Gaussian integration by parts gives Theorem 2.1: the derivative is the derivative of the comparison function minus a nonnegative, mass-weighted squared-overlap remainder. Endpoint identities and integration yield Guerra’s upper bound.
2. The two-replica estimate. The Section 4 and 5 modules construct the constrained two-replica interpolation, differentiate its disorder, field, variance and mass parameters, and prove the optimality estimates. The final assembly covers positive and negative overlaps, breakpoints, zero initial overlap and terminal cases, producing Theorem 2.4 with one constant uniform over all relevant levels.
3. From concentration to Theorem 2.2. The quadratic gap makes overlaps away from the prescribed level exponentially unlikely. A finite reduction over the attainable Ising overlaps, Proposition 2.3 and a differential inequality then force the interpolation remainder to vanish. The integration module connects this chain to the exact statement of Theorem 2.2.
4. The endpoint argument. The final module chooses a near-optimal finite scheme, applies Theorem 2.2 at a time t₀ < 1, and controls the short interval from t₀ to 1 using the derivative bound from Theorem 2.1. This gives the lower bound; together with Guerra’s upper bound it proves the limit of F_N.

The route to Theorem 2.2

Talagrand’s lower-bound argument studies two replicas—two spin configurations sampled from the same random system—and controls their overlap. For schemes that minimize the Parisi functional at their own number of levels and whose functional values are sufficiently close to the infimum over all finite schemes, Theorem 2.2 asserts convergence of the interpolated free energy on every interval 0 ≤ t ≤ t₀ < 1.

The concentration-to-convergence argument is checked: overlap concentration controls the interpolation remainder, and a differential inequality forces the gap to vanish. The uniform two-replica estimate of Theorem 2.4, obtained from the interpolation and optimality arguments in Sections 3–5, supplies the needed concentration input.

Theorem 2.4 has the uniformity required in the paper: one positive quadratic constant works across finite schemes, every physical level, both signs of the overlap, all breakpoints and the terminal cases, with the system-size threshold chosen afterward. Integrating that estimate through Proposition 2.3 and the checked convergence argument proves Theorem 2.2.

Recent work inside the formalization

Theorem 2.4 is checked. The public Lean theorem states Talagrand’s uniform quadratic bound with the required eventual-in-N quantifiers. It has no proof placeholder and uses only Lean’s standard foundational axioms.

All positive-overlap cases and the negative-overlap region are assembled, including the first level, zero initial overlap, k = 0, breakpoints and terminal padding. This closes the cases that had previously remained outside the local estimates.

Uniform local control is combined with the finite all-region assembly. Taking minima over finitely many levels gives one constant before the system-size threshold, which is the quantifier order needed for the theorem.

Theorem 2.2 and the Parisi formula are checked. The final module connects Theorem 2.4 to the downstream integration theorem and then combines the lower bound with Guerra’s upper bound. Both public declarations use only Lean’s standard foundational axioms.

What formalization adds

Much of the work is in the analytic details that a paper can compress: every differentiation through a nested Gaussian expectation needs measurability, integrability and a dominating bound; separate partial derivatives cannot silently be used as a joint chain rule; and endpoint continuity must be proved when a variance becomes zero. The proof also preserves the order of Talagrand’s quantifiers—for example, the quadratic constant in Theorem 2.4 is chosen before the sufficiently large system size.

The development reuses existing mathematics wherever its statement really matches. Mathlib supplies Gaussian integration, moment-generating-function analyticity, convexity, compactness, filters and calculus under the integral. The locked RSAT dependency supplies finite-state log-partition calculus, Gaussian integration by parts and reusable finite Gaussian-recursion machinery. The project adds the bridges to Talagrand’s normalization and the missing coupled-replica, zero-mass, signed-overlap and boundary arguments; it does not copy or modify the upstream sources.

The repository separates supporting lemmas from the main theorems. Its verification script checks both and runs checks of proof dependencies on completed results. These reject dependence on proof placeholders or axioms beyond the standard Lean foundations. Three older placeholders remain explicitly marked in a legacy milestones file, but none is a dependency of Theorem 2.2 or the Parisi formula.