Spectral isometry conjecture for C*-algebras: GPT-6 Astra proof, Lean
Event confirmedAwaiting review
Importance: major (4 of 5)The takeaway
Mathieu’s spectral isometry conjecture asks whether every unital surjective linear map between unital C*-algebras that preserves the spectral radius is a Jordan isomorphism. Only special classes were known. On 29 Oct Matthew Colbrook and George Stepaniants (Cambridge) posted what they call ‘a human digestion of a proof … found by GPT-6 Astra’. The theorem is registered in Lean on Palomar. Their AI declaration says the proof came ‘after a sequence of simple prompts’. This is the second such digest from Colbrook in a week, after Smale’s mean value conjecture. It is a preprint, not refereed.
Status
- Claim
Event confirmedAwaiting review
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 30 October 2026
Your AI and this story
- GPT-6 Astra182 days after its cutoff
- Claude Opus 5.5121 days after its cutoff
- Gemini 4 Argon212 days after its cutoff
- Grok 4.7151 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 121 days before it.
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-000031v1 (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 |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
- arXiv 2610.40470: Spectral isometries of unital C*-algebras (Colbrook, Stepaniants)arxiv.org, paper
- Palomar registry: A proof of the spectral isometry conjecture for C*-algebraspalomarregistry.org, code
Changes
- Filed (science agent; arXiv abstract and PDF read, AI declaration and Palomar reference quoted)