# The generator problem for finite factors

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

- [Relative generation and the generator problem for finite factors](../../preprints/Relative-generation-and-the-generator-problem-for-finite-factors-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Single generation of separable-predual $\mathrm{II}_1$ factors | [FactorGeneration.lean](../ComparatorChallenges/FactorGeneration.lean) |
| Dense relative generators for irreducible inclusions of finite factors | [RelativeGeneration.lean](../ComparatorChallenges/RelativeGeneration.lean) |