I am tired of two kinds of AI-in-science coverage. The first is breathless: AI is solving everything, it will replace scientists, humanity is about to leap forward by decades. The second is reflexively dismissive: it's just autocomplete, it can't do real reasoning, it will never replace human creativity.
Terence Tao cuts through both of these takes with precision. He is the right person to do it.
On February 10, 2026, Tao — delivered a lecture at IPAM's AI for Science Kickoff at UCLA titled "Machine assistance and the future of research mathematics." Tao holds the Fields Medal, mathematics' highest honor. He has been actively experimenting with formal proof assistants and LLMs in his own research. He has no AI company stock, no consulting contract with a startup, no incentive to hype. When he says something is working, it deserves attention.
The abstract of the talk is worth quoting in full: "A variety of machine-assisted ways to perform mathematical assistance have matured rapidly in the last few years, particularly with regards to formal proof assistants, large language models, online collaborative platforms, and the interactions between them. We survey some of these developments and speculate on how they will impact future practices of mathematical research."
Note the precision. Not "AI is revolutionizing mathematics." Not "AI cannot do mathematics." Machine-assisted ways to perform mathematical assistance have matured. That is a scientist being careful about what is actually true.
Let me explain what formal proof assistants actually are, because they are the most technically interesting part of this story. Systems like Lean and Coq allow mathematicians to write proofs in a formal language that a computer can verify with absolute certainty. Every logical step must be explicit. The computer does not check whether the proof seems right — it checks whether every step is valid according to the rules of logic.
This is genuinely powerful. Mathematical proofs are long, complex, and occasionally contain errors that go undetected for years. Formal verification eliminates that possibility. Tao himself has been involved in formalizing significant mathematical results in Lean.
Where LLMs fit into this picture is more nuanced. They are useful for suggesting proof strategies, identifying relevant existing results, and generating candidate steps that a mathematician then evaluates. They are not reliable for generating correct proofs independently. A large language model does not understand mathematics in the way a mathematician does — it has learned patterns from enormous amounts of mathematical text, and those patterns are often useful, but they can also confidently suggest steps that are simply wrong.
The combination — LLM for ideation and suggestion, formal proof assistant for verification — is more than the sum of its parts. Tao's observation is that these tools together are beginning to change how mathematical collaboration happens, enabling larger-scale collaborative projects and making it easier to verify complex results.
What he is not claiming is that AI will produce novel mathematical intuition — the kind of creative leaps that lead to genuinely new theorems. That remains human territory. The distance between pattern-matching on existing mathematics and making a conceptual breakthrough is, as Tao implicitly recognizes, still vast.
But the tools for checking, verifying, and assisting with the mechanical parts of proofs are genuinely mature. And that is worth reporting honestly, without the hype and without the dismissal.
