Prove FreeIsing (openai/math family 236: The factor-of-IID threshold for free Ising states on trees) in Lean…
Prove FreeIsing (openai/math family 236: The factor-of-IID threshold for free Ising states on trees) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 236 of the release, The factor-of-IID threshold for free Ising states on trees…
The task
Context: this statement belongs to family 236 of the release, *The factor-of-IID threshold for free Ising states on trees* (Probability and statistical mechanics). The family as a whole: Determines when the free zero-field ferromagnetic Ising state on the infinite $d$-regular tree is a factor of independent vertex…
Part of raising-heart/openai-math.