OpenAI model claims the free group factor problem: L(F₂) ≅ L(F₃), so all free group factors are isomorphic (Lean-formalized)
Family 287 of OpenAI's 6 Oct 2026 math release claims an affirmative answer to the free group factor isomorphism problem, a central open question of von Neumann algebra theory. The 23-page manuscript says L(F₂) and L(F₃) are isomorphic, so by the Dykema–Rădulescu dichotomy all interpolated free group factors, including L(F∞), are isomorphic and their fundamental group is ℝ₊. The result is formalized in Lean by OpenAI, and a reasoning summary is published.
Key facts
- Paper: 'An isomorphism of the free group factors' (dated 23 Sep 2026, 23 pages): 'We solve the free group factor isomorphism problem affirmatively by proving that L(F₂) and L(F₃) are isomorphic as tracial von Neumann algebras'
- Lean scope: 'interpolated free group factors with any parameters r,s>1, including the infinite parameter, are normally trace-preservingly isomorphic'; the fundamental-group consequence is not a separate formal statement
- Reasoning summary (abridged chain of thought): the model first tried rigidity and free-entropy obstructions to an isomorphism (Popa, Boutonnet–Drimbe–Ioana–Popa, Peterson, Jung, Hayes) before finding the construction
Science result
- Field
- mathematics / operator algebras
- Problem
- Free group factor isomorphism problem (is L(F₂) ≅ L(F₃)?)
- Result
- Claimed: yes; all interpolated free group factors L(F_r), 1 < r ≤ ∞, are isomorphic, with fundamental group ℝ₊.
- AI system
- OpenAI internal model (unreleased)
- Human role
- Autonomous by OpenAI's fixed procedure (per README)
- Verification
- Lean formalization by OpenAI (review 'unchecked'); not yet expert-confirmed
- Status
- pending
- Why surprising
- A long-standing central problem of the field, answered affirmatively with a machine-checked proof.
What happened
OpenAI's catalogue says family 287 resolves the free group factor problem: the von Neumann algebras generated by the free groups on two and three generators are isomorphic. A classical dichotomy then makes all of them isomorphic. The Lean formalization covers the isomorphism of all interpolated free group factors.
Why it matters
The problem has been one of the best-known open questions in operator algebras for decades. An affirmative answer, especially one checked by machine, would reshape the field. Until specialists confirm that the Lean definitions of group von Neumann algebras and interpolated factors match the classical ones, and read the construction, it is a claim.
Changelog
- 2026-10-07: created from the openai/math repository
Related events
- OpenAI releases 722 AI-written math manuscripts (372 result families) claiming hundreds of open problems, incl. quasi-Riemann, Unique Games, Hodge for CM abelian varieties and free group factors ★★★★★
- OpenAI's unreleased 'Astra' model claims ten advances in maths and theoretical CS, with Lean proofs ★★★★★
Sources (3)
- paperPaper: An isomorphism of the free group factors
- paperReasoning summary: Isomorphism of free group factors
- codeLean scope note for family 287
id: 2026-10-06-free-group-factors-isomorphism-openai · updated 2026-10-07 · open in the interactive timeline