Research library
Research productivity
Area: definition. Apply the shared measurement protocol.
Estimated progress toward AI-managed mathematics
20% 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 10 + 5 + 0 + 5 + 0 = 20/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: Low-cost benchmark proofs and growing research output suggest useful assistance. Full costs, human hours and independently accepted substantial results are not jointly measured, so autonomous sustained research productivity has the weakest evidence here. Evidence and dated sources are in the baseline below.
What would move the score: Raise the estimate when complete campaigns document accepted novel results per total dollar and human hour and sustain improvement without human research management. Reassess downward if replication fails or previously hidden human assistance emerges.
Measurement and acceptance rule
Accepted substantially new results per total research dollar and human hour, with difficulty and significance reviewed rather than inferred from raw theorem counts.
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: inference-cost and output-volume proxies are available; accepted novel results per total dollar or human hour remain unmeasured. Sources accessed November 7, 2026. Costs below are source-era figures, not current API price estimates.
Dated findings
| Evidence date | Observation | Accounting limitation |
|---|---|---|
| March 27, 2026 | FormalProofBench: Opus 4.5 Thinking averages $1.34 per test at 33.5% success. Dividing gives approximately $4.00 per successful benchmark proof. | Derived inference-cost proxy; includes test failures through the average, but excludes labor and research novelty. Paper. |
| June 8, 2026 revision | AlphaProof Nexus reports per-problem inference costs of a few hundred dollars. | Authors explicitly say these exclude the full discovery search across 353 problems; some comparisons omit AlphaProof cost, estimated at $60 per problem. Cost discussion. |
| October 6 release; repository observed November 7 | OpenAI describes approximately 4,000 posed problems and a catalogue of 721 manuscripts in 373 families. | No one-to-one mapping from attempted problems to independent accepted discoveries; dividing catalogue counts by 4,000 would be misleading. Repository. |
| September 4, 2026 | Anthropic reports roughly six billion output tokens for its Fermat formalization. | Resource-use disclosure, not a complete dollar or human-labor cost and not a novel-discovery numerator. Anthropic. |
Interpretation and tracking value
Record approximately $4 per successful historical FormalProofBench task only as a narrow cost proxy. It does not measure research productivity, and price changes alone can improve it without a mathematical capability gain.
For the requested measures, record accepted novel results per total research dollar: unknown; per human hour: unknown; improvement against matched human research: unknown. Public evidence reviewed here does not supply a complete, comparable numerator and denominator. Discovery claims, candidate screening, formalization, and expert validation consume different resources.
Next comparable measurement
Follow a fixed prospective cohort. Count all failed searches, model and tool costs, hardware, preparation, formalization, specialist review, repair, and human time. Count each accepted substantial result once. Report total campaign cost divided by accepted results, accepted results per human hour, and quality/significance strata. If nothing qualifies, report zero accepted output and full expenditure rather than omit the campaign. Compare AI-assisted and human-only cohorts using matched problems and observation periods.