Intelligence / Mathematical discovery / Attribution
Who discovered the theorem?
The question is no longer whether a machine can solve a hard mathematics problem. It is whether—and in what sense—it can make mathematics that was not known before.
Five case studies, from program search to a recent grand-conjecture proof, show why the answer depends on the intellectual work being counted. There is no honest single percentage of mathematics driven by AI.
Inspect the evidence ledger ↓A problem can be hard without being new. A theorem can be new without being important. A proof can be correct without being understood by its discoverer. An AI system can be indispensable to a result without having chosen the question that was worth asking.
Four different discoveries hidden inside one word.
When a mathematical paper says that a result was discovered, it may refer to finding a previously unknown construction, proving a proposition whose truth was unsettled, recognizing a useful intermediate concept or inventing a way of thinking that later mathematics adopts. These are connected but not interchangeable events.
AI systems can enter at many points. They can propose mathematical objects, navigate proof searches, generate counterexamples, mechanically verify logical steps or explore dozens of approaches under a researcher's direction. An honest history of a result has to identify which role the system played, which decisions humans made, what the work actually established and how it was checked.
This dossier is an experiment in making those distinctions visible. The five selected cases are not a random sample and cannot estimate how much of all new mathematics is AI-driven. Their point is to show what such an inquiry would have to measure.
What would you count?
Apply four different definitions to exactly the same five cases. A case may satisfy several. The changing count does not quantify AI's contribution to mathematics; it demonstrates how much the result depends on what “contribution” is taken to mean.
This includes supplied contest problems. It cannot be interpreted as independently discovered new mathematics.
What did the machine actually do?
Every case retains its provenance, human contributions, machine contributions, verification standard and a clear statement of what the evidence does not establish. The cases are shown in publication order; selection by a criterion is an editorial filter, not a statistical analysis.
The machine proposed programs that produced better mathematical constructions.
FunSearch · New construction for an open problem
FunSearch paired a language model with an automated evaluator in a search over programs. The resulting constructions improved known results for cap sets and supplied interpretable programs rather than merely unstructured answers.
The paper reports previously unknown cap-set constructions and a better asymptotic lower bound, alongside results in online bin packing.
Generate candidate programs; iterate through evaluation feedback and retain higher-performing proposals.
Define the mathematical task and evaluator; design the search process; interpret, check and communicate the constructions.
How it was checked. The program-defined constructions can be evaluated by the designated objective; mathematical claims are presented in a peer-reviewed Nature paper. This is not the same as an independent audit of every original research contribution.
What it does not establish. Shows that an AI-containing search system can contribute a mathematically new construction. It does not measure how frequently AI drives progress across combinatorics.
Editorial caution. A mathematically useful program, a human mathematical insight extracted from that program and an autonomous machine theorist are three different claims.
A convincing proof need not be a new theorem.
AlphaGeometry · Proofs on a defined benchmark
The neuro-symbolic system combined learned geometric guidance with symbolic deduction. The published benchmark showed solutions for 25 of 30 selected olympiad-level geometry problems.
AlphaGeometry solved 25 of 30 benchmark problems and produced human-readable proofs; the paper also describes a generalized version of a translated IMO theorem.
Propose useful constructions and reasoning steps for the symbolic engine to pursue.
Define the synthetic training setup and theorem proving task; select the benchmark and evaluate outputs.
How it was checked. The study reports mathematical evaluation of solutions; the 25/30 result describes a curated competition-level test set.
What it does not establish. Shows powerful mathematical problem solving. It does not directly count as independently originating new research questions or formalizing arbitrary areas of mathematics.
Editorial caution. The authors' described generalization matters, but the benchmark figure should not be reported as 25 discoveries of previously unknown theorems.
A proof can be machine-checked even when the research question came from humans.
AlphaProof · Machine-checked proofs of supplied problems
AlphaProof searched for formal proofs in Lean. Its 2024 IMO evaluation used expert formalization of the five non-geometry problems; the system proved three. AlphaGeometry 2 handled the geometry problem, for four of six problems overall.
AlphaProof solved three IMO problems under expert protocol, with Lean kernel verification; combined with AlphaGeometry 2, the total score was equivalent to an IMO silver medal.
Search over Lean tactics and adapt to problems over multiple days of computation; a related model generated possible answers for relevant tasks.
Manually formalize the IMO problems, set evaluation protocol and review the proofs; original problems came from the IMO committee.
How it was checked. The Lean kernel checked formal proofs; independent expert judges evaluated them against competition criteria. The system took days, unlike human contestants' time constraints.
What it does not establish. Strong evidence of verified formal problem solving under a specified protocol, not of autonomous original research across mathematics.
Editorial caution. It was not awarded an actual IMO medal as a human contestant, and IMO success is not a measure of research discovery rate.
The test changes when the conjecture was genuinely open.
Formal proof search on open problems · Reported open-problem resolutions
Researchers reported an AI agent using language-model proof generation with Lean verification on collections of open problems: nine of 353 selected open Erdős problems and 44 of 492 OEIS conjectures.
The authors report nine open Erdős problem resolutions and 44 sequence conjecture proofs in selected collections.
Generate candidate formal proofs and use a proof checker to accept or reject steps; automate repeated search.
Design the system, construct the problem sets, formalize or validate statements and evaluate the significance of the results.
How it was checked. The abstract states Lean-based verification of mathematical proof steps; this dossier does not independently inspect each certificate or review the provenance of all open-problem statements.
What it does not establish. Substantially stronger evidence of AI participating in open mathematical discovery than contest benchmarks. The fractions 9/353 and 44/492 refer only to those selected collections.
Editorial caution. The observed solve fraction must not be projected to all Erdős problems, to all open mathematics or to the fraction of mathematics invented by AI.
AI helped researchers explore many approaches. The conceptual proof remained human-directed.
KLS conjecture · Recent research-level theorem with collaborative AI use
Zhao Song and Xinzhi Zhang posted a proof of a dimension-independent bound for the Kannan–Lovász–Simonovits conjecture. Microsoft's research account describes iterative agentic exploration and human selection of mathematical directions.
The preprint proves an O(1) bound for the KLS constant; the institutional account describes AI-assisted search, human development of the recursive insight and parallel independent proof efforts.
Explore candidate approaches and carry out technical derivations under iterative direction; assist internal checking and drafting.
Choose directions, prune unsuccessful trajectories, identify and develop the key recursion, assemble and verify the final argument.
How it was checked. The theorem is stated in a 2026 preprint. The institutional account reports independent proofs and partial/associated Lean formalizations. This editorial dossier has not independently checked the full proof and does not represent the full argument as already formally certified.
What it does not establish. An especially instructive example of contribution that is significant without being autonomous. Human steering and formal proof status must be visible rather than hidden by an AI-generated label.
Editorial caution. Separate what the preprint proves from the institution's account of tool use. Do not treat an announced Lean formalization of related components as certified verification of every line of this manuscript.
The verifier does not know who had the idea.
The formal proof is one of mathematics' remarkable social technologies. A checker can establish that a proposed derivation follows the rules of an explicitly formalized system without trusting the proposer. AlphaProof's Lean-verified contest proofs illustrate this separation well: the machine found formal solutions within a human-defined evaluation pipeline, while the checking procedure evaluated logical validity rather than intellectual originality.
FunSearch occupies a different position. Its program search produced constructions relevant to an open question in combinatorics. The program can be inspected as a mathematical artifact, but its discovery involved a human-specified target, an evaluator and a search process. We should not erase the algorithm's contribution; neither should we mistake the program for an autonomous mathematician with self-selected goals.
The 2026 formal-proof-search results change an important variable: the reported target problems were open. Successfully verifying proofs in such a collection can produce new mathematical knowledge. But the selection of the open problems, the formalization of their statements, the preparation of the formal environment and the independent assessment of importance remain part of the historical account.
In the KLS case, the researchers' public account draws attention to human-directed, iterative exploration. AI systems explored possible approaches while mathematicians discarded weak routes and developed the decisive conceptual argument. The resulting theorem is a real advance whether or not AI operated autonomously. Our categories must be able to recognize major collaborative progress without pretending the machine independently originated the theory.
What a proper tracker would measure
For each mathematical result we would record the question's history, which subtasks the system performed, degrees of autonomy, validation methods, research novelty and documented subsequent influence. We would retain the original evidence and changes in assessment over time. A field-level trend would then require a carefully defined corpus of mathematical results, a sampling method, multiple raters for ambiguous contribution and transparent missing-data treatment.
There is no reason to collapse those measurements into a single score. A field may have high AI adoption but little demonstrated original discovery, or a few extraordinary AI-assisted results with low general adoption. That tension is precisely what the Atlas should reveal.
A contribution needs a verb.
Who posed the problem?
When the target is selected by a human mathematician, machine success is still real, but the system did not independently select a scientifically important research question.
What did the system actually generate?
A proof step, search strategy, construction, conjecture, auxiliary lemma, formal certificate, research direction and final theory are distinguishable intellectual contributions.
How was it verified?
An automatically checked Lean proof, an executable construction, a referee-reviewed manuscript and an independent alternative proof provide different kinds of assurance.
How much guidance was required?
Record human problem formalization and prompting. Count pruning and candidate filtering. Identify experiment design and mathematical decisions made by researchers. Avoid unsupported autonomy claims.
Was the result new and important?
A correct proof of a known theorem demonstrates mathematical capability. A verified resolution of an open problem adds knowledge. Transforming a field requires longer-horizon assessment.
What is the denominator?
A published set of illustrative wins is not a random sample of mathematical research output. Field-wide AI shares require a transparent corpus, attribution rules and coverage analysis.
Draft target, not a forecast
What happens when an AI proves something nobody knew?
One possible milestone lies at the border between assistance and intellectual independence. To forecast it properly, the criterion of success must be more precise than a headline.
Examine the connected prediction in the Atlas ↗- Target
- An AI system produces a proof of a mathematically nontrivial statement that was open before system execution. The statement's novelty is reviewed by qualified independent specialists; the proof is formally checked or published with independent mathematical scrutiny.
- Proposed horizon
- 31 December 2035
- Resolution requirements
- Before probability collection, specify what counts as nontrivial, admissible discovery, independent review and acceptable human selection or steering. Publish model versions and exact test protocol. A failed or ambiguous audit should not be silently scored as no.
- Conditional distinction
- Report separate versions for human-specified problems and machine-originated research questions; those are different forecasting targets.
- Probability
- — No prediction has been issued
The evidence remains open to inspection.
The account distinguishes published work, a recent preprint and the relevant institutional description of research practice. Our role is editorial analysis, not a claim to have independently re-proved these results.
- Mathematical discoveries from program search with large language models ↗Nature · 14 December 2023
Original research; construction claims and method.
- Solving olympiad geometry without human demonstrations ↗Nature · 17 January 2024
Original research; 25 of 30 benchmark questions.
- Olympiad-level formal mathematical reasoning with reinforcement learning ↗Nature · 12 November 2025
Original research; protocol, formal proofs and 2024 IMO evaluation.
- Advancing mathematics research with AI-driven formal proof search ↗Science · 8 October 2026
Original research; open Erdős and OEIS conjecture collections.
- An O(1) Bound for the KLS Constant ↗arXiv, version 2 · 4 October 2026
Preprint; the mathematical theorem and proof.
- Solving a 31-year-old grand challenge in mathematics – the KLS conjecture ↗Microsoft Research · 21 October 2026
Authors' institution's report on the AI-assisted process, parallels and verification status.
Editorial cutoff: 2026-10-22. This is a dated snapshot, not a continuously updated count. Corrections, independent replications and later mathematical appraisals should alter the connected contribution records without rewriting this published snapshot.