AI activity

How much of what each announcement claims can be inspected. Of 118 results announced, 100 have not been identified.

Advisory Group on Mathematics and Artificial Intelligence

OpenAI·21 Sep 2026·claims more than 100 long-standing open problems across most areas of mathematics·Source

0 of 100 identified; 0 with a checkable artifact. Announced with an independent advisory group to advise on how the results should be released. None of the problems has been named.

D0 withheld

On the Navier–Stokes Millennium Prize Problem

OpenAI·8 Sep 2026·claims Navier–Stokes blowup with smooth forcing, and unforced Euler blowup·Source

2 of 2 identified; 2 with a checkable artifact. Both results carry a paper and a Lean formalisation checked with Comparator.

Held here: Existence and Smoothness of the Navier–Stokes Equation

D3 checkable

Finite-time blowup with smooth forcing for porous media, Boussinesq and Euler

Tristan Buckmaster and Levent Alpöge·7 Sep 2026·claims three blowup results with smooth forcing, and blowup for hypodissipative Navier–Stokes held back until its Lean verification finishes·Source

4 of 4 identified; 0 with a checkable artifact. Three papers are public. The authors say the results were verified in Lean but cite no public repository, and the fourth result has no write-up yet.

Held here: Finite-time blowup for the 3D incompressible Euler equations with smooth forcing, Finite-time blowup for the inviscid Boussinesq equations with smooth forcing, Finite-time blowup for the incompressible porous media equation with smooth forcing

D1 named

Formalizing Fermat's Last Theorem

Anthropic·4 Sep 2026·claims a complete formalisation of Fermat's Last Theorem·Source

1 of 1 identified; 1 with a checkable artifact. The repository publishes the development, a Comparator challenge and a formalization.yaml.

Held here: Fermat's Last Theorem

D3 checkable

Learning more about Claude's mathematical capabilities

Anthropic·10 Aug 2026·claims a higher proven proportion of zeta zeros on the critical line·Source

1 of 1 identified; 1 with a checkable artifact. A paper on arXiv and a Lean formalisation, rebuilt here.

Held here: Proportion of zeta zeros proved to lie on the critical line (checked by qed.bot)

D3 checkable

Ten advances on open problems

OpenAI·1 Aug 2026·claims ten advances on open problems in mathematics and theoretical computer science·Source

10 of 10 identified; 10 with a checkable artifact. Each result is published with a Lean certificate. Two attach to Erdős problems held here, and both were rebuilt here.

Held here: Erdős Problem 146 (checked by qed.bot), Erdős Problem 183 (checked by qed.bot)

D3 checkable

How to read a grade

Autonomy: who did the work?

A?: Not established. Declared by whoever submitted the work and not verifiable from the record.
A3: Autonomous. The system produced the result without significant human mathematical involvement.
A2: Directed. The system produced the result while building on literature or framing supplied to it.
A1: Collaborative. A human and a system worked the problem together, or the system played a supporting role.
A0: Human. No machine contribution to the mathematics.

Evidence: was it checked?

V3: Machine-checked. The artifact was rebuilt at a pinned commit by someone other than its authors — qed.bot, or a registry that publishes the check — and it holds: a proof that elaborates on the standard axioms alone, or an object that meets the problem's own constraints.
V2: Artifact reported. A proof or a constructed object is published, but nobody independent of its authors has rebuilt it.
V1: Informal. A public write-up exists and has had community scrutiny.
V0: Claimed. No public artifact, or the claim is marked unverified at source.

Fidelity: does the statement match?

F3: Anchored. The proof is checked for exact statement identity against a statement written independently of it, held here from a separate statement corpus.
F2: Declared. The authors record how the formal statement corresponds to the claim — a comparator challenge, an alignment table or written divergences — or a statement corpus cites the proof against its own statement.
F1: Unaudited. A formal artifact exists, but nothing records that its statement says what the claim says.
F0: Absent. No formal statement is attached to the result.

Browse claims

Announcements and disclosure

How to read a grade