Beyond OpenAI’s catalogue
Claims outside OpenAI’s math catalogue: one-off announcements by OpenAI and results from other labs (Axiom Math, PSI (Physical Superintelligence), Anthropic), with the same four-step record. They are kept out of the catalogue counts and added by hand from each lab’s announcements and repositories.
Two large Lean formalizations, side by side
| AX01 | AN01 | |
|---|---|---|
| Theorem | Classification of finite simple groups | Fermat’s Last Theorem |
| Lines of Lean | about 43.1 million (Axiom’s post) | about 13 million (Anthropic’s post; our sample estimate 13 to 15 million) |
| Time taken | 24 days (Axiom’s post) | 11 days, August 7 to 17 (the post also says “a little under two weeks”) |
| Errata and outside checks | 34 noteworthy deviations from the published record, described in Axiom’s post; the errata list itself is not yet published | Kevin Buzzard compiled it and ran comparator: “it checks out” (his blog, September 4) |
| Review status in the metadata | “self-assessed” | “self-assessed” |
| Announced | October 26, 2026 | September 4, 2026 |
Special S01 · OpenAI, outside its catalogue · announced September 8, 2026 · Mathematical physics
Finite-time blowup for Navier–Stokes and Euler
Two papers and Lean proofs claim Navier–Stokes breakdown alternatives (C) and (D), with a smooth force, and blowup for the unforced Euler equations.
- Posted as a preprint
- OpenAI, September 8, 2026: two PDFs (166 and 57 pages)
- Under expert review
- None named in the repository or the papers
- Peer reviewed
- Not yet
- Checked in Lean
- OpenAI published Lean 4 proofs of the main theorems, with Comparator challenges (repository)
AN01 · Anthropic · announced September 4, 2026 · Number theory
Fermat’s Last Theorem, formalized in Lean
Anthropic’s Lean proof of Fermat’s Last Theorem, written by Claude agents in 11 days: about 13 million lines, following Darmon, Diamond and Taylor.
- Posted as a preprint
- Anthropic’s post and the repository anthropics/fermats-last-theorem, September 4, 2026
- Under expert review
- Kevin Buzzard, outside check of the Lean code (Kevin Buzzard’s blog, September 4, 2026)
- Peer reviewed
- Not yet
- Checked in Lean
- Anthropic’s Lean proof of the claim itself: three standard axioms, checked with comparator and a second kernel, as its README reports; not built or run by us (repository)
AX01 · Axiom Math · announced October 26, 2026 · Group theory
The classification of finite simple groups, formalized in Lean
Axiom Math’s Lean formalization of the classification of finite simple groups, about 43.1 million lines in 24 days, with a new written proof of the Unbalanced Group Theorem.
- Posted as a preprint
- Axiom’s blog post, October 26, 2026; repository AxiomMath/CFSG (first commit October 27, UTC); “The Unbalanced Group Theorem” on Hexagon, version 1, October 27
- Under expert review
- None independent in our sources; Axiom names Richard Lyons, Dan Nakano and Ronald Solomon as external advisors, and its metadata calls the review “self-assessed”
- Peer reviewed
- Not yet
- Checked in Lean
- Axiom’s Lean proof of the claim itself: sorry-free, three standard axioms, per its README; not built or run by us (repository)
PSI01 · PSI · announced October 23, 2026 · Mathematical physics
Three copies of the Werner state: the sharp curve in dimensions three and four and a bound in every dimension
Open Quantum Problems 2: Undistillability implies PPT? By Ian MacCormack, Ning Bao.
- Posted as a preprint
- PSI GitHub repository, released October 23, 2026
- Under expert review
- None independent. Co-author Ning Bao reviewed and edited as a paid contractor to PSI; the paper thanks an unnamed referee for a report on an earlier version, which the first author obtained.
- Peer reviewed
- Not yet
- Checked in Lean
- Qutrit case only: Theorems 1.1 and 1.2 at d = 3 (endpoint from PSI's own exact certificate), Proposition 4.2(a), Corollary 5.3 for k = 3; 48 Comparator statements. Theorem 1.3 (37/80) is not formalized. Not run by us. (repository)
PSI02 · PSI · announced October 23, 2026 · Mathematical physics
The vacuum Bell correlation of the massive free scalar field attains the classical bound for bounded regions beyond a finite separation
Open Quantum Problems 12: Bell inequalities for long range vacuum correlations By David Turturean.
- Posted as a preprint
- PSI GitHub repository, released October 23, 2026
- Under expert review
- None independent. Ning Bao (not an author) wrote a referee report on an earlier draft as a paid contractor to PSI.
- Peer reviewed
- Not yet
- Checked in Lean
- Theorem 1.1 and Corollary 1.2 of the full manuscript as stated, the CHSH form, a direction-uniform version, vacuum existence and noncommutativity; 6 Comparator statements. Not run by us. (repository)
PSI03 · PSI · announced October 23, 2026 · Mathematical physics
The optimal CGLMP measurements on maximally entangled states
Open Quantum Problems 27: The power of CGLMP inequalities By David Turturean, Ning Bao.
- Posted as a preprint
- PSI GitHub repository, released October 23, 2026
- Under expert review
- None independent. The paper thanks Ian MacCormack (PSI) for reviewing earlier drafts and Jim Halverson for coordinating the review (reviewers not named); co-author Ning Bao commented as a paid contractor to PSI.
- Peer reviewed
- Not yet
- Checked in Lean
- Projective bound and equality case (Theorems 1 and 3), attainment, witness tolerance; also statements not claimed by the current paper (tensor-CHSH noise and statistical-strength comparisons at d = 2^m, m ≥ 955 and m ≥ 41; Part A facet statements), from an earlier manuscript; 16 Comparator statements. Not run by us. (repository)
PSI04 · PSI · announced October 23, 2026 · Mathematical physics
Entanglement Breaking after 2(d−1) PPT Maps
Open Quantum Problems 38: The PPT squared conjecture By David Turturean, Ning Bao.
- Posted as a preprint
- PSI GitHub repository, released October 23, 2026
- Under expert review
- None independent. The paper thanks Adam Levine for reviewing an earlier draft of the proof and Jim Halverson for coordinating the expert review (reviewers not named); co-author Ning Bao verified the result as a paid contractor to PSI.
- Peer reviewed
- Not yet
- Checked in Lean
- Theorem 1 (both sentences), N ≥ 2(d − 1) maps, and an interleaved version; 13 Comparator statements. Not run by us. (repository)
PSI05 · PSI · announced October 23, 2026 · Mathematical physics
An extensibly causal quantum process with no purification
Open Quantum Problems 43: Are all extensibly causal processes purifiable? By David Turturean, Ning Bao.
- Posted as a preprint
- PSI GitHub repository, released October 23, 2026
- Under expert review
- None independent. Co-author Ning Bao wrote a referee report (including improvements suggested by an AI review) as a paid contractor to PSI; the paper thanks Jim Halverson for coordinating the expert review (reviewers not named).
- Peer reviewed
- Not yet
- Checked in Lean
- The counterexample, its Pauli form, the dimension dichotomy, purifiable ⇒ causally separable, ordered ⇒ purifiable and more; 11 Comparator statements. Not run by us. (repository)
AX02 · Axiom Math · announced October 12, 2026 · Number theory
No zeros past 31/32 for the Dedekind zeta function of every number field
Dean Cureton and Jesse Thorner, with AxiomProver, claim a zero-free half-plane Re s > 31/32 for every Dedekind zeta function, building on OpenAI’s results 003 and 029.
- Posted as a preprint
- Hexagon 2610.00200: version 1 October 12, 2026; version 2 October 14 (“A mix of human-written and AI-generated”)
- Under expert review
- None named in our sources (the paper thanks Ken Ono for his helpful comments)
- Peer reviewed
- Not yet
- Checked in Lean
- Axiom’s Lean proof: README says only Lean’s three standard axioms; metadata review “agent-reviewed”; not built or run by us (repository)
AX03 · Axiom Math · announced September 17, 2026 · Combinatorics
The Huang–Jiang–Oblomkov conjecture: Rogers–Ramanujan identities from X^a = Y^b
Yifeng Huang, Kenny Lau and Ken Ono prove the Huang–Jiang–Oblomkov conjecture for every coprime pair 1 < a < b, with a Lean proof by Axiom.
- Posted as a preprint
- arXiv 2609.20567: version 1 September 17, 2026; version 2 October 7
- Under expert review
- None named in our sources
- Peer reviewed
- Not yet
- Checked in Lean
- Axiom’s Lean proof (with AxiomProver): the README says the comparator run on October 7, 2026 reported “Your solution is okay!”; not built or run by us (repository)
AX04 · Axiom Math · announced October 14, 2026 · Number theory
Explicit positive lower density for the Collatz conjecture
Kenny Lau, with AxiomProver, makes Lech Mazur’s positive-proportion theorem explicit, with the constant 2^2^2^163. Not a proof of the Collatz conjecture.
- Posted as a preprint
- Hexagon 2610.00249: version 1 October 14, 2026; version 2 October 21 (“A mix of human-written and AI-generated”)
- Under expert review
- None named in our sources
- Peer reviewed
- Not yet
- Checked in Lean
- Axiom’s Lean proof: scope Theorem 1.3, Remark 1.4 and Corollary 1.2, no sorry, only Lean’s three standard axioms, review “author-verified”; not built or run by us (repository)
AN02 · Anthropic · announced August 10, 2026 · Number theory
More than two thirds of the zeta zeros are simple and on the critical line
A result first found by Claude and written up by Levent Alpöge and Ralph Furman of Anthropic, proved again by Youness Lamzouri, with Lean by Anthropic and by Axiom.
- Posted as a preprint
- arXiv 2608.13637 (Alpöge and Furman, August 13, 2026; v2 August 19) and 2609.02882 (Lamzouri, September 2; v2 September 8); Anthropic’s post, August 10
- Under expert review
- None named in our sources; the proof was checked by its listed authors at Anthropic, and Brian Conrey and Daniel Goldston are thanked for reading the manuscript
- Peer reviewed
- Not yet
- Checked in Lean
- Lean by Anthropic (the Alpöge–Furman paper, 17 comparator statements) and by Axiom (Lamzouri’s proof, 12 statements); both report the comparator; not built or run by us (repository)
Last checked October 27, 2026.