∑math20

Operator algebras · Result 296

The generator problem for finite factors

1 paperLean

Proves that every type II1 factor with separable predual is generated by a single operator, equivalently by two self-adjoint operators, resolving the generator problem. More strongly, for every irreducible inclusion \(P\subset M\) of such factors, the unitaries u with \(M=W^*(P,u)\) form a dense Gδ subset in the trace 2-norm topology.

Watch

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

Papers 1

First page of Relative generation and the generator problem for finite factors

Relative generation and the generator problem for finite factors

OpenAI · September 23, 2026

We prove that every type II1 factor with separable predual is generated by one operator, equivalently by two self-adjoint operators. Combined with the established direct-integral reduction to this case, this gives an affirmative solution of the generator problem for von Neumann algebras with separable predual.

Read PDF Download Source

Cite
@misc{OAI:Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026,
  author = {{OpenAI}},
  title = {{Relative generation and the generator problem for finite factors}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf}{OAI:Relative-generation-and-the-generator-problem-for-finite-factors-September-23-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 answers the generator problem affirmatively for type \(\mathrm{II}_1\) factors with separable predual: one bounded operator generates the factor under adjoints and weak-operator closure. It imposes no separability assumption on the representing Hilbert space or on the operator-norm topology.

It also proves the paper's relative-generation result. For an irreducible inclusion of type \(\mathrm{II}_1\) factors with separable predual for the larger factor, the unitaries that generate the larger factor together with the smaller one form a dense \(G_\delta\) set in the normalized trace two-norm topology. The normalized faithful normal trace is included in the assertion.

Comparator links

ResultComparator statement
Single generation of separable-predual \(\mathrm{II}_1\) factorsFactorGeneration.lean
Dense relative generators for irreducible inclusions of finite factorsRelativeGeneration.lean

Scope note on GitHub →