When the world's best mathematician changes the way he thinks

Imagine a chess grandmaster who, after decades of playing alone against the board, suddenly finds himself with a partner capable of suggesting unprecedented moves — sometimes brilliant, sometimes absurd, but always surprising. This is roughly what Terence Tao has been experiencing since he incorporated artificial intelligence into his daily mathematical practice. And when Tao speaks, the global mathematical community listens.
Who is Terence Tao? In two words: the most admired living mathematician of his generation. Australian-American, born in 1975, he received the Fields Medal in 2006 — the mathematical equivalent of the Nobel Prize, awarded every four years to researchers under forty for work judged exceptional. Tao works across fields as varied as number theory, harmonic analysis and partial differential equations. He is not a mathematician confined to a single lane: he is someone who breaks through the walls between disciplines with disconcerting ease.
For several years now, he has also been one of the most serious and nuanced voices on the integration of AI into mathematical research. He recently published a summary of his experiences and gave several interviews to detail his observations. The picture he paints is far from that of a naive enthusiast — or of a stubborn skeptic.

AI as a research assistant: neither oracle nor ordinary tool

To understand what AI is changing in a mathematician's work, we first need to understand what that work looks like. Contrary to what is often imagined, a top-level mathematician does not spend his days calculating. He looks for structures, hidden regularities, logical paths that connect truths to one another. A mathematical proof is a chain of arguments in which every link must be irrefutable — a single flaw, and the whole thing collapses.
In this context, large language models — AI systems trained on vast corpora of text and capable of producing coherent language, such as GPT-4 or its equivalents — at first seemed poorly suited to mathematics. Mathematics demands absolute precision; these systems, on the other hand, are known to "hallucinate," that is, to produce false statements with unshakable confidence.
Yet Tao reports something unexpected: used correctly, these tools can act as an intellectual sparring partner — a training partner. Not to validate proofs (they are not reliable for that), but to quickly explore leads, reformulate a problem from a different angle, or identify analogies with known results in other fields. In short: to speed up the exploration phase, even before rigor comes into play.

"AI does not replace the proof. But it can change the way we search for what to prove."

—

What AI does to mathematical cognition

Where Tao becomes truly fascinating is when he talks not about his results, but about his mental processes. Working regularly with AI tools, he says, changes the way problems are formulated. You learn to break a complex question down into more precise sub-questions — because AI responds better to well-targeted queries than to vague requests. In doing so, you sharpen your own thinking.

This is a well-known phenomenon in cognitive psychology: the tool shapes the user as much as the user shapes the tool. The calculator changed the way we think about numerical computation. Dynamic geometry software changed the way we explore figures. Generative AI is changing the way we explore the space of mathematical possibilities.

But this transformation also raises an uncomfortable question: if AI suggests a research direction, and the mathematician follows it to a valid proof, to whom does the intuition belong? Is mathematical creativity still entirely human? Tao does not settle the matter — and that is precisely what makes his position interesting. He is not trying to reassure. He observes.

Assisted formal proof: a work in progress

Beyond large language models, Tao is also interested in another family of tools: formal proof assistants, such as Lean or Coq. This software mechanically verifies every step of a mathematical proof — somewhat like a spell-checker, but for pure logic. If a step is false or incomplete, the system flags it immediately.

Tao has taken part in collaborative projects using these tools, in particular to formalize complex results with the help of dozens of online contributors. The experience showed him that formalization forces one to spell out assumptions that are usually left implicit — which can reveal unsuspected gaps, even in proofs believed to be solid.

The long-term stakes are considerable: if the exploratory power of large language models could be combined with the verifying rigor of formal proof assistants, we would have a tool capable both of proposing leads and of validating them. We are not there yet — but the trajectory is visible.

What this changes for students and young researchers

For a mathematics student or a young researcher, the implications are immediate and practical. First point: AI can be a tutor available around the clock, able to explain a concept from ten different angles until one of them clicks. This is valuable, especially at moments when you hesitate to bother a thesis advisor with a question that seems "too basic."

Second point, a more delicate one: the risk of short-circuiting cognitive effort. Learning mathematics is, in large part, learning to stay stuck — and to work one's own way out. This uncomfortable friction is the engine of intellectual development. If AI systematically provides the emergency exit, it can deprive the learner of the benefit of the obstacle. Tao insists on this point: the tool must amplify thinking, not replace it.

Third point: the skills that matter are changing. Knowing how to ask an AI system the right questions — what is called prompting, the art of formulating effective queries — is becoming a skill in its own right. Knowing how to critically evaluate a response generated by AI, identify its errors, and extract what is useful from it: these are abilities that mathematics education will need to build in explicitly.

Neither utopia nor dystopia

What emerges from Tao's assessment is a stance rare in debates about AI: neither the starry-eyed enthusiasm that proclaims the end of human work, nor the rigid resistance that refuses to see what is actually changing. Mathematics, he says in essence, remains a profoundly human activity — but the context in which that activity takes place is transforming at an unprecedented speed.

The real question is not "Will AI replace mathematicians?" — the answer is no, at least for everything that touches on creativity, deep intuition, and the sense of what is beautiful or important in mathematics. The real question is: "How do we train mathematicians able to work with these tools without becoming dependent on them?" And to this question, even Terence Tao does not yet have a definitive answer. Which, in a way, is reassuring.

Key takeaways

  • Terence Tao is a Fields Medalist — the "Nobel of mathematics" — and he has been using AI in his research for years: if he takes it seriously, the subject truly deserves to be taken seriously.
  • AI does not prove things in the mathematician's place: it helps explore leads before rigor comes into play — like a GPS that suggests routes, but you're the one driving.
  • Using AI regularly changes the way we think about problems — not just the way we solve them. The tool reshapes the brain that uses it.
  • Software exists that can check every step of a mathematical proof the way a spell-checker checks every word — and it sometimes reveals flaws in proofs everyone believed to be solid.
  • For students, the real danger of AI in mathematics is not cheating: it is never getting stuck anymore — and therefore never learning to work one's own way out.

For math enthusiasts

One of the most rigorous applications of AI in mathematics concerns formal proof verification. In this framework, a proof is not written in natural language but in a formal language understood by software — Lean 4, for example. Every step of the proof is an instruction that the system checks mechanically according to the rules of logic and the chosen axioms (generally those of dependent type theory, or of Zermelo-Fraenkel set theory). Tao contributed to the Polynomial Freiman-Ruzsa (PFR) project, in which a complex combinatorial proof was entirely formalized in Lean within a few weeks through a distributed collaboration. What is mathematically remarkable is that the formalization forced the authors to spell out intermediate lemmas that were implicit in the original proof, revealing the fine structure of the reasoning. In the long run, the goal is to couple these proof assistants with language models capable of generating proof candidates — what some call autoformalization: the automatic translation of natural-language statements into verifiable formal proofs.
Source: German-language article in Der Standard