Research library
Advanced examination performance
Area: definition. Apply the shared measurement protocol.
Estimated progress toward AI-managed mathematics
50% 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 + 15 + 5 + 10 + 5 = 50/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: Some supplied-statement proof benchmarks are saturated, supporting strong execution on bounded tasks. Fresh examination coverage, autonomous problem formulation and independent semantic checking remain incomplete; the baseline's 100% benchmark score is not 100% autonomy. Evidence and dated sources are in the baseline below.
What would move the score: Raise the estimate when fresh cross-branch exam performance persists without supplied formal statements or expert repair, with automated checking of intended meaning. Reassess downward if replication fails or previously hidden human assistance emerges.
Measurement and acceptance rule
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.
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: a useful graduate-level formal-proof proxy exists; the exact fresh-examination measure is not yet established. Retrieval date for all sources below: November 7, 2026. A page's update date is not necessarily the date each model was tested.
Dated findings
| Evidence date | Result | Scope and source |
|---|---|---|
| March 27, 2026, paper v1 | Claude Opus 4.5 Thinking: 33.5%, equivalent to 67/200; Gemini 3 Pro: 18.5%; GPT-5.2: 13.5%. | Historical FormalProofBench evaluation: 200 advanced undergraduate/graduate problems, supplied Lean statements, up to 40 tool-assisted turns. Paper, Table 2. |
| October 29, 2026, leaderboard update | ProofBench v1.1: Sonnet 5.5, Opus 5.5, Fable 5.1, and AlephProver each 100/100; GPT-6.1 Sol 99/100. | Private test split; qualifying-exam/textbook material with supplied formal statements. General models get 40 turns; specialist systems have different harnesses. The provider explicitly disallows comparisons with earlier revisions. Vals AI methodology and results. |
The current grader permits native_decide, broadening the trusted computing base. Scores therefore do not establish compliance with a stricter kernel-only audit. Vals AI.
Interpretation and tracking value
Record 100% on ProofBench v1.1 as a saturated benchmark observation, not “100% of PhD final exams.” The requested measure additionally requires fresh questions, timed examination conditions, per-branch reporting, and a matched human comparison. Those conditions were not established together by the reviewed evidence. Status for that exact measure: not measured, not zero.
Do not calculate a March-to-October percentage-point improvement: the benchmark changed. Nor does solving supplied formal statements measure the ability to formulate the right statement from scratch.
Next comparable measurement
Preserve the v1.1 label, private-test denominator, model configuration, permitted axioms, and tool budget. Obtain a fresh 100-question examination set across five branches with blinded grading and human controls. Record complete correctness, partial credit, time, and branch-level outcomes separately. When replacing a saturated benchmark, run overlapping models on both versions rather than splice their scores.