Is the free uniform spanning forest a factor of IID?
The free uniform spanning forest (FUSF) of an infinite connected locally finite graph is the weak limit of uniform spanning trees on finite exhaustions, without wiring the boundary. The wired forest is a factor of IID on transient graphs via Wilson's algorithm rooted at infinity, and Timar proved the free forest is a factor of IID on recurrent and invariantly amenable unimodular random graphs. Lyons (2013) asked, for Cayley graphs, whether the FUSF is a factor of IID. Can the FUSF be generated as an equivariant measurable factor of independent vertex labels, in general and in particular on nonamenable Cayley graphs?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Probability on graphs, uniform spanning forests
- Posed by
- Russell Lyons
- Year posed
- 2013
- Years open
- 13y
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 22 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: there is one Borel, root-independent, equivariant rule such that for every infinite connected locally finite simple unweighted graph with IID uniform vertex labels , the edge set selected by has the FUSF law. Further results: every translation-invariant strongly Rayleigh binary process on a countable group, including invariant determinantal processes with Hermitian positive-contraction kernels, is a factor of IID, with no amenability needed. Not shown: finitary factors or weighted graphs beyond the strongly Rayleigh results.
What the AI did
The release README says every result in it was produced by an unreleased internal OpenAI model following a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. The family is a single manuscript (September 25, 2026).
Verification
No independent mathematician has checked this yet. Checked here: the introduction and Theorem 1.1 were read against Lyons's question as cited; the theorem gives one Borel, root-independent, isomorphism-equivariant rule for all infinite connected locally finite simple graphs, which covers Cayley graphs. Lean: the challenge FreeUniformSpanningForest (theorem OAI.Problem336.fusf_is_factor_iid, solution module OAI.Probability.SpanningForest.Factor) exists at the pinned commit but is not in the formalization catalogue; its statement was read here. Graphs are encoded on vertex set N (so infinite), the FUSF law is defined by limits of uniform spanning tree cylinder probabilities over connected exhaustions, and the rule is required to be measurable and relabelling-equivariant. That is the headline. Not rebuilt here.