Aftermath bot: New page for the OpenAI hyperinvariant subspace and invariant projection counterexamples with background, Lean scope and four public rows

2026-10-18T14:21:32Z

New page for the OpenAI hyperinvariant subspace and invariant projection counterexamples with background, Lean scope and four public rows

New page

'''The hyperinvariant subspace problem''' asks whether every bounded nonscalar operator on an infinite-dimensional separable complex Hilbert space has a nonzero proper closed subspace invariant under every operator that commutes with it. Two manuscripts dated 27 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claim a negative answer, a nonzero quasinilpotent operator with no such subspace, together with operators in the hyperfinite II1 factor that have no nontrivial invariant projection, with a Lean formalization. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introductions of the two manuscripts:
** A closed subspace is hyperinvariant for ''T'' if every operator in the commutant {''T''}′ leaves it invariant. An operator algebra is transitive if its only common closed invariant subspaces are 0 and the whole space, so ''T'' lacks hyperinvariant subspaces exactly when its commutant is transitive. Douglas and Pearcy studied this connection, and Arveson proved that a transitive algebra containing a maximal abelian self-adjoint subalgebra is strongly dense.
** The ordinary invariant subspace problem and the hyperinvariant problem are distinct questions. The hyperinvariant manuscript states that a preprint of Kérchy and Pearcy claiming their equivalence was withdrawn after a counterexample, and that Atzmon and Sodin's 1999 question, whether their completely indecomposable bilateral weighted shifts with spectrum the unit circle have proper hyperinvariant subspaces, remains open.
** In finite factors, Haagerup and Schultz attached an invariant projection to each Borel set of the Brown measure, so a Brown measure that is not a point mass gives nontrivial invariant projections. Dykema and Haagerup found hyperinvariant subspaces for the quasinilpotent DT-operator, and Tucci gave quasinilpotent generators of the hyperfinite factor with invariant projections. For weighted irrational rotations, Dykema and Schultz identified the Brown measure, and Zhu, Fang and Shi asked whether such an operator with determinant zero must have a nontrivial invariant projection in the factor.

== The original results ==
* '''Claim (hyperinvariant subspaces).''' Corollary 1.2 of ''Backward intertwiners and a transitive commutant'' states that every infinite-dimensional separable complex Hilbert space admits a nonzero bounded norm-quasinilpotent operator with no nonzero proper closed hyperinvariant subspace, whose commutant is a proper strongly closed unital transitive algebra. The manuscript states that this also gives a negative answer to the question whether every unital transitive operator algebra is strongly dense. The operator is built from bilateral weighted shifts over the 2-adic integers, whose own invariant subspaces are coordinate tails, together with a commuting contraction that moves those tails backward, and it satisfies an explicit bound on the norms of its powers. The manuscript notes that the operator has many ordinary invariant subspaces.
* '''Claim (invariant projections).''' Theorem 1.1 of ''Invariant-projection counterexamples for every irrational rotation'' states that for every irrational angle θ there is a continuous weight ''f'' on the circle with exactly one zero and logarithmic integral −∞ such that the weighted rotation ''U f''(''V'') has no nontrivial invariant projection in the hyperfinite II1 factor of the rotation, answering the question of Zhu, Fang and Shi negatively. Its Corollary 1.4 derives the hyperinvariant counterexample a second way, and its Remark 1.5 states that this contradicts a hyperinvariant-subspace assertion of Cho, Ko and Lee.
* '''Sources.''' The manuscripts [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026 Backward intertwiners and a transitive commutant] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026 Invariant-projection counterexamples for every irrational rotation].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/293.md lean/docs/293.md] states that the formalization gives, on every separable infinite-dimensional complex Hilbert space, a nonzero quasinilpotent operator whose commutant is transitive, proper and strongly closed, and, for every irrational rotation angle, the continuous-weight invariant-projection counterexample, with an earlier existence construction and the Brown measure δ0 of a product model. It lists six Comparator statements, among them [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/HyperinvariantSubspaces.lean HyperinvariantSubspaces.lean] and [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/IrrationalRotation.lean IrrationalRotation.lean].
* '''Catalogue status.''' The Justin Sun Prize record on GitHub lists the problem as entry [https://github.com/TheJustinSunPrize/awards/blob/8c0c64518e775cbcff22cf59580e4cfbb01b30a6/problems/catalog-1001-1022.md#JSP-001069 JSP-001069], with status "Solved", Lean proof "reported complete for the stated scope", and eligibility "Pending verification". Google DeepMind's Formal Conjectures project records the ordinary invariant subspace problem for Hilbert space as research open in [https://github.com/google-deepmind/formal-conjectures/blob/32ac619d83ac8943c968142436f782525d75a49f/FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean FormalConjectures/Wikipedia/InvariantSubspaceProblem.lean], checked 18 October 2026 at commit <code>32ac619</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub, review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates the family "full": both summary claims are stated in Lean, the hyperinvariant theorem for every separable infinite-dimensional complex Hilbert space and the invariant-projection counterexamples. It notes that "hyperfinite" is only implicit, since one statement asserts a II1 factor with separable predual and the rotation algebra is hyperfinite by construction. It records sandboxed Comparator passes for all six challenges. || MathVet states that its ratings concern whether the Lean states the headline claims.
|-
| 2026-10-08 || Formal Conjectures [https://github.com/google-deepmind/formal-conjectures/pull/7000 pull request 7000] (anxkhn) || Formal statement || Adds <code>FormalConjectures/Paper/HyperinvariantSubspaces.lean</code> with Corollary 1.2 of the hyperinvariant manuscript at commit <code>adc7f12</code>, omitting the commutant-algebra assertions. The pull request states that the external proof was not built locally and adds no formal-proof attribute. || Pull request open, not merged, as of 18 October 2026.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/7b51dc1b8aa94f584beeea43850a300d345c2ccf/corpus/openai-math/kernel-runs/38019899278/HyperinvariantSubspaces.json cert-machine], openai/math lane K, runs 38017370880, 38019899278 and 38051470892 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept all six challenges of the family, among them <code>HyperinvariantSubspaces</code> in 630 seconds and <code>IrrationalRotation</code> in 1454 seconds. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions lists none of the six challenges of this family, so they were accepted by con-leche and by Lean's official kernel. || Development journal.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The hyperinvariant subspace problem - Revision history

Aftermath bot: New page for the OpenAI hyperinvariant subspace and invariant projection counterexamples with background, Lean scope and four public rows