Terence Tao on AI and Mathematics: Formal Proofs, Human-AI Collaboration, and the Road Ahead

Fields Medalist Terence Tao — widely regarded as one of the greatest mathematicians of our time — recently published an article titled Mathematics in the Age of AI, which sparked lively discussion on Hacker News (107 upvotes, 46 comments). As a researcher working at the forefront of mathematics who is also deeply involved in AI-assisted proof practices, Tao's perspective is especially worth paying attention to. He is neither a blindly optimistic tech evangelist nor a stubbornly skeptical traditionalist, but rather someone who examines AI's profound impact on this ancient discipline with the rigor characteristic of a mathematician.

Terence Tao was born in 1975 in Australia to parents of Chinese descent and currently serves as a professor in the Department of Mathematics at the University of California, Los Angeles (UCLA). He was awarded the Fields Medal in 2006 — an honor often called the "Nobel Prize of Mathematics," given every four years exclusively to scholars under 40 who have made outstanding contributions to mathematics. Tao's research spans harmonic analysis, partial differential equations, combinatorics, analytic number theory, and many other fields, making him renowned for an exceptionally rare breadth of expertise. In recent years, he has been active on social media and blogging platforms, openly sharing his firsthand experience with AI-assisted mathematics — including using ChatGPT for research and participating in Lean formalization projects — making him one of the most authoritative voices in discussions about the intersection of AI and mathematics.

How AI Is Changing Mathematical Research

Mathematics has long been considered the pinnacle of human intellectual endeavor, requiring rigorous logical reasoning and deep intuitive insight. Yet with the rapid development of large language models (LLMs) and automated theorem proving tools, AI is gradually making inroads into this domain. Tao points out that AI's current role in mathematics is not about replacing mathematicians, but rather serving as a powerful assistive tool that reshapes the workflow of mathematical research.

Large Language Models (LLMs) such as GPT-4 and Claude are built on the Transformer architecture and learn the statistical patterns of language through self-supervised learning on massive text corpora. In mathematics, LLMs can handle tasks like theorem proving and formula derivation, but their underlying mechanism is probabilistic "next-token prediction" rather than logical deduction from axiomatic systems. This means that when LLMs tackle mathematical problems, they are primarily performing pattern recognition and analogical reasoning — extracting structured patterns from the vast body of mathematical text in their training data and recombining those patterns for new problems. This mechanism gives LLMs remarkable flexibility but also introduces a fundamental vulnerability: they cannot guarantee from first principles that every step of their reasoning is logically correct.

Tao draws an analogy between AI's role in mathematics and earlier tool revolutions throughout history. From logarithm tables and slide rules to electronic computers and computer algebra systems (such as Mathematica), each advance in tooling has dramatically expanded the boundaries of what mathematicians can achieve. A Computer Algebra System (CAS) is a software system capable of performing symbolic mathematical operations — unlike purely numerical computation, it can precisely manipulate mathematical expressions, simplify formulas, and find analytical solutions to equations. Mathematica (launched by Stephen Wolfram in 1988) is one of the most prominent commercial CAS platforms; other important systems include Maple and SageMath. These tools have vastly accelerated mathematicians' work in integral computation, series expansion, matrix operations, and more. By placing CAS alongside AI tools, Tao makes the point that mathematicians' acceptance of computational tools has been a gradual process: each new generation of tools initially triggered the question "Is this still real mathematics?" but was ultimately embraced by the mainstream mathematical community because these tools freed up cognitive resources, allowing mathematicians to focus on higher-level creative thinking. AI-assisted tools are the latest link in this chain, but what makes them unique is that they touch for the first time on the most fundamental aspects of mathematics — "reasoning" and "proof" — rather than being limited to numerical computation or symbolic manipulation.

The history of Automated Theorem Proving (ATP) dates back to the 1950s. In 1956, the "Logic Theorist" program developed by Allen Newell, Herbert Simon, and Cliff Shaw successfully proved 38 theorems from Principia Mathematica. Subsequently, automated reasoning systems based on the Resolution Principle made significant progress in the domain of first-order logic. However, traditional ATP systems face the combinatorial explosion problem — as problem complexity increases, the search space grows exponentially. Modern approaches attempt to combine deep learning with traditional symbolic reasoning: for example, Google DeepMind's AlphaProof system successfully solved 4 out of 6 problems at the 2024 International Mathematical Olympiad (IMO), demonstrating the enormous potential of neural network-guided theorem proof search. This "neuro-symbolic" hybrid approach is becoming a frontier direction in AI mathematical reasoning research.

The Rise of Formal Proof Tools

Tao places particular emphasis on the transformative potential of combining formal proof tools (such as the Lean proof assistant) with AI. Traditionally, mathematical proofs are written by humans and reviewed by humans, inevitably leaving room for oversights or containing complex arguments that are difficult to verify. With proof assistants like Lean, mathematical theorems can be fully verified by machine, ensuring that the logical chain is airtight.

Lean is an interactive theorem prover initially developed by Leonardo de Moura at Microsoft Research starting in 2013, with Lean 4 being the widely used current version. It is based on Dependent Type Theory, which treats mathematical propositions as types and proofs as terms of those types (the "propositions as types" Curry-Howard correspondence), thereby transforming mathematical proofs into type-checking problems. Lean's core advantage is that once a proof passes its type checker's verification, there is an extremely high degree of confidence in its logical correctness — independent of any human reviewer's judgment. The Mathlib mathematical library project built around Lean has formalized a vast amount of undergraduate and graduate-level mathematical content, making it one of the largest unified formal mathematical knowledge bases in existence.

Tao himself has led large-scale formalization collaboration projects, decomposing complex theorems into modular tasks that can be distributed among numerous participants (including non-specialists). In 2023, he publicly shared on his blog the experience of formalizing the proof of the PFR conjecture (Polynomial Freiman-Ruzsa conjecture) using Lean. The entire process was completed through crowdsourced collaboration on GitHub in just a few weeks, becoming a landmark case in large-scale formalization efforts. In this process, AI played the role of auto-completion, suggesting proof strategies, and discovering lemmas — significantly lowering the barrier to formalization and potentially compressing what would have taken months into weeks or even days.

A Fundamental Shift in Collaboration: From Artisan Workshop to Industrial Scale

One of Tao's core insights is that AI will transform the scale and collaborative nature of mathematical research. Traditional mathematical research has typically been the work of a few gifted individuals or small teams, because deeply understanding a frontier problem requires extensive specialized knowledge, making effective division of labor difficult.

But when AI and formal tools enter the picture, a grand proof can be decomposed into many relatively independent, verifiable small tasks. Participants don't need to understand the big picture — they only need to complete their local work, while machines ensure the correct assembly of all parts. This is analogous to modular development in software engineering — mathematical research could potentially evolve from an "artisan workshop" model to "industrialized collaboration."

This idea of large-scale collaborative mathematical research isn't entirely new. In 2009, Tao and Cambridge mathematician Timothy Gowers co-launched the Polymath project — an open mathematical collaboration experiment conducted through blogs and wiki platforms. In the Polymath1 project, numerous mathematicians collectively found a combinatorial proof of the Density Hales-Jewett theorem through online discussion, demonstrating the feasibility of collective intelligence in mathematical research. However, a limitation of the Polymath project was that participants still needed substantial domain expertise, and the "granularity" of collaboration was relatively coarse — contributors needed to understand the overall framework of the problem. The introduction of AI and formal tools further refines this granularity: individual contributors may only need to prove a highly localized lemma without grasping the global picture, while machines verify the interface correctness between modules. This represents a qualitative leap from Polymath-style "intellectual brainstorming" to truly engineered, modular mathematical production.

The implications of this shift are profound. It means mathematical research could attract a much broader range of participants — including students, programmers, and even hobbyists — creating an unprecedented form of large-scale crowdsourced mathematical exploration. Tao believes this could give rise to complex mathematical results that would be beyond the reach of any individual working alone.

Limitations and Risks of AI-Assisted Mathematics

Despite his enthusiasm for the prospects, Tao consistently maintains the caution characteristic of a mathematician. He explicitly identifies several clear limitations in AI's current mathematical applications:

• Reliability issues: LLMs are prone to "confidently generating nonsense" — producing proof steps that appear plausible but are actually incorrect. AI hallucination refers to large language models generating content that seems fluent and confident but is actually wrong or fabricated. In everyday conversation, this may be a minor inconvenience, but in mathematics, the danger is amplified enormously. Mathematical proofs require every link in the logical chain to be absolutely correct; a seemingly minor erroneous step can bring the entire edifice crashing down. Even more dangerous is that the erroneous mathematical reasoning generated by LLMs often has extremely high "surface plausibility" — it may correctly cite theorem names, use appropriate mathematical terminology, and mimic reasonable proof structures, while making illegitimate logical leaps or incorrect equivalence transformations at critical steps. Even experienced mathematicians might be misled by such "pseudo-proofs" during quick reviews. This is precisely why Tao emphasizes formal verification as an indispensable "safety net": tools like Lean provide a deterministic correctness judgment mechanism free from psychological biases.
• Lack of genuine understanding: AI excels at pattern matching and recombining existing knowledge, but still falls short when it comes to deep innovation requiring entirely new conceptual breakthroughs. True mathematical insight — those "aha" moments — remains exclusively in the human domain for now.
• Dependency risks: Over-reliance on AI tools could erode mathematicians' own reasoning training, posing new challenges particularly for the development of young scholars.

Tao emphasizes that AI should be viewed as a partner that augments human capabilities, not a replacement. Mathematicians need to learn to harness these tools, understand the boundaries of their capabilities, and fully leverage their value in appropriate contexts.

Implications for Mathematics Education and the Future

Tao's reflections also extend to education. When AI can assist with or even complete many computational and proof tasks, where should the focus of mathematics education shift? He is inclined to believe that future mathematical training should place greater emphasis on cultivating meta-skills — the ability to ask good questions, judge the reasonableness of results, and collaborate effectively with tools — rather than purely mechanical computation skills.

Regarding the future landscape of mathematics, Tao envisions a new paradigm of "human-AI collaboration": human mathematicians take charge of proposing research directions, building mathematical intuition, and maintaining strategic oversight, while AI handles tedious details, explores vast search spaces, and verifies logical rigor. Together, this combination holds the promise of cracking long-standing unsolved mathematical problems.

Conclusion

The value of this article lies in the fact that it comes from a top scholar who is truly at the research frontier and has personally practiced AI-assisted mathematics. Tao sees both the enormous opportunities AI brings — expanded collaboration scales, the popularization of formal verification, and leaps in research efficiency — while also remaining clear-eyed about its limitations and potential risks.

For the broader technology and AI community, Tao's perspective offers a rare, balanced, and profound frame of reference: AI is not the terminator of mathematics, but rather the latest major tool revolution in mathematics' long evolutionary journey. The real question is not "Will AI replace mathematicians?" but "How will mathematicians work with AI to redefine the boundaries of mathematical research?" In this age of AI, what may remain most precious is still human curiosity, creativity, and judgment.