Research library
Formal verification
Area: definition. Apply the shared measurement protocol.
Estimated progress toward AI-managed mathematics
45% complete — judgment-based estimate as of November 7, 2026. Confidence: low. This uses the requested scale: 0% is the pre-2022 starting point; 100% means AI manages continuing mathematical progress without human involvement. It is not a measured fraction of all mathematics, a benchmark score, or a forecast of time remaining.
The shared mathematics scoring rubric assigns up to 20 points each for execution, breadth, agenda-setting, validation, and sustained autonomous improvement. This outcome's points are 15 + 10 + 5 + 10 + 5 = 45/100, in that order. Unknown evidence earns no demonstrated-progress credit in the affected component; that does not prove the capability is absent.
Reason for the estimate: Large Lean formalizations show substantial execution capability. Artifact coverage is incomplete, and humans still choose statements, check meaning, review axiom use and supervise difficult formalization. Independent clean-rebuild coverage is unknown. Evidence and dated sources are in the baseline below.
What would move the score: Raise the estimate when a frozen cohort consistently produces faithful formal statements, reproducible builds and automated independent audits without human correction. Reassess downward if replication fails or previously hidden human assistance emerges.
Measurement and acceptance rule
Percentage of claimed completed proofs with a reproducible Lean project, pinned Lean and mathlib versions, and an independent clean rebuild and proof audit.
Evidence requirements
Every result counted as a verified new proof must include a human-readable statement and argument, complete Lean source, dependency versions, build instructions, and reviewer reports. A mathematician must confirm that the formal statement matches the intended theorem and does not introduce stronger assumptions that trivialize it.
Audit transitive axiom dependencies, including #print axioms for the principal results. Reject sorryAx, admitted obligations, custom unproved assumptions used to assume the conclusion, and verification bypasses. Record the permitted foundational axioms; use independent proof rechecking appropriate to the threat model. The Lean validation guidance explains why editor check marks alone are insufficient. Lean verifies formal derivation, while human review establishes meaning, novelty, and significance.
Related milestones
See the area's proposed milestones. Proposed targets are distinct from the dated evidence below.
Baseline as of November 7 2026
Status: large public Lean artifacts and verification protocols exist; the requested independently audited coverage percentage is not established. Sources accessed November 7, 2026. No Lean project was compiled or independently audited during this documentary review.
Dated findings
| Evidence date | Finding | Verification level |
|---|---|---|
| September 4, 2026 | Anthropic reports an end-to-end Lean formalization of Fermat's Last Theorem, using the three standard axioms and a Comparator match to Mathlib's statement. Kevin Buzzard is quoted as reviewing it. | Developer report with named external review and public repository; this formalizes known mathematics. Technical report. |
| October 7, 2026 version history | OpenAI records 300/719 top-line results formalized, approximately 41.72%. | Historical artifact-coverage figure, not a percentage independently re-audited here. Later entries record additional formalizations and configuration fixes, so retain the date and denominator. Release history. |
| November 7, 2026 repository observation | OpenAI's README still describes approximately 42% formalization coverage. | Rounded provider summary; do not multiply it by the current catalogue size to invent an exact count. Repository. |
| October 29, 2026 ledger update | Epoch's Erdős evaluation requires Comparator to check identical statements, permitted axioms, and Lean-kernel replay in an isolated environment. | Benchmark evaluator's validation protocol, stronger than a bare compilation claim. Methodology. |
Interpretation and tracking value
Maintain two distinct series: published formal-artifact coverage and independently audited coverage under this project's rule. The former has a dated 300/719 observation for one collection; the latter is unknown. Public repositories and successful compilation do not automatically establish clean rebuilds, semantic correspondence, or novelty.
Fermat's Last Theorem is a demonstration of formalization scale, not a newly discovered theorem. Do not count its intermediate lemmas as independently novel discoveries.
Next comparable measurement
Choose a frozen collection and commit. For every claimed completed proof, record whether source, pinned dependencies, reproducible build, axiom audit, statement review, and independent evaluator signoff are present. Report the numerator passing every check over all claims in that collection, with failure reasons. Retain original releases and corrections so verification coverage can be reconstructed over time.