Browse › Operator algebras › 297 A ZFC counterexample to Naimark's problem
A counterexample to Naimark's problem in ZFC
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 construct in ZFC a unital infinite-dimensional simple complex C∗-algebra with a faithful tracial state whose nonzero irreducible representations are all unitarily equivalent. This gives a negative answer to Naimark's problem without additional set-theoretic assumptions.
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.
Comments and discussion
- Nik Weaver, Timothy Chow and commenters, How many of the results released by OpenAI went against the conventional mathematical wisdom? (MathOverflow, 2026-10-08–2026-10-10). Weaver identifies result 297 as contrary to his expectation that a positive answer might also be consistent with ZFC; in the comments, Chow relays Alex Meiburg's concern that the Lean statement does not establish provability in ZFC, and Weaver replies that, after looking at the manuscript, he does not think this is an issue.
Formalization
- OpenAI, A ZFC counterexample to Naimark's problem — Lean scope notes (lean/docs/297.md, OpenAI math release, 2026-10-06). The release's scope note describes a Lean formalization of a unital, infinite-dimensional, simple complex C*-algebra with a faithful tracial state and a unique nonzero irreducible representation up to unitary equivalence, not isomorphic to any algebra of compact operators, and links the Naimark Comparator statement. [AI-generated per source] [family-level]
- OpenAI math release, Naimark.lean comparator statement (lean/ComparatorChallenges/Naimark.lean, 2026). The comparator file linked from the scope note, which states the target theorem
mainwith simplicity, infinite-dimensionality, a faithful tracial state, unitary equivalence of irreducible representations and non-isomorphism to compact operators. [family-level] - Ryotaro Tanaka / MathlibAnnex, MathlibAnnex v0.4.0 (GitHub source release, 2026-09-20). A separate, earlier Lean 4/mathlib development (entry module
MathlibAnnex.Projects.Naimark) for Tanaka's CAR-based ZFC counterexample cited by the paper, reporting formal results on its irreducible representations, faithful separable representation, trace and density, plus a biconditional between CH and a counterexample of density aleph-one; it does not formalize this paper's reduced-HNN argument. [AI-generated per source] - Exact Mathematics with AI, Naimark's problem (MathlibAnnex companion project page) (project page, 2026). A reading guide to the formal declarations of the MathlibAnnex Naimark project, covering Tanaka's construction rather than the one in this paper. [AI-generated per source]
Related prior literature mentioned by others
- Ryotaro Tanaka, A separably representable counterexample to Naimark's problem in ZFC (arXiv:2609.26930v1, 2026-09-22). Highlighted in the AI Proved What? exposition and already cited by the manuscript, this earlier construction claims the same existence conclusion with additional faithful separable representability, unique trace and exact norm-density properties. [AI-generated per source]
Possibly relevant literature (found by the agent, not checked)
- R. Tanaka (publication responsibility), Naimark's problem, Exact Mathematics with AI: Brief Report, Draft R1 (September 21, 2026). An AI-assisted preliminary account of the ZFC construction in Tanaka2026, which the paper cites for the existence conclusion of its main theorem; the report states that human verification was incomplete. [AI-generated per source]
- R. Tanaka, Banach space theoretical construction of (primitive) spectra of C-algebras and the Naimark problem revisited* (arXiv:2504.05551, April 2025). Characterizes elementary C*-algebras among those with singleton spectrum and recalls Rosenberg's separable case, which relates to the paper's "History and scope" discussion.
Digests and expositions
- AI Proved What?, One irrep, not compact? (episode 297, October 2026). This AI-assisted video and transcript compare the paper with Tanaka's earlier construction and outline its selective joining of pure-state classes and countable-determination scheduling argument. [AI-generated per source]
- Gradient Damage, Kaplansky's Quasitrace Conjecture, Naimark's Problem and 7 More in Operator Algebras (video compilation, 2026-10-15). The chapter beginning at 1:45 introduces Naimark's problem and presents the release's claimed counterexample, with an explicit statement that the animations illustrate results rather than proofs.
News and blogs
- Carlos Toledo, OpenAI's math release: what it claims beyond what it checks (audit report, findings dated 2026-10-10). For the Naimark challenge at commit fd4aeeb2, the report identifies seven definitions whose bodies Comparator does not ordinarily compare, reports matching bodies and a successful Lean transfer check under additional checks, and lists the challenge as accepted by both Lean's kernel and nanoda.
Elsewhere
- Emergent Mind: family 297
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026,
author = {{OpenAI}},
title = {{A counterexample to Naimark's problem in ZFC}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026/naimark-counterexample-zfc.pdf}{OAI:A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/297.md. The Lean statements have not been checked by people against the paper's claims.
Family 297: A ZFC counterexample to Naimark's problem
Gives an alternative to Tanaka's ZFC construction of a unital infinite-dimensional simple complex C∗-algebra with a faithful tracial state and exactly one nonzero irreducible representation up to unitary equivalence. Thus the unrestricted compact-operator characterization fails without additional set-theoretic assumptions; the counterexample is nonseparable.
This is the only paper in this family.