∑math20

Probability and statistical mechanics · Result 231

The free uniform spanning forest is a factor of IID

1 paperLean

On every infinite connected locally finite simple unweighted graph, the free uniform spanning forest is a factor of independent vertex labels, by one isomorphism-equivariant rule using no root. Translation-invariant strongly Rayleigh binary processes on every countable group, including invariant determinantal processes with Hermitian positive-contraction kernels, are also factors of IID.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The free uniform spanning forest is a factor of IID

The free uniform spanning forest is a factor of IID

OpenAI · September 25, 2026

We prove that the free uniform spanning forest is a factor of IID on every infinite connected locally finite simple unweighted graph. One Borel rule works for all such graphs and uses no root, answering affirmatively the general factor question for unimodular random graphs. We also show that every translation-invariant strongly Rayleigh process indexed by a countable group is a factor of IID, including invariant determinantal processes with Hermitian positive-contraction kernels. This group-action conclusion requires no amenability.

Read PDF Download Source

Cite
@misc{OAI:The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026,
  author = {{OpenAI}},
  title = {{The free uniform spanning forest is a factor of IID}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf}{OAI:The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalization proves that the free uniform spanning forest is a factor of independent identically distributed vertex labels on every infinite connected locally finite simple unweighted graph. One Borel equivariant rule works for all such graphs and uses no distinguished root.

The linked supplements also give equivariant IID sampling for invariant strongly Rayleigh laws on countable groups and existence, uniqueness, and IID-factor results for determinantal laws with Hermitian positive-contraction kernels on countable index sets. These group results require neither amenability nor finite generation, and the kernels need not be trace class.

Comparator links

ResultComparator statement
Strongly Rayleigh and determinantal-process IID factorsStronglyRayleighDPP.lean
A universal IID factor for the free uniform spanning forestFreeUniformSpanningForest.lean

Scope note on GitHub →