Math 2.0: Why Solving Is Only the Beginning

Imagine opening a theorem file produced by an AI system. The file is enormous, the checker accepts it, and yet nobody in the room can explain the key idea, which assumptions are doing the work, or what problem should come next. We have a correct answer, but the answer has arrived without a community around it.

That is the tension behind Math 2.0, a phrase for mathematics in which artificial intelligence can generate and verify proofs at a scale that changes the research workflow. It is not a new branch of mathematics or a software release. It is a question about what we choose to count as progress.

A proof can be correct and still be lonely

In the older Math 1.0 rhythm, proving a difficult conjecture—a mathematical claim awaiting proof—was the beginning of a long social and intellectual process. The authors gave talks. Other mathematicians tried the argument, found cleaner routes, connected it to neighboring subjects, and turned its central ideas into lemmas that could be reused. Graduate students encountered the result in seminars or lecture notes, then carried pieces of it into the next generation of problems.

Exposition, meaning the careful explanation of a result and its ideas, was not decoration added after the real work. It was part of how the result became useful. A proof that nobody can teach, adapt, or place in context has less life than a shorter proof that reveals why the argument works.

AI can compress the first step dramatically. That is valuable. It can also create a dangerous stopping point: a problem is marked solved, the proof is stored, and everyone moves on before the result has been digested.

What AI can do now

A formal proof is a proof written in a strict language that a computer can check line by line. A theorem prover, also called a proof assistant, is the software that checks it. Lean is one such system. It lets mathematicians state definitions and theorems precisely, then asks a small trusted kernel—the part of the system responsible for checking final proof objects—to verify that the conclusion really follows from the assumptions.

Here is a tiny Lean example:

import Mathlib

example (a b: ℝ) (h: a = b): a + 1 = b + 1:= by
 simpa [h]

The symbol ℝ means real numbers. The hypothesis h says that a and b are equal. The tactic, which is a small proof instruction, rewrites the expression using that equality and checks that both sides match. The example is elementary, but it shows the important boundary: a language model may suggest a proof, while Lean decides whether the submitted proof is valid.

By 2026, this approach had moved well beyond toy examples. At the 2024 International Mathematical Olympiad, Google DeepMind’s AlphaProof, combined with AlphaGeometry 2, solved four of six problems and reached 28 of 42 points, equivalent to a high silver-medal result. A Nature paper published in November 2025 described how AlphaProof used reinforcement learning, a method in which a system improves by trying actions and receiving feedback, inside Lean. Its training pipeline translated roughly one million informal problems into around 80 million formal problem statements.

Those numbers are striking, but they describe proof search under formal constraints. The system can explore a huge space of possible steps and receive an unmistakable signal when Lean accepts one. That is different from deciding which questions are fertile, explaining a surprising construction to a room of mathematicians, or helping a newcomer see why a theorem deserves attention.

The missing layer is digestion

Formal verification answers an essential question: is this derivation valid? The harder question is: what does this theorem change?

Math 2.0 should treat the second question as a technical requirement, not a public-relations exercise. An AI-assisted result ought to come with a compact human proof, a map of the important lemmas, examples showing where the assumptions matter, and notes about failed approaches. A million verified steps may be useful to a checker, but a researcher usually needs the one construction that makes the argument click.

The same applies to community. Mathlib, the shared mathematics library built around Lean, is more than a warehouse of finished theorems. It gives researchers a common vocabulary, reusable components, and a place where definitions are tested in public. Documentation, code review, discussions about naming, and repairs to old results all make future work faster. They may look like maintenance from a distance, yet they are part of the field’s intellectual infrastructure.

Then there is direction. A solved problem should fan outward into examples, counterexamples, stronger variants, weaker hypotheses, computational experiments, and connections to other subjects. AI systems are well suited to generating many such variations. Humans still need to judge which ones are mathematically meaningful rather than merely numerous.

A healthy workflow might look like this:

conjecture
 ↓
formal statement
 ↓
machine search and checking
 ↓
human explanation
 ↓
examples, variants, connections
 ↓
new questions

Many current systems are becoming impressive at the third line. Math 2.0 will be defined by whether the rest of the chain becomes equally visible and valued.

A better ladder for newcomers

The fear that AI will remove every beginner-sized problem is understandable. If raw problem solving becomes cheap, a student may wonder where a first contribution can fit.

The answer is not to protect a scarcity of puzzles. It is to recognize more kinds of mathematical work. A newcomer can formalize a known theorem, test whether a hypothesis is actually necessary, find a counterexample, simplify an opaque proof, improve a library lemma, create examples, or write an explanation that makes a difficult idea accessible. Each task creates useful ground for someone else.

These are not consolation prizes. Formalizing a familiar result can reveal that its usual statement hides an unnecessary assumption. Writing examples can expose the right generalization. Comparing two proofs can show which ideas transfer to another subject. A field with many such entry points has a future; a field that rewards only spectacular firsts eventually becomes a locked room.

That means education, publication, and academic careers will need a broader scorecard. A strong AI-assisted paper might include the formal statement, machine-checked proof, readable proof sketch, dependency information, failed attempts, generated variants, and open questions. Credit should also reach the people who build libraries, maintain datasets, write expository notes, and create the discussions that allow results to spread.

The first proof will still matter. It should no longer be the only trophy.

Math 2.0 will not mean that humans stop proving theorems. It will mean that a proof is judged partly by the life it creates afterward. A machine-checked argument is a seed; exposition makes it understandable, community makes it reusable, and new questions keep it growing. The best AI result will not merely close a problem quickly. It will leave mathematics richer than it found it.