Research library
Substantial novelty
Area: definition. Apply the shared measurement protocol.
Estimated progress toward AI-managed mathematics
25% 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 + 5 = 25/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: Evidence supports some novel mathematical contributions, but catalogue counts contain related, revised and unverified claims. Establishing significance and prior art still depends heavily on specialists, and the project's fully qualified novelty count is unknown. Evidence and dated sources are in the baseline below.
What would move the score: Raise the estimate with independently confirmed new concepts or methods across branches, supported by reliable autonomous prior-art checking and novelty assessment. Reassess downward if replication fails or previously hidden human assistance emerges.
Measurement and acceptance rule
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.
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: 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
| Evidence date | Finding | Novelty classification for this baseline |
|---|---|---|
| May 21, 2026; revised June 8 | AlphaProof Nexus authors report resolutions of open Erdős/OEIS questions and an improved convex-optimization bound using a new parameter schedule. | Research-discovery evidence, author reported. Do not automatically treat every formalized conjecture as a separately significant new theorem. Paper. |
| September 4, 2026 | Fermat's Last Theorem formalization follows existing mathematics. | Formalization achievement; excluded from the count of substantially new theorems or proof strategies. Anthropic. |
| November 7, 2026 observation | OpenAI's catalogue lists 721 manuscripts in 373 related-result families and describes the material as research data at differing verification stages. | Candidate claims, not 721 independently accepted discoveries; related papers can share one result. Repository README. |
| October 7, 2026 correction record | Three manuscripts withdrawn; 14 others revised. | Track withdrawals and repairs explicitly. A release count cannot stand in for a vetted novelty count. Release history. |
| November 7, 2026 observation | Epoch's Open Problems inventory classifies one AI-associated solution as a breakthrough and one as a major advance; both are human-plus-AI entries. | Editorial significance assessments, distinct from this project's required two-specialist novelty approval and Lean audit. Epoch inventory. |
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.