OpenAI claim summary for Math-2917

IID factors for invariant strongly Rayleigh laws on countable groups

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The free spanning forest on every infinite locally finite simple graph is claimed obtainable by one root-free Borel rule from iid labels; invariant strongly Rayleigh processes have an analogous group-equivariant construction.

Mathematical statement of the claimed result

Result 1.

One Borel root-independent rule $\Phi(G,U,e)\in\{0,1\}$ is claimed to work for every infinite graph that is connected, has finite degrees, and is simple, undirected and unweighted. With independent uniform vertex labels, its selected edge set \[ \{e:\Phi(G,U,e)=1\} \] has the free uniform spanning-forest law and the rule commutes with graph isomorphisms. The second theorem takes any countable group $\Gamma$ and any translation-invariant strongly Rayleigh law $\nu$ on $\{0,1\}^\Gamma$. It supplies a Borel map $\Phi_\nu:[0,1]^\Gamma\to\{0,1\}^\Gamma$, equivariant at every input, whose iid-uniform input has output law $\nu$.

Outline of the argument

Finite determinant tilts define a canonical response drift for the free forest law. Brownian observations provide independent innovations, and a deterministic inverse reconstructs the sampler; vertex labels are converted to independent edge paths in a measurable rule that also applies to varying graphs.

Formal verification

For family 231, the Lean scope includes a root-free iid rule for free spanning forests and invariant strongly Rayleigh and determinantal sampling supplements without amenability assumptions. The listed Comparator files are FreeUniformSpanningForest.lean, StronglyRayleighDPP.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, The free uniform spanning forest is a factor of IID, 2026-09-25; citation key OAI:The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: thm:sr-group.
• Family 231: Lean scope.
• Comparator FreeUniformSpanningForest.json.
• Comparator FreeUniformSpanningForest.lean.
• Comparator StronglyRayleighDPP.json.
• Comparator StronglyRayleighDPP.lean.
• OpenAI catalogue entry.