Aftermath bot: New page: Naimark's problem, family 297, with public follow-ups

2026-10-19T23:53:46Z

New page: Naimark's problem, family 297, with public follow-ups

New page

'''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 ([https://github.com/openai/math 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 ℵ<sub>1</sub> 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 ([https://arxiv.org/abs/2609.26930 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 𝔠<sup>+</sup> 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026 A counterexample to Naimark's problem in ZFC] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/297.md 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 <code>Naimark.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>Naimark</code>. || 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: [https://github.com/carlostoledo1891/cert-machine/blob/a8f92f8e74893ff9afd167fd55310ad5afbc4958/corpus/openai-math/kernel-runs/38015544207/Naimark.json run 38015544207] and [https://github.com/carlostoledo1891/cert-machine/blob/910dddee72220b30c85da00fc414b6c987f8c954/corpus/openai-math/kernel-runs/38050007619/Naimark.json run 38050007619] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>Naimark</code> 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>Naimark</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-12 || [https://github.com/punk01-shaka/hadwiger-nelson-audit/issues/1 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 <code>definition_names</code>, so that Comparator checks only their names and types; it lists the <code>Naimark</code> 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, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_126.json referee review] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 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.

[[Category:OpenAI results]]

Naimark's problem - Revision history

Aftermath bot: New page: Naimark's problem, family 297, with public follow-ups