Invariant projections, hyperinvariant subspaces, and transitive algebras

2 papersLean

Constructs a nonzero norm-quasinilpotent operator on every infinite-dimensional separable complex Hilbert space with no nonzero proper closed subspace invariant under every commuting operator. The construction also gives operators with no nontrivial invariant projection in the hyperfinite type II₁ factor.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Invariant-projection counterexamples for every irrational rotation

OpenAI · September 27, 2026

For every irrational angle, we construct a continuous nonnegative circle weight with exactly one zero and logarithmic integral \(-\infty\) whose weighted rotation has no nontrivial invariant projection in the associated hyperfinite type II₁ factor. This answers negatively the question of Zhu, Fang, and Shi, with the angle prescribed in advance. The resulting operator is nonzero and norm-quasinilpotent.

Read PDF Download Source

Cite

@misc{OAI:Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026,
  author = {{OpenAI}},
  title = {{Invariant-projection counterexamples for every irrational rotation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf}{OAI:Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026}},
  year = {2026}
}

Backward intertwiners and a transitive commutant

OpenAI · September 27, 2026

We give a negative answer to the hyperinvariant-subspace problem by constructing, on every infinite-dimensional separable complex Hilbert space, a nonzero bounded norm-quasinilpotent operator with no nonzero proper closed hyperinvariant subspace. Its commutant is a proper strongly closed unital transitive complex operator algebra.

Read PDF Download Source

Cite

@misc{OAI:Backward-intertwiners-and-a-transitive-commutant-September-27-2026,
  author = {{OpenAI}},
  title = {{Backward intertwiners and a transitive commutant}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf}{OAI:Backward-intertwiners-and-a-transitive-commutant-September-27-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

For every irrational rotation angle \(\theta\in(0,1)\), the formalization constructs a continuous nonnegative circle weight with a single zero and logarithmic integral \(-\infty\) whose weighted rotation is nonzero and quasinilpotent. In its associated hyperfinite type \(\mathrm{II}_1\) factor, the operator has no nontrivial invariant projection: \((1-p)Tp=0\) forces \(p=0\) or \(p=1\). The linked statements also include an earlier existence construction, a product realization, and the selected product model's Brown measure \(\delta_0\).

The formalization for the companion paper Backward intertwiners and a transitive commutant gives, on every separable infinite-dimensional complex Hilbert space, a nonzero quasinilpotent operator whose commutant is transitive, proper, and closed in the strong operator topology. Thus no nontrivial closed subspace is invariant under every operator in the commutant.

The hyperinvariant-subspace problem asks whether every bounded operator on a complex Hilbert space has a nontrivial closed subspace invariant under every operator that commutes with it. The formalization gives a negative answer on every separable infinite-dimensional complex Hilbert space: there is a nonzero quasinilpotent operator with a transitive commutant. Its commutant is a proper unital operator algebra closed in the strong operator topology. The construction therefore has no nonzero proper closed hyperinvariant subspace.

Comparator links

Result	Comparator statement
Finite-factor invariant-projection counterexample	FiniteFactor.lean
Quasinilpotent operator with transitive commutant	BackwardIntertwiners.lean
Continuous-weight invariant-projection counterexample	ContinuousCircleWeight.lean
Quasinilpotent operator with a transitive commutant	HyperinvariantSubspaces.lean
Invariant-projection counterexamples for every irrational rotation	IrrationalRotation.lean
Brown measure of the selected product weighted shift	ProductBrown.lean
Quasinilpotent operator without a hyperinvariant subspace	HyperinvariantSubspaces.lean

Scope note on GitHub →