Terence Tao at ICM 2026: What Mathematics Keeps When AI Can Prove

Video: Bilibili BV11T8A6FEgC. The upload is about 51 minutes long. Bilibili exposes no public subtitle track for this video, so this article is an analysis of the lecture topic, its public slides, and Tao’s accompanying essay—not a verbatim transcript.

The provocative part is not “AI can do mathematics”

The title of Terence Tao’s ICM 2026 public lecture is deliberately broad: Mathematics in the Age of AI. The obvious question is whether a model can solve a hard problem. Tao’s more useful question is what happens to the mathematical community when systems can generate research-level candidates faster than people can read, verify, explain, and absorb them.

That change has a different shape from the usual automation story. A calculator did not make arithmetic meaningless. Computer algebra did not make symbolic manipulation disappear. A proof assistant did not make proof irrelevant. Each tool moved the scarce part of the work. AI may move the scarce part again—from producing a plausible argument to deciding which arguments deserve human attention and become durable mathematics.

The video description frames the tension correctly: the challenge is not only capability, but the values and practices of the community. Tao’s essay, Mathematics in the age of AI, gives the public lecture a more precise written backbone. The lecture slides are available from Tao’s website.

A proof is a pipeline, not a sentence

Popular discussions compress mathematics into a binary test: is the proof correct? Research mathematics is a longer pipeline:

Someone chooses a question that is worth asking.
A conjecture is shaped into a tractable form.
Ideas, lemmas, examples, and counterexamples are explored.
A candidate proof is produced.
The proof is checked, often by several people and sometimes by software.
The argument is explained in a way that others can reuse.
The result enters the shared body of mathematics through seminars, citations, teaching, and later work.

AI can help at every stage, but not in the same way. A language model can suggest a lemma, translate notation, search a large corpus, or draft Lean code. A theorem prover can reject an invalid formal term. Neither fact alone answers whether the result is important, understandable, well-motivated, or worth building on.

This distinction explains why “AI generated a proof” is an incomplete headline. A formally checked proof establishes a strong kind of correctness. It does not automatically supply a good definition, a compelling reason to care, a short conceptual explanation, or a map of the consequences.

Abundance changes the economics of attention

If AI produces ten plausible proofs, a researcher can inspect them. If it produces ten thousand, production is no longer the bottleneck. Verification, ranking, and interpretation become the bottlenecks.

This is a mathematical version of Goodhart’s law. Once a visible metric becomes a target, systems optimize the metric rather than the underlying goal. If publication rewards proof-shaped output, researchers may receive mountains of technically valid but low-value arguments. If benchmark scores become the goal, models may learn to solve the kinds of problems that are easiest to score while neglecting the questions that reshape a field.

Tao’s framing matters because mathematics has several goals at once: solving open problems, developing theory, explaining phenomena, training new mathematicians, building a community, and creating knowledge that remains usable. “More theorems” is only one measurement, and a noisy one.

The risk is not that correct mathematics becomes false. The risk is that the stream of new material outruns the community’s ability to distinguish a useful idea from a formally decorated dead end.

Formalization is the missing bridge

Natural-language proofs are powerful because they are compact and flexible. They are also full of omitted steps, overloaded notation, and context that experts reconstruct automatically. Formal systems such as Lean force definitions and dependencies into a machine-checkable language.

That makes formalization more than a final audit. It can become an interface between people and models. A model proposes a proof state or a tactic; the prover reports exactly what is accepted; the human changes the statement, the strategy, or the decomposition. The interaction is narrower than a chatbot conversation, but the feedback is much sharper.

The trade-off is real. Formalizing a theorem can take longer than writing an informal proof, especially when libraries do not yet contain the right abstractions. A formally verified result may still be hard to understand. A community that values only formal completion could accidentally reward low-level labor over conceptual progress.

The sensible target is a layered workflow: informal exploration for speed, formal checking for reliability, and human exposition for transfer. Each layer catches a different class of failure.

Collaboration gets larger—and stranger

Mathematics has always been collaborative, even when a paper carries one name. It depends on conversations, references, examples from colleagues, software, databases, seminars, and generations of shared notation. AI makes the collaboration more explicit and potentially much larger.

One researcher may ask a model to search variants of a conjecture. Another may formalize the surviving lemma. A third may find a counterexample. A fourth may write the explanation that makes the result legible. The old image of one person solving one problem from beginning to end becomes less accurate.

That creates questions of credit and responsibility. Who is an author? Who is accountable for an error? How should prompts, failed attempts, model versions, and machine-checked artifacts be recorded? Tao’s proposal to make tool use transparent is practical: readers need to know which parts were produced, checked, or transformed by automated systems.

Transparency is not a ritual confession. It is provenance. Without provenance, future mathematicians cannot tell whether a result is independently understood, reproducible with available tools, or dependent on a vanished service and an opaque prompt.

What this means for students

Students will face a sharper version of an old problem: the easiest way to obtain an answer is often the worst way to learn. A model can supply a polished derivation before a student has learned to notice a missing hypothesis.

The answer is not to ban tools. Students should learn to use them as adversarial partners:

ask for several approaches, then compare their assumptions;
request a counterexample before accepting a general claim;
formalize a small lemma instead of trusting a long explanation;
explain the proof without looking at the generated text;
keep a record of failed routes and why they failed.

The human skill that becomes more valuable is not memorizing every manipulation. It is judgment: choosing a useful problem, detecting a suspicious step, and explaining why an abstraction deserves to exist.

The likely near future is uneven

AI will not improve every area of mathematics at the same speed. Domains with abundant formal libraries, clear symbolic structure, and cheap verification are easier targets. Areas that depend on taste, geometric intuition, long cultural context, or new definitions may resist automation for longer.

Even inside one field, capability will be lumpy. A system may prove a difficult-looking technical lemma while failing on a basic variant because the representation is wrong. It may find a result in a large search space but fail to explain why that result changes the field.

That unevenness is why both triumphalism and dismissal are poor strategies. The right unit of evaluation is a complete workflow: problem selection, candidate generation, checking, explanation, reproduction, and downstream use.

My reading of the lecture

The strongest message is institutional rather than futuristic. Mathematics should decide what it values before automated systems force that decision through sheer volume.

If the community protects only the final theorem statement, it may lose the reasons, methods, and educational pathways that make mathematics humanly useful. If it treats AI as a dangerous intruder, it will miss a chance to make verification and collaboration more accessible. The better response is to widen the pipeline while keeping standards visible.

AI can generate candidates. Proof assistants can check formal obligations. People still have to decide what counts as progress, what deserves explanation, and what should be carried forward.

That is a less cinematic conclusion than “AI replaces mathematicians.” It is also the one that the video, the public essay, and the surrounding discussion support most strongly.