Operator algebras·OpenAI Math·Result 303·Lean formalisation listed
Weak pure infiniteness and Cuntz-algebra absorption
One of the 372 results in OpenAI's public mathematics catalogue, filed under operator algebras: 1 preprint, the latest dated 25 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and will embed the animation.
Latest paper
Weak pure infiniteness and O-infinity absorption
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
Resolves the ordinary-to-strong pure-infiniteness question of Kirchberg and Rørdam for complex C∗-algebras. For exact algebras, proper infiniteness of one fixed finite amplification of every positive element also suffices. Consequently, every separable nuclear algebra with this property absorbs 𝒪∞, without unitality or simplicity assumptions. (Lean)
Paper
Weak pure infiniteness and O-infinity absorption
We prove that every complex C∗-algebra in which each positive element is properly infinite is strongly purely infinite. This answers the ordinary-to-strong part of Kirchberg–Rørdam's comparison question. For exact algebras, we also prove that proper infiniteness of one fixed finite amplification of every positive element implies proper infiniteness of each positive element. Consequently, every separable nuclear algebra with this fixed-amplification property absorbs 𝒪∞, without assumptions of unitality or simplicity.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Operator algebras
- 285Counterexamples to Baum–Connes and Kadison–Kaplansky
- 286Rigidity and arithmetic of lattice von Neumann algebras
- 287Isomorphism of the free group factorsLean
- 288Kadison's similarity conjectureLean
- 289Strong Kadison–Kastler stability and its spatial boundariesLean
- 290Relative bicentralizers and modular spectral recoveryLean