OpenAI claim summary for Math-2819

Single generation of separable-predual finite factors

OpenAI's claim

All type-II_1 factors with separable predual are claimed to have a single operator generator; the established direct-integral reduction then gives single generation for general separable-predual von Neumann algebras. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

For every type-$\mathrm{II}_1$ factor $M$ with separable predual, OpenAI claims self-adjoint $a,b\in M$ with \[ M=W^*(a,b)=W^*(a+ib). \] Here $W^*$ means generated von Neumann algebra. Its relative generation input says that for every irreducible inclusion $P\subset M$ of such finite factors, the unitaries $u$ with $W^*(P,u)=M$ form a dense $G_\delta$ in the trace $2$-norm topology. The headline conclusion is single non-self-adjoint generation.

Outline of the argument

Manuscript 1 (family 296, 2026-09-23): Free independence lets a small perturbation accumulate along many occurrences in a long word, retaining a definite correlation with a chosen target. A free-group convolution bound controls the nonlinear remainder without growth in word length. Coordinate selection returns the ultrapower construction to the factor; density and a corner-and-matrix argument turn relative generation into one-operator generation.

Formal verification

For family 296, the scope page documents the following selections. Selections give one-operator generation for factors with separable predual and dense relative unitary generators of irreducible inclusions in trace two-norm. No operator-norm separability is required. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: FactorGeneration.lean, RelativeGeneration.lean. Declarations: OAI.Generator.single_generation_of_II1_separable_predual, OAI.RelativeGeneration.main_theorem.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, Relative generation and the generator problem for finite factors, 2026-09-23; citation key OAI:Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 296: Lean scope.
• Comparator FactorGeneration.json.
• Comparator FactorGeneration.lean.
• Comparator RelativeGeneration.json.
• Comparator RelativeGeneration.lean.
• OpenAI catalogue entry.