Browse › Operator algebras › 292 Kirchberg's $\mathcal O_2$ norm-ultrapower embedding problem
An explicit obstruction to nuclear norm-ultrapower embeddings
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We give a negative answer to Kirchberg's norm-ultrapower embedding problem. We construct an explicit separable unital full group C∗-algebra that admits no unital embedding into Bω, for any nonzero unital nuclear C∗-algebra B and any free ultrafilter ω on ℕ. In particular, it does not embed unitally into $\mathcal O_2^\omega$.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, Kirchberg's $\mathcal O_2$ norm-ultrapower embedding problem: Lean scope notes (lean/docs/292.md, OpenAI Math Release, 2026-10-06). The release reports a formalization of the explicit full group $C^*$-algebra obstruction for every nonzero unital nuclear target and every free ultrafilter on $\mathbb N$, including the $\mathcal O_2$ case. [family-level]
- OpenAI math release, NuclearUltrapower.lean comparator statement (lean/ComparatorChallenges/NuclearUltrapower.lean, release of 2026-10-06). The Lean statement
main_no_embeddingof the headline claim, including the Cuntz-algebra corollary; the proof lives in a separate solution module. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Isaac Goldbring, Model theory and Ultrapower Embedding Problems in Operator Algebras (arXiv:2210.01223, 2022). This survey covers the model-theoretic approach to ultrapower embedding problems, including KEP and its existential-closure reformulation, which the paper's corollary on consequences of a negative KEP relies on.
- Isaac Goldbring and Bradd Hart, Operator algebras with hyperarithmetic theory (arXiv:2004.02299, 2020). Its result that $\mathcal O_2$ has a hyperarithmetic theory is conditional on a positive answer to KEP, the hypothesis the paper's Theorem 1.1 claims to refute.
- Isaac Goldbring and Bradd Hart, A quantum complexity approach to the Kirchberg Embedding Problem (arXiv:2107.14010, 2021; v2 marked withdrawn). It derives consequences of a positive answer to KEP, in the same line of conditional approaches as Fox–Goldbring–Hart discussed in the paper's "Previous work" paragraph.
Digests and expositions
- Open Mathematics Courses, Kirchberg's embedding problem (online course, undated). Three lessons explain the paper's spectral test, nuclear finiteness argument and predecessor-chain contradiction, with property (T) of $\mathbb Z^3\rtimes\mathrm{SL}_3(\mathbb Z)$ and nuclearity of $\mathcal O_2$ taken as named hypotheses; the course states that independent review is incomplete. [AI-generated per source]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 292
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026,
author = {{OpenAI}},
title = {{An explicit obstruction to nuclear norm-ultrapower embeddings}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026/paper.pdf}{OAI:An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/292.md. The Lean statements have not been checked by people against the paper's claims.
Family 292: Kirchberg's $\mathcal O_2$ norm-ultrapower embedding problem
Constructs an explicit separable unital full group C∗-algebra that cannot embed unitally into the norm ultrapower of any fixed nonzero unital nuclear C∗-algebra, for any free ultrafilter on the natural numbers. Taking the target to be $\mathcal O_2$ answers Kirchberg's norm-ultrapower embedding problem negatively.
This is the only paper in this family.