Prove DilutedSpin (openai/math family 221: The Mezard–Parisi formula for diluted spin glasses) in Lean 4…
Prove DilutedSpin (openai/math family 221: The Mezard–Parisi formula for diluted spin glasses) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 221 of the release, The Mezard–Parisi formula for diluted spin glasses (Probability…
The task
Context: this statement belongs to family 221 of the release, *The Mezard–Parisi formula for diluted spin glasses* (Probability and statistical mechanics). The family as a whole: Proves the Mezard–Parisi hierarchical cavity formula for Poisson-diluted even-arity Ising models satisfying the Panchenko–Talagrand…
Part of raising-heart/openai-math.