VibeMathedMath problems solved with AI
Sign in

Kirchberg-Rordam comparison question: pure infiniteness implies strong pure infiniteness, and weak equals strong for exact C*-algebras

Kirchberg and Rordam introduced three notions for (possibly nonsimple) C*-algebras: CC is purely infinite if every positive element hh is properly infinite (h⊕h≾hh\oplus h\precsim h in Cuntz comparison), weakly purely infinite if h⊕nh^{\oplus n} is properly infinite for every positive hh and one fixed nn, and strongly purely infinite if for all positive x,yx,y and ε>0\varepsilon>0 there are s,ts,t with ∥s∗x2s−x2∥<ε\|s^*x^2s-x^2\|<\varepsilon, ∥t∗y2t−y2∥<ε\|t^*y^2t-y^2\|<\varepsilon, ∥s∗xyt∥<ε\|s^*xyt\|<\varepsilon. Strong implies ordinary implies weak, and for separable nuclear algebras strong pure infiniteness is tied to O∞\mathcal O_\infty-absorption. Do the three notions coincide, in general and for nuclear algebras?

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
Operator algebras; C*-algebras, pure infiniteness
Posed by
Eberhard Kirchberg and Mikael Rordam (Adv. Math. 2002, Question 9.5); recorded as Problem LXXII by Schafhauser, Tikuisis and White
Year posed
2002
Years open
24y
Solved
2026-09-25
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
27 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: every complex C*-algebra in which every positive element is properly infinite is strongly purely infinite, with an arbitrary cross term in the diagonalization. Theorem 1.2: for exact algebras, proper infiniteness of h⊕nh^{\oplus n} for one fixed nn and all positive hh implies proper infiniteness of every positive element, hence strong pure infiniteness. Corollary: a separable nuclear algebra with this fixed-amplification property absorbs O∞\mathcal O_\infty, with no unitality or simplicity assumption (via Kirchberg's central-sequence results). Not settled: whether weak pure infiniteness implies pure infiniteness for non-exact algebras, which the paper states remains outside its conclusions.

What the AI did

The release README says all results were produced by an unreleased internal OpenAI model using one fixed procedure, about three hours of ChatGPT Pro thinking compute per result on average. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscript is authored 'OpenAI' and names no human author. Lean statements for both main theorems are among the release's Comparator challenges.

Verification

No independent mathematician has checked this yet. Checked here: the introduction and Theorems 1.1 and 1.2 were read against the question. lean/docs/303.md lists two challenges: IndividualStrongInfiniteness.json (OAI.MainGap.Manuscript.individual_to_strong_main, module OAI.Analysis.CStarAlgebra.PureInfiniteness.Main) and ExactInfiniteness.json (OAI.WeakPureInfiniteness.exact_weaklyPurelyInfinite_stronglyPurelyInfinite plus an individual proper-infiniteness variant, module OAI.Analysis.WeakInfiniteness.Main). Both solution files exist at the pinned commit; neither challenge is in the formalization catalogue formalization.yaml. The statements were read here: for a nonunital complex C*-algebra, every positive element properly infinite (Cuntz comparison in a stabilization built in the file) implies arbitrary-entry diagonalization and strong pure infiniteness; for exact algebras (exactness defined from scratch in the file) weak pure infiniteness implies strong. That is the headline. Not rebuilt here. The O-infinity absorption corollary rests on published Kirchberg results and is not formalized.

Sources

Changelog1 change

Discussion