The Mézard–Parisi formula for diluted spin glasses
From OpenAI Aftermath
The Mézard–Parisi formula for diluted spin glasses concerns spin glasses with a finite mean number of interactions per spin, such as the Viana–Bray model, in which random sparse interactions act on Ising spins. Mézard and Parisi's hierarchical cavity method describes the limiting pressure, the expected logarithm of the partition function per spin, through a hierarchy of distributions of local fields, and Panchenko and Talagrand proved in 2004 that every finite level of this hierarchy gives an upper bound for Poisson-diluted even-arity models of a factorized class, with equality conjectured. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), listed as its result 221 and dated 23 September 2026, claims that equality: for that class, under only first-moment assumptions, the limiting pressure equals the infimum of the trial functional over all finite hierarchy depths. The collection includes a Lean formalization of the main theorem.
Background
- As recounted in the introduction of the manuscript:
- Viana and Bray introduced the classical diluted two-spin model, and Mézard and Parisi developed the hierarchical cavity picture for the fixed-connectivity Bethe-lattice spin glass, with an explicit one-step replica-symmetry-breaking functional. Franz and Leone adapted Guerra's interpolation method to diluted systems and obtained replica-symmetric and one-step bounds for even-arity models, and Panchenko and Talagrand proved the bounds for every finite level; the equality conjecture is stated after their Theorem 4.
- Other exact variational descriptions use different order parameters: the cavity principle of Aizenman, Sims and Starr and its Viana–Bray counterpart by De Sanctis, Panchenko's formula over invariant exchangeable spin distributions, and the invariant-kernel formula of Coja-Oghlan and Perkins for random regular factor graphs under their positivity condition. Panchenko established a hierarchical single-site representation for finite replica-symmetry-breaking asymptotic Gibbs measures of modified models, and Biswas, Chen and Sen and Concetti obtained replica-symmetric formulas in some regimes and a full replica-symmetry-breaking bound for random regular graphs.
The original results
- Claim. Theorem 2.1 of The Mézard–Parisi formula for diluted spin glasses states that for Poisson-diluted even-arity Ising models whose interactions satisfy the Panchenko–Talagrand factorization and positivity conditions, with first moments of the interaction and the external field finite, the thermodynamic limit of the pressure exists and equals the infimum over all finite hierarchy depths of the trial functional. The manuscript states that the theorem does not assume that a trial law attains the infimum or that a limiting Gibbs state with infinite depth has been constructed.
- Consequences, as stated. Corollaries in its last section state the formula for the Viana–Bray model and for diluted even-spin models with symmetric couplings, for soft random SAT with an even number of literals per clause and nonnegative clause weights, and a variational formula for the expected ground-state energy obtained as the zero-temperature limit.
- Method, as described: the upper bound is the interpolation bound of Franz–Leone and Panchenko–Talagrand. For the lower bound, the manuscript adds bounded Poisson perturbations to a cavity reservoir, uses a calculus for finite probability trees to obtain identities for prescribed replica branching patterns, concentrates all finite multioverlaps on average over branching depths by shifting each branching depth one level later, and then replaces cavity sites by independent copies of a hierarchical message process. It states that its lower bound holds for every bounded interaction law invariant under permutations of its inputs, without factorization or positivity.
- Formalization, as described by the repository. The scope note states that the formalization proves the 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, for every even arity at least two and every positive interaction density. The Comparator statement is
DilutedSpin.lean. - Source (openai/math repository, commit
7ef5c0c): The Mézard–Parisi formula for diluted spin glasses, dated 23 September 2026.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | The hierarchical cavity formula for diluted spin glasses, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claimed exact Mézard–Parisi variational formula for a specified even-arity interaction class as an infimum over finite hierarchies. It stresses that the interaction assumptions are part of the theorem and that the main obstacle is the control of all replica patterns, that is of all multioverlaps rather than pair overlaps alone, and outlines the key steps of the proof. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records a sandboxed Comparator pass for DilutedSpin. Its note states that the formal statement matches the summary for the Panchenko–Talagrand class, with the named models as instances of the class rather than separate statements. As a caveat it notes that the pressure and the hierarchical functional are hand-written with Bochner integrals and an infimum that take the value zero off the integrable class, which it describes as a fidelity risk, not a trivialization. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the DilutedSpin solution, in 1,416 s. C. Toledo's report lists the challenge among those certified by both kernels. |
Repository. |
| 2026-10-12 | Y. Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics, arXiv:2610.17090v1, section 9.4.1 | Reading (survey of methods) | Records the claimed formula and notes that the lower bound is stated for every bounded permutation-invariant interaction, while the factorization and positivity hypotheses are conditions on the model class, verified for the Viana–Bray model and soft SAT, not assumptions on the Gibbs measure. It describes the marked-depth Poisson perturbations with identities for prescribed trees, the depth shift that controls the coefficients of fresh splits, and the recursive encoding of a single site as the instruments, and states that the concentration of all finite multioverlaps is the factorization that Panchenko had described as missing. It also notes that OpenAI's reasoning summary for the result names Barbier–Panchenko and Mourrat–Panchenko, whom the paper does not cite. | Preprint, released under CC BY 4.0; its caveats state that the architecture and selected estimates of section 8 were inspected without checking every inequality and that the Lean development was not compiled. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_273 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. It states that it read all sections and checked by hand, among other steps, the interpolation upper bound, the finite-tree calculus, the cavity increment, the perturbation and concentration estimates and the decorrelation induction in detail. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-17 | AI Proved What?, episode 221 Many states, one exact formula?, remade version of 22 October 2026 | Reading (exposition) | Video explainer of the claim that, for Panchenko and Talagrand's class of Poisson-diluted models with interactions on an even number of spins, a factorized form and a sign condition, and only first moments of couplings and fields, the limiting log partition function per spin exists at every temperature and density and equals the infimum of the hierarchical trial functional over all finite depths, covering the Viana–Bray model, diluted even-spin models with symmetric couplings, soft random SAT with an even number of literals per clause and their ground-state limits. The episode states that only the lower bound is new and that the result does not cover an odd number of spins per interaction, so not random 3-SAT, nor fixed-degree graphs, the depth needed, a full replica-symmetry-breaking functional or a description of the Gibbs states. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 36 pages, dated September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem. The page states that the preprint has not been revised since the repository's initial commit of 6 October 2026, that the main theorem is formalized against a pinned statement in about 56,000 lines with no unproved steps, which the site did not build, and that the corollaries are not formalized. It states that 403 of the 405 Lean files are reused by the release's random 3-SAT result, that OpenAI's reasoning summary for this result names three works as inspirations that the paper does not cite, and that it found no expert reaction or earlier proof and no OSVerify review. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
- See also The random k-SAT satisfiability threshold.
