qedbot

Activity

AI activity

Every recorded contribution to a statement or record, graded for who did the work, whether it was checked, and whether the formal statement matches the claim.

257 claims on a statement 34 autonomous full claims 132 with a named collaborator 5 announcements ↓

Browse claims

Filters

Announcements and disclosure

5 announcements

An announcement is a claim about results. What matters is how much can be inspected. Of 114 results announced here, 100 have not been identified.

Advisory Group on Mathematics and Artificial Intelligence

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

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
Formalizing Fermat's Last Theorem

Anthropic·2026-09-04·claims a complete formalisation of Fermat's Last Theorem

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
Ten advances on open problems

OpenAI·2026-08-01·claims ten advances on open problems in mathematics and theoretical computer science

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 disclosure is graded
D3
Checkable. Every result announced is identified, and each carries a machine-checkable artifact.
D2
Written up. The results are identified and written up, but not all carry a machine-checkable artifact.
D1
Named. The results are identified but not written up.
D0
Withheld. Results are claimed without being identified.

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
None. No formal statement is attached to the result.