∑math20

Probability and statistical mechanics · Result 221

The Mézard–Parisi formula for diluted spin glasses

1 paperLeanreasoning

Proves the Mézard–Parisi hierarchical cavity formula for Poisson-diluted even-arity Ising models satisfying the Panchenko–Talagrand factorization and positivity assumptions, with only first-moment integrability. The limiting free energy equals the infimum over finite-depth hierarchical trial laws. This includes the Viana–Bray model, symmetric diluted even-spin models, and weighted soft even-K satisfiability.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of The Mézard–Parisi formula for diluted spin glasses

The Mézard–Parisi formula for diluted spin glasses

OpenAI · September 23, 2026

We prove the Mézard–Parisi hierarchical cavity formula for diluted even-arity Ising models in the Panchenko–Talagrand class. This resolves the variational equality conjecture for that class: the limiting pressure equals the infimum of the trial functional over all finite hierarchy depths and trial laws. Only first moments of the interaction and external field are required.

Read PDF Download Source

Cite
@misc{OAI:The-Mezard-Parisi-formula-for-diluted-spin-glasses-September-23-2026,
  author = {{OpenAI}},
  title = {{The M{\'e}zard--Parisi formula for diluted spin glasses}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Mezard-Parisi-formula-for-diluted-spin-glasses-September-23-2026/paper.pdf}{OAI:The-Mezard-Parisi-formula-for-diluted-spin-glasses-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves the Mézard–Parisi hierarchical cavity formula for diluted even-arity Ising models in the Panchenko–Talagrand class. Under the class's factorization, independence, integrability, and positivity assumptions, the finite-system pressure converges to the infimum of the trial functional over all finite hierarchy depths and trial laws. The arity is any even integer at least two and the interaction density is positive.

Comparator links

ResultComparator statement
Mézard–Parisi variational equality for diluted even-arity spin glassesDilutedSpin.lean

Scope note on GitHub →

Reasoning summary

OpenAI released an abridged summary of the model's reasoning for this result: The Mézard–Parisi formula for diluted spin glasses (PDF).