Research library
Mathematics
View the four-date completion graphs and reconstruction notes.
Promise and evidence
AI could accelerate theorem discovery, proof construction, and verification, providing dependable foundations for science and software. FrontierMath supplies difficult problems authored by expert mathematicians. Benchmark success should be tracked separately from discovering previously unknown mathematics.
Apply the shared measurement protocol. All milestones here are proposed. Each linked measurable-outcome file now contains a dated evidence baseline as of November 7, 2026, separating published measurements, proxy observations, and measurements not yet established. Source publication and update dates are recorded separately from the review date. This was a documentary review, not an independent rebuild of the cited Lean proofs.
Progress scale
The following estimates use the requested endpoints: 0% represents the period before ChatGPT's public release in 2022; 100% represents mathematics whose continuing advancement is entirely managed by AI, without human participation in selecting problems, developing methods, proving results, validating meaning and novelty, or improving the research process. The 0% anchor is a project convention: AI and automated theorem proving existed before 2022.
These are subjective assessments of demonstrated progress, rounded to five-point increments, not scientific measurements of distance to a singularity. Confidence is low for every estimate. Percentage changes describe changes in this rubric, not equal increments of difficulty, elapsed time, or probability of reaching the endpoint. A high exam score alone cannot reach 100%.
Score each dimension from 0 to 20 in five-point steps: 0 = no demonstrated post-anchor autonomous progress in that dimension; 5 = isolated or heavily supported demonstrations; 10 = repeatable bounded performance with material human involvement; 15 = broad, mostly autonomous performance with remaining gaps; 20 = dependable autonomous performance throughout the relevant scope. Missing evidence receives no demonstrated-progress credit, rather than an invented empirical value.
| Dimension | Requirement for all 20 points |
|---|---|
| Execution | Reliably performs the outcome's mathematical work at research quality. |
| Breadth | Transfers across mathematical branches and genuinely unfamiliar problems. |
| Agenda-setting | Selects worthwhile questions and plans work without human direction. |
| Validation | Checks correctness, intended meaning and relevant novelty without human repair or adjudication. |
| Sustained autonomous improvement | Maintains and improves the process over repeated research cycles without human management. |
All five dimensions have equal weight; sum their points for the displayed percentage. Current independent human review remains an evidence requirement for our assessment, not evidence that AI already validates everything autonomously. Machine checking and existing computing infrastructure may support the endpoint, but necessary ongoing human research or repair would prevent a 100% rating. Even 100% on all six outcomes would require a separate field-wide demonstration before claiming mathematics as a whole has met that endpoint.
Estimates as of November 7, 2026
| Measurable outcome | Estimated progress | Execution / breadth / agenda / validation / improvement (each out of 20) |
|---|---|---|
| Advanced examination performance | 50% | 15 / 15 / 5 / 10 / 5 |
| Formal verification | 45% | 15 / 10 / 5 / 10 / 5 |
| Research problem success | 25% | 10 / 5 / 0 / 5 / 5 |
| Substantial novelty | 25% | 10 / 5 / 0 / 5 / 5 |
| Time to a new proof | 30% | 15 / 5 / 0 / 5 / 5 |
| Research productivity | 20% | 10 / 5 / 0 / 5 / 0 |
Each outcome explains its estimate next to its existing empirical baseline. Do not average these overlapping indicators into a field-wide percentage. Preserve dated scores and reasons when updating them.
Measurable features
| Feature | Measurement and acceptance rule |
|---|---|
| Advanced examination performance | Fully correct solutions / all assigned fresh graduate-level problems, plus rubric-based partial credit. Use timed, independently written qualifying or comprehensive exam sets; report algebra, analysis, geometry, probability, and other branches separately. Doctoral programs do not share a universal final exam. |
| Research problem success | Independently accepted solutions / all preregistered research problems within a fixed time and compute budget. Separate known-answer problems from genuinely open ones. |
| Time to a new proof | Wall-clock hours from frozen problem statement to accepted proof; separately report time to informal argument, Lean formalization, and independent review. Include failed attempts and human hours. Report unresolved problems at the cutoff instead of dropping them from timing results. |
| Substantial novelty | Count proofs approved by at least two independent specialists after a documented literature search. Classify a new theorem separately from a substantially new proof of a known theorem. Renaming variables, rearranging steps, routine specialization, or translating a known proof into Lean does not qualify as substantial novelty. |
| Formal verification | Percentage of claimed completed proofs with a reproducible Lean project, pinned Lean and mathlib versions, and an independent clean rebuild and proof audit. |
| Research productivity | Accepted substantially new results per total research dollar and human hour, with difficulty and significance reviewed rather than inferred from raw theorem counts. |
Required proof package
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.
Proposed milestones
Score at least 80% fully correct on 100 fresh graduate-level problems across at least five branches, under fixed first-attempt budgets and blinded grading. Publish the matched human comparison.
Deliver one substantially new result accepted by two independent specialists with the complete audited Lean package. Maintain separate counts for new theorems and new proofs of known theorems.
Produce ten such accepted results across at least three branches; compare total cost and completion time with a prospectively matched human research cohort.
Demonstrate that a verified AI-developed mathematical method improves later AI research on fresh tasks under controlled resource budgets. This last step connects mathematics to the feedback hypothesis directly.