Show your work.
qed.bot records each claim that an AI system contributed to a mathematical problem, and grades it for who did the work, how it has been checked, and whether its formal statement says what was claimed.
The register holds 1,858 statements from 19 collections and 77 record targets, with 650 claims of AI contribution; 37 results have been machine-checked. How the grades work.
Contents
- Register
- Every problem, conjecture and theorem held, with its claims, formal statements and checks.
- Breaking
- New claims, announcements and changes, and what the monitors have seen since the last refresh.
- Formal record
- What formalisation projects declare about their proofs, and what independent rebuilds found.
- Discoveries
- Bounds and constructions, with the history of each record and who holds it.
- Activity
- Every graded claim of AI contribution, by system, grade and outcome.
- Millennium problems
- The seven Clay problems: their histories, what would count, and what has been claimed.
- Registries
- How other registries record the same work, and where they differ from this one.
- Systems
- Each AI system, with the record computed from its claims.
- Method
- How autonomy, evidence and fidelity are graded, and what each grade requires.