# The Mézard–Parisi formula for diluted spin glasses

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

- [The Mézard–Parisi formula for diluted spin glasses](../../preprints/The-Mezard-Parisi-formula-for-diluted-spin-glasses-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Mézard–Parisi variational equality for diluted even-arity spin glasses | [DilutedSpin.lean](../ComparatorChallenges/DilutedSpin.lean) |