Research library
Time to a new proof
Area: definition. Apply the shared measurement protocol.
Estimated progress toward AI-managed mathematics
30% 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 + 5 + 0 + 5 + 5 = 30/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: Generation and known-theorem formalization can be rapid. The end-to-end time from a new question to a verified substantial result, including failed searches and human work, is still unmeasured. Fast selected demonstrations therefore receive only partial credit. Evidence and dated sources are in the baseline below.
What would move the score: Raise the estimate when prospective campaigns report the entire time distribution, unresolved cases and negligible human work through accepted new proofs. Reassess downward if replication fails or previously hidden human assistance emerges.
Measurement and acceptance rule
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.
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: public generation and formalization timings exist, but no comparable end-to-end time-to-accepted-new-proof baseline was established. Sources accessed November 7, 2026.
Dated findings
| Evidence date | Timing | What the clock actually measures |
|---|---|---|
| March 27, 2026 | FormalProofBench reports mean latency of 4,036.78 seconds, approximately 67.28 minutes, per test for Claude Opus 4.5 Thinking. | Query execution including retries across the benchmark, not time to a successful novel theorem. Paper, Table 2 and section 5.2. |
| September 4, 2026 | Anthropic reports 11 days for Fermat formalization and three days for a Vinogradov three-primes formalization. | Known-theorem formalization demonstrations; the Fermat effort used parallel agents and human guidance. These are not novel-discovery or independent-acceptance times. Anthropic. |
| October 6, 2026 release | OpenAI reports roughly three hours of ChatGPT Pro thinking-equivalent compute per average result. | A compute-equivalence estimate, not observed elapsed time from problem assignment through specialist acceptance. Release announcement. |
Interpretation and tracking value
Baseline for median end-to-end hours to an independently accepted, substantially new, Lean-audited proof: not measured. This is a missing measurement, not evidence that no new proofs exist.
Keep generation, formalization, automated checking, and human review clocks separate. Parallel execution can reduce wall time while increasing aggregate compute. An average over selected successes also omits unsuccessful research, so it cannot predict time to a new accepted result in a prospective campaign.
Next comparable measurement
For each prospectively assigned problem, record assignment time, first correct informal proof, completed Lean artifact, independent rebuild, and final novelty/acceptance decision. Log active human hours and all parallel compute separately. Retain unresolved cases with their observation cutoff. Report success fraction at fixed horizons, then time distributions with unresolved cases appropriately censored; do not compute a success-only average and label it the campaign's completion time.