Mathematics

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

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.

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

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.

Status: positive results on open problems, with measurable but highly benchmark-specific success rates. All sources were checked November 7, 2026; percentages calculated below are simple successes divided by the stated denominator.

Dated findings

Interpretation and tracking value

Use 3/68 at the stated Epoch budget as the clearest recent, reproducible-protocol reference in this review. It remains evaluator-reported evidence, not a proof rebuild performed for this repository. Separate the earlier 353-problem campaign and the Open Problems inventory into different series.

These figures do not imply a 4.41% chance of solving an arbitrary research question. Problem selection, existing formal statements, budgets, and publication exposure matter. With only three successes, small count changes produce large relative changes.

Next comparable measurement

Capture task IDs, model release and training cutoff, exact harness, number of attempts, actual spend, timeouts, and accepted proof artifacts. Re-evaluate the same unresolved subset under the same budget; flag problems whose solutions became public before later models' training cutoffs. Preserve full-set historical scores alongside any contamination-filtered comparison.

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

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.

Status: documented research advances and large claim collections exist; a count satisfying this project's full novelty-and-verification rule is not yet established. Sources accessed November 7, 2026.

Dated findings

Interpretation and tracking value

The baseline is positive evidence of novel research, with an unestablished qualifying count. Do not record zero: this review did not perform a comprehensive adjudication of all candidates. Conversely, neither proof compilation nor a publisher's claim establishes that all required novelty checks have passed.

Separate new theorems, substantially new proofs of known theorems, improved bounds, routine consequences, rediscoveries, and formalizations. Assign one stable discovery ID across related manuscripts and research areas.

Next comparable measurement

Create a candidate ledger containing exact theorem, earliest public date, prior-art search, AI/human contribution, two independent specialist decisions, Lean artifact and audit, and acceptance date. Promote only fully documented candidates into the qualifying count. Preserve withdrawn, disputed, and pending records. Reassess credit and priority when new prior work appears rather than silently rewriting the historical total.

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

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.