--- id: "2026-10-29-spectral-isometry-conjecture-c-star-algebras-gpt-6-astra" url: "https://postcutoff.com/e/2026-10-29-spectral-isometry-conjecture-c-star-algebras-gpt-6-astra/" as_of: "2026-10-30T13:42:00+01:00" date: "2026-10-29" date_precision: day category: science importance: 4 confidence: high status: [Event confirmed, Awaiting review] verification: Lean-verified sources: 2 editor: human editor human_review: null version: "2026-10-30" --- As of: 2026-10-30 13:42 CET. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-10-29-spectral-isometry-conjecture-c-star-algebras-gpt-6-astra/ # Spectral isometry conjecture for C*-algebras: GPT-6 Astra proof, Lean Full title: Spectral isometry conjecture for C*-algebras: proof 'found by GPT-6 Astra after a sequence of simple prompts', written up by Colbrook and Stepaniants, Palomar-registered Lean proof arXiv 2610.40470 (29 Oct 2026), "Spectral isometries of unital C*-algebras" by Matthew J. Colbrook and George Stepaniants, proves that every unital surjective complex-linear spectral isometry between unital C*-algebras is a Jordan isomorphism, and without unitality a central unitary multiple of one. This settles the spectral isometry conjecture (Mathieu–Schick 2002, Conjecture 4.6; Mathieu 2009, Problem 5). The proof was found by GPT-6 Astra; the authors studied it with ChatGPT 6 and wrote the paper. A Lean proof is on the Palomar registry (PALOMAR-2026-10-28-000031). ## Key facts - Theorem 1.1 (paper): if A, B are unital complex C*-algebras and T: A → B is surjective, complex-linear, T(1) = 1 and r_B(T(a)) = r_A(a) for all a, then T is a Jordan isomorphism (T(a²) = T(a)²). Without T(1) = 1, T is a central unitary multiple of a Jordan isomorphism - AI declaration (verbatim): 'The proof was found by GPT-6 Astra after a sequence of simple prompts. We then wrote the paper after discussing the proof further with ChatGPT 6 to understand the underlying mechanisms. After we wrote the paper ourselves, ChatGPT 6 was used for minor language editing of the penultimate draft in this stage only.' - Problem sources (paper): Mathieu and Schick, 'First results on spectrally bounded operators', Studia Math. 152 (2002), Conjecture 4.6; Mathieu, 'A collection of problems on spectrally bounded operators' (2009), Problem 5. It is the spectral analogue of Kadison's theorem that unital surjective isometries of C*-algebras are Jordan *-isomorphisms; the commutative case followed from Nagasawa's theorem - Method (abstract): show that a one-parameter group of unital spectral isometries consists of automorphisms, by passing to the bidual, which splits into finite and properly infinite parts; quadratic and cubic trace identities on the finite part - Formal proof: 'the result has been formally verified in Lean', reference PALOMAR-2026-10-28-000031 v1 (palomarregistry.org), registered 28 Oct - Pattern: Colbrook (with Tom Adamczewski) posted a human digest of GPT-6 Astra's disproof of Smale's mean value conjecture on 26 Oct (arXiv 2610.36158); Colbrook and Stepaniants earlier disproved the Schiffer and Pompeiu conjectures with AI help (Aug 2026) - Verification status: preprint plus Lean proof on Palomar; not refereed; no specialist reaction or HN thread found on 30 Oct ## What happened A linear map between C*-algebras is a spectral isometry if it preserves the spectral radius of every element. Kadison showed long ago that maps preserving the norm are Jordan *-isomorphisms. Mathieu and Schick conjectured in 2002 that spectral isometries are Jordan isomorphisms too. This was known for commutative algebras and other special classes. On 29 Oct Matthew Colbrook and George Stepaniants posted a proof for all unital C*-algebras. They describe the paper as a human digest of a proof GPT-6 Astra found "after a sequence of simple prompts". They say they studied the argument with ChatGPT 6 and then wrote the paper themselves. A Lean proof was registered on Palomar the day before. ## Why it matters The conjecture is a standard open problem on spectrum-preserving maps, listed in Mathieu's 2009 problem collection. With a Lean proof and named authors at Cambridge, it is one of the better-documented AI results of October. It follows the same "AI proof, human digest" format as Colbrook's Smale paper. ## What is disputed or not yet verified - Verification: Preprint; Lean proof registered on Palomar (PALOMAR-2026-10-28-000031); not refereed ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 182 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 121 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 212 days after its cutoff - Grok 4.7 (training cutoff May 2026): 151 days after its cutoff ## Sources 1. [arXiv 2610.40470: Spectral isometries of unital C*-algebras (Colbrook, Stepaniants)](https://arxiv.org/abs/2610.40470) (arxiv.org, paper) 2. [Palomar registry: A proof of the spectral isometry conjecture for C*-algebras](https://palomarregistry.org/entry?id=PALOMAR-2026-10-28-000031&version=1) (palomarregistry.org, code) ## Changes - 2026-10-30 (filed): Created (science agent; arXiv abstract and PDF read, AI declaration and Palomar reference quoted) ## Related - 2026-10-30: [AI-assisted results, 30 Oct: arXiv announcement of 29–30 Oct](https://postcutoff.com/e/2026-10-30-ai-assisted-results-october-30-listing/index.md) - 2026-09-03: [GPT-6 Astra autonomously disproves Smale's mean value conjecture in Lean](https://postcutoff.com/e/2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra/index.md) - 2026-08-18: [Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims](https://postcutoff.com/e/2026-08-18-palomar-lean-registry/index.md) - 2026-08-03: [Planar Schiffer and Pompeiu conjectures disproved by two independent groups](https://postcutoff.com/e/2026-08-03-schiffer-pompeiu-conjectures-disproved/index.md)