Kirchberg's embedding problem: does every separable C*-algebra embed in a norm ultrapower of the Cuntz algebra O2?
Kirchberg and Phillips proved that every separable unital exact C*-algebra embeds unitally into the Cuntz algebra . Kirchberg asked how far this universality extends beyond exact algebras once is replaced by its norm ultrapower . Goldbring and Sinclair (2015) named this Kirchberg's embedding problem and showed its equivalence with existential closedness statements; it is distinct from Connes' embedding problem and from the tensor-norm form of Kirchberg's QWEP conjecture. Does every separable unital C*-algebra admit a unital embedding into for a free ultrafilter on ?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Operator algebras; model theory of C*-algebras
- Posed by
- Eberhard Kirchberg, as recorded and named by Isaac Goldbring and Thomas Sinclair, On Kirchberg's embedding problem (J. Funct. Anal., 2015)
- Year posed
- 2015
- Years open
- 11y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 28 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: for with , the full group C*-algebra is separable and unital and has no unital embedding into for any nonzero unital nuclear and any free ultrafilter ; in particular none into . The obstruction combines property (T) of with a finiteness lemma for approximate representation types in nuclear algebras. Via Goldbring-Sinclair it follows that no exact or nuclear unital C*-algebra is existentially closed. It says nothing about Connes' embedding problem or the QWEP conjecture.
What the AI did
The release README says every result was produced by an unreleased internal OpenAI model with a fixed procedure of roughly three hours of ChatGPT Pro thinking compute per result. This family 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 manuscripts are authored 'OpenAI' and name no human author. The family is a single manuscript dated September 23, 2026.
Verification
No independent mathematician has checked this yet. Checked here: the introduction, Theorem 1.1 and the consequences section were read against the problem as Goldbring-Sinclair state it. The Lean challenge lean/ComparatorChallenges/NuclearUltrapower.lean (solution module OAI.Analysis.NuclearUltrapower.Main, which exists at the pinned commit) is not in the formalization catalogue; it was found through lean/docs/292.md. Its statement main_no_embedding was read: there is a separable full group C*-algebra of the explicit group (dyadic 3-vectors by SL3(Z) times Z) with no injective unital *-homomorphism into the norm ultrapower of any nonzero unital nuclear C*-algebra (nuclearity as min = max tensor norm) for any free ultrafilter, and in particular none into that of the universal Cuntz algebra on two isometries. That is the headline claim. Not rebuilt here.