The sharp factor-of-IID threshold for the free Ising model on regular trees

Lean formalization in OpenAI math repository (Result 236)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The sharp factor-of-IID threshold for the free Ising model on regular trees'. For every integer d ≥ 3 and inverse temperature β ≥ 0, the free zero-field ferromagnetic Ising measure on the infinite d-regular tree is a factor of IID exactly when \tanh\beta\le(d-1)^{-1/2}. We prove the positive implication, including equality, resolving the conjecture of Nam, Sly and Zhang; the strict converse is known. The spin factor can be chosen to commute with every tree automorphism on every label input.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 236). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository