On October 29, two mathematicians at the University of Cambridge posted a proof of a conjecture posed in 2002. Their abstract describes the paper as “a human digestion of a proof of the spectral isometry conjecture for C*-algebras found by GPT-6 Astra,” and their AI declaration says the model found the proof “after a sequence of simple prompts.”
The same day, a team led from Pacific Northwest National Laboratory posted a test on open conjectures picked at random. Given 200 of them, drawn from this year’s arXiv math papers, three GPT models proposed a proof or a counterexample for about 60%, at a median cost of 41 cents to $1.71 per attempt.
A question from 2002
The problem comes from operator algebras, the branch of mathematics that studies algebras of operators such as C*-algebras. Every element of such an algebra has a spectral radius, a single number: the largest absolute value in its spectrum. A spectral isometry is a linear map between two of these algebras that leaves every element’s spectral radius unchanged.
The conjecture asks whether keeping that one number for every element forces the map to preserve squares as well. It states that every spectral isometry that is surjective and sends the identity to the identity is a Jordan isomorphism: a bijection under which the image of a² is the square of the image of a.
Martin Mathieu and G. J. Schick of Queen’s University Belfast stated it as Conjecture 4.6 of “First results on spectrally bounded operators,” published in Studia Mathematica in 2002. Mathieu listed it again as Problem 5 in a collection of open problems posted in 2008. Partial results followed: the commutative case, properly infinite von Neumann algebras (Mathieu and Schick, 2003) and unital C*-algebras of real rank zero without tracial states (Mathieu, 2020).
The prompts, the write-up and the Lean check
Matthew J. Colbrook of Cambridge’s Department of Applied Mathematics and Theoretical Physics and George Stepaniants, of Cambridge and NYU’s Courant Institute, now prove it “for arbitrary unital C*-algebras” in a nine-page preprint. Their AI declaration opens: “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.” They add that ChatGPT 6 was used afterward only for minor language editing.
The paper says “the result has been formally verified in Lean,” the proof assistant that checks every logical step by computer. The formalization was posted on GitHub on October 28, under the Apache 2.0 license, with the statements in one file, the proofs in another, an axiom report and a comparator check in “paranoid” mode. Its automated Lean verification run completed successfully on October 28, according to the repository’s GitHub Actions log. We did not build the project ourselves.
The README states that “AI assistance was used for the Lean formalization, verification and review” and that it “was not used to write the manuscript.” The formal proof builds on Mathlib and on what the authors call “the OpenAI operator-algebra formalization.” Formal checking is also being applied at a much larger scale: on October 29 we reported that Axiom used AI agents to turn math’s 15,000-page proof into computer-checked code in 24 days.
200 conjectures picked at random
Single successes like Cambridge’s say little about how often such attempts work. Helen Jenne, Davis Brown, Jesse He and Henry Kvinge, of PNNL, the University of Pennsylvania, UC San Diego and the University of Washington, set out to measure the base rate. Their paper, “Beyond Selected Breakthroughs,” argues that “studying only the current set of major breakthroughs provides an incomplete picture.”
They built OpenConjecture, a dataset of conjectures from arXiv math papers published since February 2026, sampled 200 papers at random and drew one conjecture from each. GPT-5.6 Sol made the first attempt, with the full paper, web search and an instruction to “make a sustained attempt to prove or refute” the conjecture. Unresolved problems went to GPT-5.6 Sol Pro, then to GPT-6 Astra Pro, without web search. All runs used reasoning effort xhigh, and none got problem-specific guidance.
The models proposed counterexamples to 70 conjectures and proofs of 55, or 125 of the 200. The first pass produced 82 of those answers, the second 26 and the third 17, and by the third pass proofs outnumbered counterexamples. Median token use translated into about $0.97, $0.41 and $1.71 per attempt for the three passes, “at the time of writing.”
A fresh instance of the same model then reviewed each answer, and 84% passed. A model review classified about 60% of the surviving counterexamples from the first two passes as “off-the-shelf,” the kind a specialist would try first. Third-pass counterexamples “typically involved nontrivial modifications,” and the paper concludes that “some resolutions exhibit at least moderate novelty.”
The rest of the week on arXiv
The Ramanujan Challenge, organized by the Ramanujan Machine group at the Technion in Haifa, published its results the same day. The challenge ran from July to August 2026 with ten number theory problems: eight results the organizers had proved but not published, and two open conjectures.
Participants sent 228 submissions holding 4,802 pages of proofs and 1,079,380 lines of Lean, Python, Mathematica and Sage code. One open conjecture, an integral over the roots of a knot polynomial that expresses π², received a correct Lean-formalized proof and several other likely correct ones. The other remains open. The best natural-language proofs came from submissions using Claude and GPT models, and correct solvers included “a person with no higher mathematical education” whose solution to one problem was simpler than the organizers’ own.
In physics, Valentin Link of TU Berlin showed on October 27 that TEMPO, a method for simulating quantum systems that interact with their surroundings, can use a network whose internal size no longer grows with the system, “making large system sizes accessible.” His abstract states: “This structure was discovered by Claude Opus 5.5 during guided algorithm development.”
Earlier this month, on October 22, we reported that three teams had posted proofs of a 31-year-old geometry conjecture, all using AI, and on October 26 that six probability journals had paused new submissions, citing a surge driven largely by AI.
Limits the authors spell out
All three math papers are preprints, and none has been peer reviewed. The Cambridge result rests on the authors’ write-up and their Lean files, which were themselves produced with AI assistance.
The PNNL paper qualifies its own headline figure: its counts “should not be interpreted as rates of newly solved open problems.” No expert checked the 125 answers, and since each was reviewed by a new instance of the model that wrote it, “the solver and reviewer model may share mathematical errors.”
Some counterexamples take a conjecture literally and miss its intent: the trivial group offered against a number theory conjecture, or a single-vertex graph that the model itself labeled a “literal counterexample.” Several first-pass proofs covered conjectures already settled in later preprints, and only GPT models were tested, one run each. The Ramanujan organizers write that the solutions to their conjectures “have not yet been fully evaluated.”
What it means
In each of these papers, checking the results is the slow part. In the Cambridge case, GPT-6 Astra produced the argument after simple prompts, and the two authors spent their effort understanding it, writing it up and getting it through Lean. The Technion group names the same constraint: “as AI systems produce mathematical and scientific results faster than experts can verify them, validation is becoming a central bottleneck.”
The random sample answers the usual objection to such stories, that they are cherry-picked. On 200 conjectures nobody selected, the models proposed answers for most of them, at a median cost under two dollars per attempt. The study does not say how many of those answers are right or new, and its authors call for evaluations that also measure “fidelity to the intended statement, attribution, and the nature of the mathematical contribution.”
Three things will show how much of this holds: expert review of the 125 OpenConjecture answers, journal referees on the Cambridge proof and the Technion organizers’ evaluation of the conjecture solutions, which they promise “in the coming weeks.”
Sources
- Spectral isometries of unital C*-algebras, Matthew J. Colbrook and George Stepaniants, arXiv, October 29, 2026
- A proof of the spectral isometry conjecture for C*-algebras (Lean formalization), Matthew J. Colbrook and George Stepaniants, GitHub, October 28, 2026
- First results on spectrally bounded operators, M. Mathieu and G. J. Schick, Studia Mathematica, 2002
- A Collection of Problems on Spectrally Bounded Operators, Martin Mathieu, arXiv, October 15, 2008
- Beyond Selected Breakthroughs: Evaluating Language Models on Randomly Sampled Mathematical Conjectures, Helen Jenne, Davis Brown, Jesse He and Henry Kvinge, arXiv, October 29, 2026
- Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs, Alan Sorani et al., arXiv, October 29, 2026
- The TEMPO network can be made independent of the system size, Valentin Link, arXiv, October 27, 2026
Header image: chart by MACCUS, data from the OpenConjecture study (Jenne, Brown, He and Kvinge, arXiv:2610.40382, October 29, 2026)
