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 II1 factor. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above. Read the assessments
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
For every irrational \theta\in(0,1) there exists a continuous function f:\T\to[0,1] such that
and every projection p\in R_\theta satisfying (1-p)Uf(V)p=0 is either 0 or 1.
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.
Every separable infinite-dimensional complex Hilbert space carries a nonzero norm-quasinilpotent operator with no nontrivial hyperinvariant subspace. Its commutant is a proper strongly closed transitive unital algebra.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
BackwardIntertwinersThe paper states
In Backward intertwiners and a transitive commutant, 27 September 2026
Every infinite-dimensional separable complex Hilbert space admits 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.
The words they share: dimensional, hyperinvariant, commutant, transitive, complex, space, separable, closed, algebra, norm, operator, infinite, hilbert, proper, subspace, quasinilpotent, nonzero.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
BackwardIntertwiners.lean, the release lists it as a main result.
theorem direct_algebra_corollary (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [TopologicalSpace.SeparableSpace H] (hInf : ¬FiniteDimensional ℂ H) : Hyperinvariant233.FullClaim (H:=H) := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
ContinuousCircleWeightThe paper states
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
For every irrational \theta\in(0,1) there exists a continuous function f:\T\to[0,1] such that
and every projection p\in R_\theta satisfying (1-p)Uf(V)p=0 is either 0 or 1.
The words they share: irrational, log, function, projection, rotation, continuous.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
ContinuousCircleWeight.lean, the release lists it as a supporting statement.
def MainStatement : Prop := ∃ (θ : ℝ) (f : C(CircleX, ℝ)) (U V : unitary Operator) (e : TracialHilbert), 0 < θ ∧ θ < 1 ∧ Irrational θ ∧ IsTracialRotation θ U V e ∧ (∀ x, 0 ≤ f x ∧ f x ≤ 1) ∧ (∃ z : CircleX, ∀ x, f x = 0 ↔ x = z) ∧ (∫⁻ x, negativeLog (f x) ∂(volume : Measure CircleX)) = ∞ ∧ ∀ p : Operator, p ∈ rotationAlgebra U V → IsStarProjection p → (1 - p) * weightedRotation U V f * p = 0 → p = 0 ∨ p = 1theorem main_theorem : MainStatement := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
FiniteFactorThe paper states
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
There are angles 0<\theta_i<1 and costs c_i>0, with \sum_i\theta_i<\infty and 1,\theta_1,\theta_2,\ldots rationally independent, such that the measurable weight
is positive almost everywhere and has \int_X\log f\,d\mu=-\infty. The algebra M is a type \mathrm{II}_1 factor with separable predual, and T=U\pi(f) is nonzero and norm-quasinilpotent, with \Delta(T)=0. Every projection p\in M satisfying (1-p)Tp=0 is 0 or 1.
Moreover, |T| has pure-point spectral type. The abelian algebra generated by any finite family of polar conjugates U^n|T|U^{-n} is atomic, whereas W^*(U^n|T|U^{-n}:n\in\Z) is diffuse.
The words they share: conjugates, predual, factor, product, separable, finite, algebra, nonzero, projection, norm, delta, realization, measurable.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
FiniteFactor.lean, the release lists it as a supporting statement.
theorem main_theorem : MainTarget.{0} := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
HyperinvariantSubspacesThe paper states
In Backward intertwiners and a transitive commutant, 27 September 2026
Every infinite-dimensional separable complex Hilbert space admits 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.
The words they share: dimensional, commutant, transitive, complex, space, closed, operator, infinite, hilbert, hyperinvariant, proper, unital, separable, subspace, quasinilpotent, algebra, bounded, nonzero.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
HyperinvariantSubspaces.lean, the release lists it as a supporting statement.
theorem main_theorem (hInf : ¬FiniteDimensional ℂ H) : FullClaim (H := H) := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
IrrationalRotationThe paper states
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
There are angles 0<\theta_i<1 and costs c_i>0, with \sum_i\theta_i<\infty and 1,\theta_1,\theta_2,\ldots rationally independent, such that the measurable weight
is positive almost everywhere and has \int_X\log f\,d\mu=-\infty. The algebra M is a type \mathrm{II}_1 factor with separable predual, and T=U\pi(f) is nonzero and norm-quasinilpotent, with \Delta(T)=0. Every projection p\in M satisfying (1-p)Tp=0 is 0 or 1.
Moreover, |T| has pure-point spectral type. The abelian algebra generated by any finite family of polar conjugates U^n|T|U^{-n} is atomic, whereas W^*(U^n|T|U^{-n}:n\in\Z) is diffuse.
The words they share: rationally, conjugates, predual, factor, ii, costs, independent, atomic, log, polar, diffuse, spectral, weight, abelian, product, generated, angles, realization, separable, pi, positive, exp, measurable, finite, quasinilpotent, algebra, projection, norm, delta, tp, nonzero, theta.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
IrrationalRotation.lean, the release lists it as a supporting statement.
theorem prescribed_irrational_counterexample (θ : ℝ) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hθ : Irrational θ) : ∃ f : C(Circle, ℝ), Rotation.IsContinuousCounterexample θ f := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
The file states one more theorem: product_.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
ProductBrownThe paper states
No paper theorem is paired with this Lean statement.
no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.
Statements it shares words with:
The Lean statement
No paper theorem is paired with it.
ProductBrown.lean, the release lists it as a supporting statement.
def ProductBrownClaim : Prop := ∀ (θ : SourceCoordinate → ℝ) (hθ : SourceAngles θ), IsBrownMeasure sourceVacuumFunctional (sourceOperator θ sourceLogWeight hθ.nonneg sourceLogWeight_nonneg) (Measure.dirac 0) theorem productBrown : ProductBrownClaim := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
IsBrownMeasure Model.lean, line 120ProductBrownClaim Model.lean, line 132HasScalarCenter Model.lean, line 14IsFiniteAlgebra Model.lean, line 18HasNoMinimalProjection Model.lean, line 22HasSeparablePredual Model.lean, line 27MainTarget Model.lean, line 32MainStatement Model.lean, line 40The source scan also found 45 theorem or lemma declarations whose names contain ‘manuscript’.
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note: Both summary claims are stated: Hyperinvariant.main_theorem (hInf : ¬FiniteDimensional ℂ H) (also BackwardIntertwiners.direct_algebra_corollary) for every separable infinite-dimensional complex Hilbert space: ∃ T ≠ 0, ‖T^n‖^(1/n) → 0 ∧ TransitiveCommutant T ∧ commutant T ≠ ⊤ ∧ SOT-closed commutant (no nonzero proper closed hyperinvariant subspace), and for the invariant-projection counterexamples FiniteFactor.main_theorem (a II₁ factor with separable predual and a nonzero quasinilpotent T ∈ M with (1 - p) T p = 0 → p = 0 ∨ p = 1), IrrationalRotation.prescribed_irrational_counterexample (every irrational θ: continuous weight f with Rotation.IsContinuousCounterexample θ f, T in the irrational-rotation algebra, nonzero, norm-quasinilpotent, trivial invariant projections) and ProductBrown (Brown measure δ₀). ‘Hyperfinite’ is only implicit (FiniteFactor asserts a II₁ factor with separable predual; the rotation algebra is the hyperfinite one by construction).
Definitions the group asks readers to compare with the paper: Hand-written operator-algebra notions: TransitiveCommutant T := ∀ K closed submodule, (∀ A commuting with T, A K ⊆ K) → K = ⊥ ∨ K = ⊤, HasOnlyTrivialInvariantProjections, NormQuasinilpotent, vectorFugledeKadisonDeterminant, IsVectorBrownMeasure, strongOperatorTopology, HasSeparablePredual M := ∃ separable Banach E, Nonempty (StrongDual ℂ E ≃ₗᵢ⋆[ℂ] M); quasinilpotence is via ‖T^n‖^(1/n) → 0 and ContinuousCircleWeight.MainStatement does not itself state quasinilpotence (only trivial invariant projections for a weight with log-integral -∞).
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).
“MATCHES”, in their words: The challenge statements state the headline as OpenAI wrote it.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
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.
Quasinilpotent operator with transitive commutant BackwardIntertwiners
Unreviewed AI draft: states a consequence of a paper’s theorem. States the backward-intertwiner paper’s corollary (a quasinilpotent operator with transitive commutant on every separable infinite-dimensional Hilbert space) rather than its direct-model theorem.
Continuous-weight invariant-projection counterexample ContinuousCircleWeight
Unreviewed AI draft: states a weaker form of a paper’s theorem. States the invariant-projection counterexample for some irrational angle, whereas the main theorem gives one for every irrational angle; the note calls it an earlier existence construction.
Finite-factor invariant-projection counterexample FiniteFactor
Unreviewed AI draft: states a weaker form of a paper’s theorem. States only that some II₁ factor with separable predual contains a nonzero quasinilpotent operator without nontrivial invariant projections, an existential form of the main theorem without its prescribed rotation and weight.
Quasinilpotent operator with a transitive commutant HyperinvariantSubspaces
Unreviewed AI draft: states a consequence of a paper’s theorem. States the corollary shared by both accompanying papers: every separable infinite-dimensional Hilbert space carries a nonzero quasinilpotent operator with a transitive, proper, strongly closed commutant, hence no nontrivial hyperinvariant subspace.
Invariant-projection counterexamples for every irrational rotation IrrationalRotation
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem for every irrational rotation angle (a continuous weight whose weighted rotation is nonzero, quasinilpotent and without nontrivial invariant projection), with the product realisation.
Brown measure of the selected product weighted shift ProductBrown
Unreviewed AI draft: states a supporting result. States that the Brown measure of the selected product weighted shift is the point mass at zero, a property of the paper’s product model rather than its main theorem.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
BackwardIntertwinersThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 165 s; peak memory 6.4 GiB). | 10 October 2026 | Original report |
ContinuousCircleWeightThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with Lean’s kernel: accepted (the check took 207 s; peak memory 6.5 GiB). | 11 October 2026 | Original report |
FiniteFactorTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
HyperinvariantSubspacesTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
IrrationalRotationTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
ProductBrownTwo reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
This family’s papers cite no paper elsewhere in the release.
No paper elsewhere in the release cites this family’s papers.
anxkhn, Series of 15 issues and 15 draft PRs adding release results to Formal Conjectures (issues 6972 to 6997, PRs 6977 to 7002), 8 October 2026. Source
Proposes adding the release’s quasinilpotent operator without a hyperinvariant subspace to Formal Conjectures (issue 6995, PR 7000).
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare one Lean statement with its paper: FiniteFactor, BackwardIntertwiners, ContinuousCircleWeight, HyperinvariantSubspaces, IrrationalRotation, ProductBrownSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a counterexample and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Author not stated. Source
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Corollary 1.4
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Corollary 1.2
In Backward intertwiners and a transitive commutant, 27 September 2026
Why this passage is shown
Theorem 1.1
In Backward intertwiners and a transitive commutant, 27 September 2026
Why this passage is shown
Proposition 2.3
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Proposition A.2 (Phase ranges)
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Theorem A.1 (Product realization)
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Proposition A.3 (Ordered orbit-pair sampling)
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Theorem 1.1
In Backward intertwiners and a transitive commutant, 27 September 2026
Why this passage is shown
Corollary 1.4
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Why this passage is shown
Corollary 1.2
In Backward intertwiners and a transitive commutant, 27 September 2026
Why this passage is shown
Theorem 1.1
In Invariant-projection counterexamples for every irrational rotation, 27 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, BackwardIntertwiners
Proof-verification report
MathVet, BackwardIntertwiners
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, BackwardIntertwiners
Proof-verification report
cert-machine, ContinuousCircleWeight
Proof-verification report
MathVet, ContinuousCircleWeight
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, ContinuousCircleWeight
Proof-verification report
cert-machine, FiniteFactor
Proof-verification report
MathVet, FiniteFactor
Proof-verification report
cert-machine, HyperinvariantSubspaces
Proof-verification report
MathVet, HyperinvariantSubspaces
Proof-verification report
cert-machine, IrrationalRotation
Proof-verification report
MathVet, IrrationalRotation
Proof-verification report
cert-machine, ProductBrown
Proof-verification report
MathVet, ProductBrown
Lean statement
BackwardIntertwiners
Lean statement
ContinuousCircleWeight
Lean statement
FiniteFactor
Lean statement
HyperinvariantSubspaces
Lean statement
IrrationalRotation
Lean statement
ProductBrown