Naimark's problem
From OpenAI Aftermath
Naimark's problem asks whether a C*-algebra all of whose nonzero irreducible representations are unitarily equivalent must be isomorphic to the algebra of compact operators on some Hilbert space. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026, claims a counterexample in ZFC, without additional set-theoretic assumptions; the collection's own summary presents it as an alternative to an earlier ZFC construction of Tanaka. The collection includes a Lean formalization of the theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Naimark's question dates to 1951; Rosenberg gave affirmative results, and an algebra whose unique irreducible representation acts on a separable Hilbert space is isomorphic to the compact operators (Calderón and Farah). Akemann and Weaver constructed a counterexample under Jensen's diamond principle and showed that the existence of a counterexample generated by ℵ1 elements is independent of ZFC.
- Calderón and Farah obtained a counterexample from a Cohen-forcing variant of diamond together with the continuum hypothesis, and Vaccaro constructed counterexamples under diamond with prescribed tracial state spaces.
- Tanaka (arXiv:2609.26930, 22 September 2026) gave a ZFC construction with a faithful tracial state, starting from the CAR algebra; the manuscript states that the existence conclusion of its theorem is already present there and that its own proof is an alternative.
The original result
- Claim. Theorem 1.1 of A counterexample to Naimark's problem in ZFC states that there exists a unital infinite-dimensional simple complex C*-algebra with a faithful tracial state all of whose nonzero irreducible representations are unitarily equivalent; in particular it is not isomorphic to the compact operators on any Hilbert space. No separability is assumed; the collection's summary describes the counterexample as nonseparable.
- Method, as described: the algebra is built by a transfinite iteration of length 𝔠+ that repeatedly joins two equivalence classes of pure states by adjoining a unitary through a selective bridge over a faithfully tracial algebra, using reduced HNN extensions, and controls the construction through unique state extension and countable determination of pure states.
- Source. The manuscript A counterexample to Naimark's problem in ZFC at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization gives a counterexample in ZFC: a unital infinite-dimensional simple complex C*-algebra with a faithful tracial state whose irreducible representations are all unitarily equivalent but which is not isomorphic to the compact operators on any Hilbert space, with no additional set-theoretic assumption. The Comparator statement is
Naimark.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the Lean statement asserts a unital infinite-dimensional simple C*-algebra with a faithful tracial state and a unique irreducible representation up to unitary equivalence that is not isomorphic to the compact operators on any Hilbert space; nonseparability is a consequence and is not stated. It notes that the representation theory used is written by hand. It records a sandboxed Comparator pass for Naimark. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38015544207 and run 38050007619 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the Naimark solution (3,335 s and 2,611 s); two intermediate runs record that the challenge was not run. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list Naimark, so the challenge was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-12 | Issue #1 in the GitHub repository punk01-shaka/hadwiger-nelson-audit | Critique (formalization setup) | The issue states that several of OpenAI's Comparator configurations declare fully written definitions as definition_names, so that Comparator checks only their names and types; it lists the Naimark configuration, with seven such definitions, among them, demonstrates accepted fake solutions for three other results, and states that this does not show any result to be wrong. |
Open issue; no fake solution is demonstrated for this family. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap, with no minor notes, and states that the reviewer read every section in full. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript; Tanaka's preprint precedes the manuscript and also gives a ZFC counterexample, which in addition has a faithful representation on a separable Hilbert space.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
