Deep Dive

Terence Tao on AI at the ICM: AI proofs will multiply, but math won't get faster

He breaks mathematical research into a five-step pipeline. AI dramatically speeds up only the first step; the further down the line you go, the slower and more human-dependent it gets.
The 60-Second Read
  • AI can now genuinely solve research-level math problems: First Proof gave four AI systems ten brand-new problems; seven of them received at least one solution deemed publishable. Meanwhile, the Erdős Problems website has accumulated nearly twenty AI-generated solutions, and no human expert is willing to verify them. The problems get solved; everything after that lags behind.
  • On July 24, at a public lecture during the International Congress of Mathematicians, Terence Tao addressed exactly this. He didn't argue about whether AI is up to the task. Instead, he asked the audience to assume it is—then asked: what does that mean for the field?
  • He framed mathematical research as a pipeline: produce a proof → verify it → write it readably → get peer acceptance → get it into textbooks. AI massively accelerates only the first step. The further along you go, the slower the work gets—and the more human, and the more valuable.
  • The most counterintuitive point: a proof that reads too smoothly may actually be harmful. He showed a photo of his youthful annotations on a 1991 Bourgain paper, scrawled with "AARGH!" and "I hate Jean Bourgain." The places that trip readers up are exactly what force them to slow down and actually learn.
  • His prescription for colleagues has three parts: normalize disclosing AI use; shift effort from racing to solve problems toward proof digestion; and the hardest one—if you can't explain your result, you shouldn't publish it.
On the Ground

AI can already solve research-grade problems. That's where the trouble begins.

The Erdős Problems website now holds dozens of AI-generated proofs.

Many of them are probably correct. The problem is that nobody is checking.

The people qualified to check definitely exist. The hard part: no mathematician of sufficient standing is willing to spend days reading an anonymous, potentially dozens-of-pages-long document, then sign their name to "I confirm this is correct." Some submissions even come with a disclaimer from the submitter: I'm not qualified to judge whether this is right.

From the stage, Tao posed the question: might we one day have a verified proof of a major result that no human understands well enough to explain?

And the fact that AI can solve research-level math is no longer hypothetical.

First Proof is an independent evaluation project that tests AI on research-level math. The approach: a group of mathematicians contributed problems from their own research, already solved but never published—nowhere online or in the literature. The second batch had ten problems spanning computability theory, discrete geometry, stochastic PDEs, von Neumann algebras, and more. In late May, under controlled conditions, four AI systems each attempted all ten, with one shot per problem and no human intervention allowed. The solutions went to blind review: roughly thirty experts in relevant fields, at least two reviewers per submission.

7 / 10
Problems where at least one AI system produced a publishable-level solution
39 total
Submissions from the four systems, double-blind reviewed by ~30 experts
1 problem
Where all four systems failed to make real progress (metric geometry)

For one stochastic PDE problem, a system's approach diverged entirely from the human author's—the reviewers were impressed.

July 24, Philadelphia. The quadrennial International Congress of Mathematicians—the field's highest-profile gathering—is underway. Tao delivers a public lecture titled "Mathematics in the Age of AI." Fifty-two slides.

His topic: AI can already do some mathematics. What should the field do about it?

On whether AI is "really" capable, he wrote a whole slide—then said he wouldn't discuss it

He phrased the question as a mathematical conjecture, deliberately leaving blanks:

AI Capability Hypothesis · Template

At some point in the near future, some AI tool will, at some cost, under some degree of human supervision, correctly complete some research-level mathematical tasks in some domains, with some non-trivial success rate, and some degree of correctness and quality.

The highlighted parts are all placeholders. How you fill them determines which version of the conjecture you're arguing for. People who debate AI capability are often just filling in different blanks.

Roughly speaking, he said, a weak form and a strong form are enough. The two versions imply completely different responses from the field:

Even the weak form is false

Then everyone can treat AI as a long-term irrelevance and go about business as usual.

The strongest form is true

Then sustaining the current culture and practice becomes very difficult — especially when "solve as many open problems as possible" is our top goal.

Then he said: this lecture is not about that conjecture.

His reasoning: the debate has stalled. There's a pile of evidence on both sides, but most of it wasn't collected under controlled scientific conditions. What's publicly visible is heavily distorted by reporting bias and assorted non-scientific motivations, and key costs and variables simply aren't disclosed. He also flagged a distinction worth not conflating: whether a claim is true is a completely different question from whether we want it to be true.

So he took another approach: he asked the audience to assume AI can do it, to accept it as a premise. He called it a "working hypothesis," and made it explicit: I'm not asking you to want it to be true, believe it's true, or accept it as true. This is a conditional analysis. Evidence for or against the hypothesis is irrelevant to what I'm about to say.

His framing: this is a foundational crisis — the second one

The first happened a century ago. For centuries before that, mathematics ran on a "naive" foundation: what sets, numbers, and infinity are, which axioms math rests on — these questions were mostly left to philosophers. The Russell paradox in 1901 and Gödel's incompleteness theorems in 1931 forced working mathematicians to re-examine the assumptions they'd been taking for granted.

Those three decades were turbulent but hugely productive: a clear, rigorous, standardized foundational framework emerged. It survived intense scrutiny and remains a trustworthy working environment for mathematics today.

Tao says we're entering a similar turbulent period. Last time, it was the logical foundations that needed re-examination. This time, it's the field's values and working practices. He also offered the same conclusion: once we've thoroughly examined and explicitly written down these things, the community will emerge stronger and more resilient.

The Mechanism

AI can help you solve more problems. But is solving more problems really the point?

AI writing fast is just the surface. The real reason proofs pile up: "solving a problem" was never the only thing this field is after.

In the lecture, Tao listed reasons for doing mathematical research. There were so many they barely fit on one slide:

Build theory
Solve olympiad problems
Solve Erdős problems
Apply knowledge
Mathematical knowledge↖ ↑ ↗ ← → ↙ ↓ ↘
Solve research problems
Build community
Train the next generation
Create works of lasting aesthetic value
Redrawn in Chinese from slide 22. These are the goals he listed. The eight outward arrows are from the original; what they point to will become clear below. Tao's own footnote under the figure: this diagram is grossly oversimplified; the real dimensionality is much higher.

In the past, he said, these goals were roughly aligned: progress on one usually carried the others along. So you could use one or two as proxies for the rest; many goals didn't even need to be stated explicitly.

But when any metric gets optimized to death, it runs into Goodhart's law: once a measure becomes a target, it ceases to be a good measure.

Tao added: generative AI is inherently "ungrounded" — its outputs aren't anchored in any fact, and it has no internal mechanism guaranteeing its statements are true. Combine that with the financial incentives of AI companies, and you have a recipe for triggering this law particularly easily.

So excessive AI optimization makes these once-aligned goals diverge from each other. He showed this on three consecutive slides:

Before

Goals roughly aligned. Push one, the others follow. So you can use one or two as proxies.

After excessive optimization

The same goals, now diverging. Proxies break down: the problem-solving number goes up, but the others don't follow.

Redrawn in Chinese from slides 20, 21, and 22 (the original progression: nearly aligned, then angles widening, then the eight-way divergence above). The central circles in both figures represent "mathematical knowledge."

This diagram is worth holding up to your own industry. Every field can list a set of goals like this, and every field got used to using one or two as proxies for the rest because they used to move together. AI excels precisely at driving a single metric to extreme heights on its own.

So which things should we actually want? That's the main body of the lecture. On stage, Tao revised the goal five times.

The Breakdown

From solving problems to writing textbooks, AI only speeds up step one

He picked "problem solving." He was careful to note this is only one facet of the field — theory building is an equally important other side that needs its own analysis — but problem solving is the part most exposed to AI.

The pipeline below is what his five revisions produced. Click the tabs to watch it grow:

Goal · v1Solve as many open problems as possible.
Goal · v2Solve as many open problems as possible, and verify that the solutions are correct.
Goal · v3Solve as many open problems as possible, verify them, and make sure the results are clearly communicated and understood by the mathematical community.
Goal · v4Solve open problems, verify them, ensure clear communication, and have the results digested and accepted by the community.
Goal · v5Solve open problems, verify them, ensure clear communication, get them digested and accepted, and have them incorporated into the canonical theory of the field.
Open problem
Proof generationMassively sped up by AI
Solution
Proof verificationAI helps; formal tools can check
Verified solution
Proof expositionAI's track record is mixed
Well-written solution
Proof publicationSlow; depends on human editors & reviewers
Accepted solution
Proof canonicalizationSlowest; needs collective deliberative consensus
Canonical theory
Redrawn and combined into an interactive Chinese version from the five flowcharts on slides 24, 26, 29, 37, and 43. The "Can AI handle this?" notes on the right summarize Tao's prose across those slides; they are not in the original figures.

v1: Solve as many open problems as possible

On its face this goal sounds fine, and the network is simple: an open problem on one end, a solution on the other, a single arrow called "proof generation" in between.

The risk was known long before AI: you'll receive a flood of incorrect solutions to major problems. Anyone who works in number theory has gotten emails claiming a proof of the Riemann hypothesis.

v2: Add "and verify that they're correct"

The pipeline grows a second stage: what's generated is first called an "unverified solution"; it only counts once verified.

Here AI genuinely helps. Proof assistants like Lean, Rocq, and HOL can encode mathematical proofs as code a computer checks line by line. Having AI do that translation is called automatic formalization.

Human verification

Read the whole argument, judge whether each step holds. Requires an expert in the subfield, days to weeks of time, and willingness to put their name on the conclusion.

It's tiring, it misses things, and often nobody picks it up because "it's not my research contribution."

Machine verification

Translate the proof into Lean or similar, and the compiler checks it line by line. If it passes, there's no logical gap.

The catch: someone (human or AI) has to do that translation first, and the translation is itself a heavy piece of work.

Tao said that on both the generation and verification ends, AI has already dramatically accelerated things in many cases, and under the working hypothesis, that acceleration will continue.

Then he posed the question: what if AI produces a long proof that nobody understands — not even the person who fed it the problem?

That's exactly the pile on the Erdős Problems website from the opening. A machine might verify it, but no human can step up and say "I've checked this, I vouch for it."

v3: Add "and ensure it can be clearly communicated and understood"

The pipeline grows another stage: a verified solution must become a "well-written solution." This step is called proof exposition.

And this is where AI behaves the strangest.

Counterintuitive

When the writing is too smooth, readers don't learn

Tao's assessment of AI's current mathematical writing is split.

The good half

Spelling, grammar, and formatting are nearly flawless.

He added a footnote here: arguably too flawless.

The bad half

It often goes on at length about trivial details, then rushes past — or actively obscures — the most interesting and novel parts of the argument.

It also frequently fails to relate the result to existing literature or give a high-level overview.

The same observation shows up elsewhere. In the blind review reports from First Proof's second batch, the same complaint recurs: AI solutions tend to be extremely thorough on routine parts, then hand-wave through the hardest steps — sometimes asserting a key conclusion "follows by standard arguments" without a reason, sometimes citing a paper that doesn't actually contain the stated result.

The reports also recorded something more damning. Several AI solutions to one problem borrowed line-by-line phrasing from the proposer's own earlier paper, including made-up terminology (T-patterns, bends) and equation labels (B, T, D, H), without citing that paper even once. The reviewer's exact words: if a human had submitted this, it would be plagiarism.

One level deeper: exposition can also be over-optimized

Exposition is a much fuzzier optimization target than verification. Under the working hypothesis, AI's exposition will improve eventually. But even once it improves, there's another problem: exposition itself can be over-optimized.

A proof can become too smooth: the routine parts and the genuinely hard parts are presented as equally easy to digest.

In human-written proofs, the places the author found difficult typically leave some kind of natural friction: sentences get rougher, gaps get wider, the tone tightens. These traces tell the reader: slow down here, look closer.

Excessive AI polishing sandpaper away both kinds of friction at once: the artificial (author was lazy, didn't write clearly) and the natural (this was genuinely hard). Once smoothed over, the reader glides through without being pushed to actually understand the key ideas. He used the phrase "paradoxically": the "flaws" in human exposition may end up helping readers.

Human-written proof
The line's height is how smooth it reads: high means smooth, dipping means stuck. The two dips are where the author also got stuck — sentences get rougher, gaps widen, tone tightens, and the reader is forced to slow down and actually understand.
Over-polished proof
Equally smooth from start to finish. The reader slides through and learns nothing.
This is an original schematic by this site, not from the slides.

After this section, he showed a photo.

Facing pages of a 1991 Bourgain paper covered in handwritten pen annotations in the margins and between lines
Slide 33. Tao's only caption: "A 1991 paper by Bourgain, annotated by a much younger me." Jean Bourgain was a Belgian mathematician, Fields medalist, and a major figure in harmonic analysis, who died in 2018.
Zoomed-in detail of the same page: AARGH handwritten beneath the printed text We skip the details, next to three question marks and I hate Jean Bourgain
A zoomed-in detail of the same page (cropped by this site). The printed line "We skip the details." is underlined, with AARGH! written beneath; to the right are three large question marks and further right, "Sobolev norms!"; the handwritten line above reads "I hate Jean Bourgain."

This photo is the physical evidence for the argument.

Bourgain wrote "we skip the details." The young Tao got stuck right there. He underlined it, put question marks, wrote "Sobolev norms!" to remind himself which direction to think, and finally scrawled in the margin: "I hate Jean Bourgain."

More than thirty years later, he photographed the page and put it up on the big screen at the ICM. These very sticking points forced him to slow down and genuinely learn the material. A proof where every step is equally smooth leaves no such place for the reader.

Immediately after, he quoted William Thurston's 1994 essay "On Proof and Progress in Mathematics":

We are not trying to meet some abstract production quota of definitions, theorems, and proofs. The measure of our success is whether what we do enables people to understand and think more clearly and effectively about mathematics.

William Thurston, "On proof and progress in mathematics," 1994
Diagnosis

More proofs, but math isn't getting faster

Making it readable for humans is only step three.

v4: Add "and have it digested and accepted by the community"

For a proof to actually contribute to a field, being correct and readable isn't enough. Other mathematicians need to digest it, absorb it into their own work.

The author can help: explaining where they got stuck, how they figured it out, why they took this path — these things let others absorb it faster. But current AI tools are quite opaque about their own solution process — especially proprietary models whose inner workings are trade secrets.

And community acceptance is, by nature, slow and human. Good exposition and careful writing can facilitate it, but ultimately it's an external process that can't be optimized unilaterally by the author and their AI.

What keeps this whole system running right now? Volunteer labor from human editors and reviewers. Tao pointed out: this work is often seen as less prestigious than generating proofs, but it's indispensable — it's how an individual mathematician's achievement becomes collective progress and understanding.

AI can act as a filter here — journals could automatically reject papers flagged as insufficiently verified or poorly exposited. But a filter can't substitute for acceptance itself.

v5: Add "and have it incorporated into the canonical theory of the field"

Even being published isn't always the end point. Key results eventually make their way into the field's authoritative textbooks and reference works, becoming the standard account taught to the next generation of students. Tao calls this step canonicalization.

It's the slowest stage of all, requiring broad, deliberative consensus across the community — and the least suited to AI optimization.

But, he said, it's the most valuable part of the entire pipeline. Two reasons. First, many applications only become feasible once the underlying mathematics has been thoroughly digested. Second, and more importantly: AI tools' success in mathematics today depends critically on the canonical theories human mathematicians built up over centuries. Models can solve problems because previous generations organized the field into a form that was learnable.

Once the five steps are in place, the diagnosis lands

If AI can do this work, and policy and culture don't change accordingly, this pipeline will develop "impedance mismatches" everywhere. It's an electrical engineering term — two stages that don't interface properly, so energy gets stuck at the junction. He also offered a blunter phrase: proof indigestion.

Concretely, four bottlenecks:

Before verificationAI-generated proofs pile up, waiting to be checked.
Before expositionMany verified proofs wait for a human-readable write-up.
Before reviewEven with requirements for correctness and clarity, volume overwhelms the traditional peer-review system.
Before canonicalizationEven published results outnumber what the community can integrate into canonical form.

In one sentence: we will move from an era of proof scarcity to an era of proof surplus.

Proof generationMassively sped up by AI
Proof verificationFormal tools help, but a human decides what's worth checking
Proof digestionWriting, publishing, textbook entry: human speed
Schematic showing three different speeds (original to this site, not in the slides). Bar lengths indicate only relative speed, not empirical data; the striped area at the right marks material piling up at the junction.

The signs are already visible. In fact, he said, the pressure had been building well before modern AI.

He once used a more intuitive analogy himself

Three months earlier, on social media, he recast the pipeline in terms of food:

Proof generation = foraging Proof verification = cleaning and inspecting Proof digestion = cooking

A society used to food scarcity is bottlenecked on getting food. The hard work of cleaning and cooking is appreciated, but the prestige goes to the hunter who brings down the prey. In that world, nearly any non-toxic meat or vegetable is welcomed to the communal table, and volunteers can always be found to turn it into a meal.

A potluck in a food-abundant society is different. Raw ingredients dropped off casually are no longer welcome: a stranger dumping the carcass of an unknown animal for others to clean and cook gets no thanks (unless the prey has an especially unique and interesting story behind it, and the meat is assured safe). Even a ready-to-eat meal that's been inspected, packaged, and certified is usually just one part of the table. What's truly valued is the home-cooked dish made with care by someone the community trusts — because the conversation that forms around those dishes is part of the gathering itself, and an opportunity to train the next generation of cooks.

From a series of Mastodon posts by Tao dated April 27, 2026, not part of this lecture. This site found it more accessible than the slide version, so it's included here.

In that same thread, he made an observation sharper than anything on the slides: the massive acceleration in proof generation has not actually produced a corresponding acceleration in mathematical progress itself.

He also noted a side effect: a problem "solved" by AI but understood by no one may actually kill others' interest in pursuing it. After all, it's been "solved" — even though no human understands the solution.

Recommendations

So what should mathematicians do?

Since the bottlenecks are in the later steps, that's where the effort should go.

He recommended the Leiden Declaration as a starting point. The initiative went live June 2 of this year, beginning with a workshop at Leiden University in September 2025, drafted by a working group of sixteen mathematicians from institutions including Cambridge, Columbia, Oxford, Leiden, and ETH Zurich. It has already received endorsement from the International Mathematical Union — the same organization hosting this congress.

Tao picked four clauses and added three comments of his own.

Clause 1Disclose tool use
Transparently disclose the use of automated tools, including large language models, machine learning systems, proof assistants, and other mathematical software. Include a "Tools and compute resources disclosure" section in papers. When reviewing, follow the publisher's rules; if AI use is permitted, disclose how you used it and take responsibility for your substantive comments.
Tao's commentWe need to avoid the worst case: authors secretly use AI, then hide it to avoid peer criticism. Responsible disclosure should be normalized.
Clause 2Support the needs of review
Using AI when writing papers introduces content that makes review harder. Make it easier for peers to review your work by disclosing tool use, providing precise and complete citations of prior results, and providing formalized proofs when feasible and appropriate.
Tao's commentWe need to de-emphasize proof generation, the race to be first, and re-emphasize proof digestion — exposition, publication, and canonicalization.
Clauses 4 + 6Retain responsibility for correctness · Work on proper attribution
When automated techniques are used in published mathematical research, responsibility for the correctness and adequacy of arguments and results, and for the completeness and accuracy of citations to relevant prior work, rests entirely with the human authors. Automated tools' known limitations in correctly attributing ideas create a corresponding obligation: proactively seek out and acknowledge the sources that made the new result possible; when satisfactory attribution cannot be achieved, state that clearly in the publication.
Tao's comment — his rule of thumbIf authors cannot convincingly demonstrate that they can give a clear, expert-level, correct, and properly attributed account of their result, then the result should not be published.

Worth noting: the Leiden Declaration is much broader than the four clauses Tao drew on. It has dedicated sections on AI in warfare, mass surveillance, undermining democracy, and environmental costs, calling for stronger public oversight of the AI industry — one clause aimed at policymakers is literally titled "Don't believe the hype." This lecture only used the operational parts. He was talking about how the mathematical community should do its own work.

He made two disclosures himself, in the slides

The footnote on the first page reads: all the em-dashes in these slides were typed by hand. (Em-dashes are now often treated as a telltale sign of AI writing.)

On the "normalize disclosure" slide, the footnote reads: this slide uses AI tools to autocomplete text and generate figures.

Neither was in the body of the slides. Both were just in the footer.

Finally

Problem solving, he said, is just one facet. The same analysis needs to be done for teaching, mentoring students, hiring, grant applications, and public communication. In some areas — especially education and training — the human side of the work needs to be emphasized, with AI tool use strictly limited. In others, the field should proactively define how to integrate these tools into workflows on our own terms. And new workflows and infrastructure are needed to supplement traditional ones — but that's another lecture.

His final line to the audience: our community needs to sit down together and have an open, honest discussion about AI capabilities and our goals and values.

The last page of the talk's main body, he added no comment — just Leiden Declaration clause 7:

Screenshot of the original text of Leiden Declaration clause 7: Participate in public discourse
Slide 51, the last page of the talk's body. Only this clause, no commentary. English text below.
Clause 7Participate in public discourse
Mathematicians have a responsibility to support serious science journalism and to participate in public discourse, explaining AI-assisted methods and results and putting them in proper context. This matters especially within our own subfields, where assessing the depth, difficulty, and significance of a result requires specialized knowledge. Furthermore, we encourage mathematicians to seek opportunities to collaborate with and support other researchers and creators facing similar challenges.
The closing slides also listed a few new workflows and infrastructure he considers worth watching: Mathlib (Lean's mathematical library), the Erdős Problems website, a crowdsourced database for optimizing constants that he initiated, and the public competitions from the SAIR Foundation he co-founded. One item read "Mathematical Discourse," followed by TBA — not yet announced.
Source
Mathematics in the age of AITerence Tao · ICM 2026 public lecture·Slides (PDF)·2026-07-24
About this piece
The two annotated paper photos are from slide 33; the second is a zoomed detail cropped by this site. The five-step pipeline and goal-divergence diagrams are Chinese versions redrawn by this site from slides 22, 24, 26, 29, 37, and 43; the three-speed schematic is original to this site and contains no empirical data. First Proof review details, problem domains, and four-tier ratings come from its second batch report (arXiv:2606.18119); the slides contain only a one-line conclusion. The per-problem cost range Tao cited in the lecture was $10–$1,000; the report's actual figures run from $8 to $951. Note: Tao is a team member of one of the four systems tested (UCLA Moonshot Harness); the slides do not mention this. The food analogy is from his Mastodon post of April 27, 2026, not part of this lecture.