Five years ago, a language model solving multi-step mathematics was almost a curiosity. Today the question is no longer only whether it can solve exercises. It is becoming what happens when it can also produce research results.
The change matters for more than a benchmark table. For centuries, obtaining a new proof has been scarce work: it could take months, decades, or an entire career. Publications, reputation, training, and much of mathematical culture were built around that difficulty.
If proof production begins to scale computationally, scarcity does not disappear. It moves.
From exercises to open problems
The recent progression explains why the discussion changed so quickly.
OpenAI published GSM8K in 2021 because large models still failed systematically on elementary multi-step problems. A year later, Google’s Minerva made a clear advance on technical problems spanning school, university, and quantitative sciences.
In 2023, FunSearch combined a program-generating model with an automatic evaluator. It found new constructions for the cap set problem and better bin-packing heuristics. The conceptual step mattered: candidates could be tested and retained when they improved the state of the art.
In 2024, AlphaGeometry approached the average performance of a human gold medallist on a set of historical olympiad geometry problems. AlphaProof and AlphaGeometry 2 then solved four of the six International Mathematical Olympiad problems: 28 out of 42 points, silver-medal level.
In July 2025, an advanced Gemini Deep Think reached gold-medal level: five problems, 35 points, and natural-language proofs within the 4.5-hour limit. The symbolic competition barrier had fallen. One comfortable distinction remained: an olympiad is not research.
In 2026, the category of evidence changes
First Proof tested that frontier directly. It collected ten problems arising from active research whose solutions were known to their authors but had never been published. Four systems worked under controlled conditions, and 30 specialists reviewed the answers.
For seven of the ten problems, at least one system produced a solution judged essentially flawless or requiring only minor revision. The report also records the failure mode: systems often explained routine parts in detail while skating over the hardest step, and some citations did not support the claim being made.
That is more informative than saying “AI can do mathematics.” It shows real capability on a small sample and the weaknesses that emerge when plausible prose faces expert review.
In May, OpenAI published a counterexample generated by an internal model that disproved an Erdős conjecture about unit distances in the plane. External mathematicians checked the proof and wrote a companion paper to explain and contextualise it.
In August, OpenAI presented ten results from its internal Astra system across geometry, coding theory, groups, complexity, cryptography, and combinatorics. The company says the system generated the arguments, humans prepared the manuscripts with the model, and the model then formalised each argument in Lean. They are public and checkable results, but their long-term reception and significance remain for the mathematical community to determine.
Days later, Anthropic announced another striking advance. An experimental Claude tried to attack the Riemann hypothesis. It did not solve it. During the attempt, it produced an argument raising a related lower bound—from 41.6% to 67.2%—for the fraction of zeta zeros on the critical line.
This does not mean the hypothesis is “67% solved.” Anthropic explicitly says it does not expect the technique to prove the conjecture. Two in-house mathematicians validated the work, external specialists examined it, and a Lean formalisation exists. It is progress on a related question, not a fraction of the main conjecture.
Checking a proof is not understanding it
Mathematics has an unusual advantage over other sciences. A model-designed molecule still needs a laboratory. A proof can be translated into a formal object and checked step by step by a small kernel. Lean does not need to trust a company’s reputation or an author’s intuition.
But formal verification answers a limited question: does the conclusion follow from the encoded axioms and definitions through valid inferences? It does not tell us whether the formalisation captures the intended statement, whether the proof explains anything, or whether the result deserves attention.
A 100,000-line proof can be correct and still be unusable by a community that does not understand its central idea. Turning it into smooth prose is not enough either. An over-polished explanation can hide the choices, failed attempts, and connections through which people actually learn the argument.
From proof scarcity to proof indigestion
Terence Tao frames the risk as a shift from proof scarcity to proof abundance. If we assume that AI will complete a meaningful share of research tasks, a chain of bottlenecks appears:
- generate a candidate proof;
- verify that it is correct;
- explain it so others can understand it;
- have the community assess and use it;
- integrate it into theories, courses, and textbooks.
Automating the first stage does not automate the rest. It may flood them. Proofs can accumulate faster than we can referee, read, and turn into shared knowledge.
This problem predates AI. Specialisation, long papers, and pressure on peer review had already produced a literature that is difficult to digest. Mass generation can multiply the mismatch.
The valuable part may never have been only the theorem
Problem solving is only one part of doing mathematics. Choosing good questions, building definitions, finding connections, forming judgement, teaching, and sustaining a community all matter too.
Historically, these activities were correlated. Producing a difficult proof usually required deep understanding; the process created techniques, intuitions, and new questions. “Proving a result” could therefore stand in as a rough proxy for many other contributions.
AI can break that correlation. If generating a proof takes minutes but understanding why it works takes months, the output is no longer a sufficient measure of valuable work.
That raises harder questions:
- Who deserves credit when different actors generate, select, verify, and explain a proof?
- How do we train mathematicians if we automate the painful steps through which they learn?
- How do we prioritise a literature that grows faster than people can read it?
- Can a theory be formally correct while no person understands it as a whole?
- Which activities should remain human even when they can be automated?
The answer is neither to reject all automation nor to accept anything that passes a verifier. It is to design processes in which generation, validation, attribution, and explanation are separate and visible.
AI does not make mathematics less interesting. It makes it impossible to keep confusing proof production with understanding. If proving stops being the hard part, we may discover that the value was always also in knowing what to prove, why it matters, and how to make it intelligible to others.
Sources
- OpenAI: Solving math word problems (GSM8K)
- Google Research: Minerva
- Google DeepMind: FunSearch
- Google DeepMind: AlphaProof and AlphaGeometry 2 at IMO 2024
- Google DeepMind: Gemini Deep Think at IMO 2025
- First Proof: second batch report
- OpenAI: counterexample to the unit-distance conjecture
- OpenAI: ten advances in mathematics and theoretical computer science
- Anthropic: progress related to the Riemann zeta function
- Terence Tao: Mathematics in the age of AI
