# Terence Tao

> Source: https://aiwiki.ai/wiki/terence_tao
> Updated: 2026-07-24
> Fact-checked: 2026-07-24
> Categories: AI for Science, Mathematics, People
> License: CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) - attribute to "AI Wiki (aiwiki.ai)"
> Cite as: AI Wiki. "Terence Tao." aiwiki.ai, 24 Jul 2026. https://aiwiki.ai/wiki/terence_tao
> From AI Wiki (https://aiwiki.ai), the free encyclopedia of artificial intelligence. Reuse freely with attribution.

Terence Tao (born 17 July 1975 in Adelaide, Australia) is a mathematician at the University of California, Los Angeles, where he holds the James and Carol Collins Chair in the College of Letters and Sciences [1][2][5]. He received the Fields Medal in 2006 [3][6] and is known outside his own subject for the Green-Tao theorem, proved with Ben Green in a 2004 preprint, which shows that the prime numbers contain arithmetic progressions of every finite length [2][4].

Since 2023 Tao has also written extensively in public about artificial intelligence and its use in mathematics. His involvement takes three fairly distinct forms. He organizes large formalization projects in the [Lean](https://aiwiki.ai/wiki/lean) proof assistant, he publishes hands-on evaluations of frontier models applied to genuine research tasks, and he contributes problems, commentary and infrastructure to efforts that measure machine performance on [mathematical reasoning](https://aiwiki.ai/wiki/mathematical_reasoning) [7][9][13][15].

What distinguishes his commentary is that it is dated, specific and revised. In September 2024 he compared working with a frontier model to advising a "mediocre, but not completely incompetent" graduate student; by June 2026 he was reporting that autoformalization tools could finish virtually every formalization task he issued within hours [15][23]. He has also been publicly critical of uncontrolled benchmark comparisons, and of his own group's results when they came back weak [18][21].

## Background and mathematical career

Tao competed in the [International Mathematical Olympiad](https://aiwiki.ai/wiki/international_mathematical_olympiad) three times as a schoolchild, first at the age of ten [3], taking a bronze medal in 1986, a silver in 1987 and a gold in 1988, the year he turned thirteen [1][3]. He completed a B.Sc. (Hons) at Flinders University in December 1991 and an M.Sc. there in August 1992 under Garth Gaudry, then a Ph.D. at Princeton University in June 1996 under Elias Stein [1][28]. He joined UCLA in 1996 as a Hedrick Assistant Professor and has been a full professor there since 2000 [1][2].

The Clay Mathematics Institute, which appointed him a Clay Research Fellow in 2001 and gave him its Clay Research Award in 2003, describes his work as split between real-variable harmonic analysis, the analysis of nonlinear dispersive and wave equations, and combinatorics arising from representation theory and symplectic geometry [28]. Alongside the Fields Medal he was named a MacArthur Fellow in 2006 [2], and he served on the President's Council of Advisors on Science and Technology (PCAST) during the Biden administration [5]. He writes the blog What's new and has posted to the Mastodon instance mathstodon.xyz since November 2022, where much of his commentary on AI appears [30].

## Formalization and the Lean projects

### The Polynomial Freiman-Ruzsa formalization

In November 2023, Tao, Timothy Gowers, Ben Green and Freddie Manners posted a proof of a conjecture of Katalin Marton, widely known as the polynomial Freiman-Ruzsa conjecture, in characteristic 2 [8]. Days later Tao announced a project with Yael Dillies and Bhavik Mehta to formalize the argument in Lean 4, coordinated through a GitHub repository and Patrick Massot's Blueprint tool, which renders a human-readable version of the proof as a dependency graph whose nodes turn green as each step is verified [9][11].

Tao's stated goal was simply to get every bubble in the graph coloured in [9]. He noted that the blueprint structure lets contributors work on different parts of a proof asynchronously, without waiting for earlier stages to be fully formalized [9]. On 5 December 2023 he reported that the project had succeeded after three weeks, with the dependency graph fully green and the Lean compiler confirming that the conjecture followed from the standard axioms [10]. The repository has since been extended to consequences of the result and to sharper exponents [11].

### The Equational Theories Project

On 25 September 2024 Tao proposed a larger experiment: a crowdsourced attempt to settle every implication among the 4,694 equational laws of order at most four, meaning the laws on magmas that use the magma operation at most four times [12][13]. In the announcement he argued that proof assistant languages such as Lean "provide a potential way to overcome these obstacles, and allow for large-scale collaborations involving professional mathematicians, the broader public, and/or AI tools", while warning that such tools "can 'hallucinate' plausible-looking, but nonsensical arguments, which therefore need additional verification" [12].

The Equational Theories Project (ETP) launched that same month, maintained by Tao with Pietro Monticone and Shreyas Srinivas [14]. Its primary goal was reached on 14 April 2025, when all 22,028,942 implications between the 4,694 laws had been determined, with every proof or refutation formalized in Lean [13]. Over fifty contributors took part, coordinating through a channel on the Lean Zulip forum and a single GitHub repository [13]. The report contrasts this with the earlier Polymath model of open online collaboration, which required human moderators to review and integrate contributions and which the authors judged would not scale to a project demanding the verification of over twenty million statements [13]. The 4,694 laws resolved into 1,415 equivalence classes [13].

The project's own report is unusually candid about where machine learning helped and where it did not. Most of the automation came from conventional [automated theorem provers](https://aiwiki.ai/wiki/automated_theorem_proving) and related solvers, among them Vampire, Prover9 and Mace4, the SMT solver Z3 and the SAT solver Kissat, not from neural systems [13]. [Large language models](https://aiwiki.ai/wiki/large_language_model) were used "in a fairly limited fashion": for writing the code behind the project's visualization tools, for autocompletion during formalization via [GitHub Copilot](https://aiwiki.ai/wiki/github_copilot), and in one case where [ChatGPT](https://aiwiki.ai/wiki/chatgpt) guessed a complete rewriting system for a particular law that could then be formally verified [13]. On the hard cases, the report states, "we found that LLMs did not provide useful suggestions beyond what the human participants could already propose", and the project "largely moved away from the use of such LLMs" [13].

One machine learning result did stand out. A five-layer convolutional network trained on character-level tokenizations of equation pairs predicted implication status on a held-out test set with 99.7 percent accuracy, and still reached 92.2 percent when trained on 0.1 percent of the data [13]. The authors suggest such a model could guide the extension of the graph to order 5 by letting the automated provers focus first on the network's predicted status for each implication [13].

### Continuing work

Tao maintains a Lean companion to his textbook Analysis I as a public repository [26], and by mid-2026 was reporting a qualitative change in tooling. He is one of the organizers of the Integrated Explicit Analytic Number Theory Network, an IPAM project at UCLA that aims to crowdsource the formalization of the computational parts of papers in explicit analytic number theory [31]. Writing about that project on 21 June 2026, he said that "autoformalization has reached the point where virtually every formalization task I had issued could be completed within hours", leaving its queue of unclaimed formalization tasks essentially empty [23]. The tools, he noted, "tended to create quite bloated proofs, often hundreds of lines longer than what a human would choose to do, with a lot of redundancy, with many lemmas not stated at the natural level of abstraction"; since each such proof adds tens of seconds to the total build time, the cumulative effect had become noticeable and hard to review [23]. He added a distinction that recurs in his writing: agents can execute a refactor he explains to them, but "they struggle to spontaneously discover such refactors on their own" [23].

## Public evaluations of AI systems

### 2023: a forecast

In an essay for Microsoft's AI Anthology published on 12 June 2023, Tao wrote that when integrated with formal proof verifiers, internet search and symbolic math packages, "2026-level AI, when used properly, will be a trustworthy co-author in mathematical research, and in many other fields as well" [7].

### 2024: o1 and the graduate student comparison

On 13 September 2024 Tao posted three experiments with a prototype version of OpenAI's [o1](https://aiwiki.ai/wiki/o1), which he had been granted access to [15]. On a semantic search task that earlier models had answered with "hallucinated nonsense", o1 identified the relevant theorem (Cramer's theorem) and gave what Tao called a perfectly satisfactory answer [15]. On a complex analysis problem the results were "better than previous models, but still slightly disappointing": the model "could work its way to a correct (and well-written) solution if provided a lot of hints and prodding, but did not generate the key conceptual ideas on its own, and did make some non-trivial mistakes" [15].

His summary was the sentence that circulated most widely: "The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, (static simulation of a) graduate student. However, this was an improvement over previous models, whose capability was closer to an actually incompetent (static simulation of a) graduate student" [15]. The parenthetical qualifiers were added on 19 September, and on 16 September he posted an apology for having implied that human graduate students can be ranked on "a static, one dimensional level of 'competence'" [15]. The earlier, weaker performance he was contrasting against was that of [GPT-4](https://aiwiki.ai/wiki/gpt-4)-class models, which he had asked to write up the same complex analysis proof in an earlier experiment [15].

Asked in the same thread to make the comparison concrete, he offered a numerical version: getting useful output from the latest tools still costs "some multiple (but not an enormous multiple now, say 2x to 5x) of the effort needed to properly prompt and verify the output", and he saw "no reason to prevent this ratio from falling below 1x in a few years, which I think could be a tipping point for broader adoption of these tools in my field" [15]. A third experiment asked o1 to break a formalization task in Lean into sublemmas; the model understood the task but produced code with errors, which Tao attributed to training data on Lean and [Mathlib](https://aiwiki.ai/wiki/mathlib) being a year or more out of date [15].

### FrontierMath

Tao was one of four mathematicians quoted by [Epoch AI](https://aiwiki.ai/wiki/epoch_ai) in the paper introducing [FrontierMath](https://aiwiki.ai/wiki/frontiermath), the research-level benchmark posted on 7 November 2024, and he also contributed several problems to it [6]. Shown a selection of questions, he said: "These are extremely challenging. I think that in the near term basically the only way to solve them, short of having a real domain expert in the area, is by a combination of a semi-expert like a graduate student in a related field, maybe paired with some combination of a modern AI and lots of other algebra packages..." [6]. He expected the benchmark to "resist AIs for several years at least", citing the near absence of relevant training data: for many problems, he said, it is "almost nonexistent...you're talking like a dozen papers with relevant things" [6]. At launch, leading models solved under 2 percent of the problems [6].

He also raised the economics. Commenting on systems such as AlphaProof, he observed that "if your amazing tool takes three days of compute off of all of Google to solve each problem...then that's less of a useful tool" [6].

### AlphaProof and the Olympiad

On 26 July 2024, after [Google DeepMind](https://aiwiki.ai/wiki/google_deepmind) announced that [AlphaProof](https://aiwiki.ai/wiki/alphaproof) and [AlphaGeometry 2](https://aiwiki.ai/wiki/alphageometry_2) had together solved four of six IMO problems for 28 of 42 points, one short of the gold threshold [17], Tao posted preliminary impressions [16]. He called it "great work, shifting once again our expectations of which benchmark challenges are within reach of either AI-assisted or fully autonomous methods", judged that "IMO level geometry problems are now effectively a solved problem for specialized AI tools", and qualified that formalizable IMO problems were now "at least somewhat amenable to AI attacks (though currently requiring genuinely significant amounts of compute per problem, and human assistance on the formalization side)" [16]. He suggested the database of generated formal proofs "could be a useful resource if shared more openly", and contrasted the systems with the open [NuminaMath](https://aiwiki.ai/wiki/numinamath) model, which was "fully automated and orders of magnitude more resource efficient" [16].

A year later he set out a longer caution. On 19 July 2025 he noted that the 66th IMO had run without an official controlled competition for AI models, although "several AI companies have submitted solutions to many of the IMO questions, though with no regulation on how much compute or human assistance was used" [27]. In a three-part thread later the same day he laid out a human metaphor: a team of contestants given days instead of hours, allowed tools and internet access, permitted to collaborate, prompted by their team leader, and free to submit only their best solution or none at all, could go from not always reaching even bronze medal performance to reliable gold medal performance without anything about the contestants changing [18]. His conclusion: "in the absence of a controlled test methodology that was not self-selected by the competing teams, one should be wary of making overly simplistic apples-to-apples comparisons between the performance of various AI models on competitions such as the IMO, or between such models and the human contestants", adding that he would not comment on self-reported results whose methodology had not been disclosed in advance [18]. He stressed in an edit that the remarks were not aimed at any single result [18].

## Literature search and the Erdős problems database

In October 2025 Tao set out a general position on where AI would pay off first: the most productive near-term uses in mathematics would come "not from applying the most powerful models to the most challenging problems", but "from using medium-powered tools to accelerate and scale up more mundane and time-consuming, but still essential, research tasks" [19]. The fact that a human expert could in principle have produced the same output "is actually a feature rather than a bug", because it makes the output cheap to check [19].

His worked example was literature review on erdosproblems.com, a database of over a thousand problems attributed to Paul Erdős, roughly 600 of them then marked open [19]. Contributors began running an AI deep research tool across the problem list, with human review before anything was posted [19]. Six problems were reclassified from open to solved as a result, and a dozen or so others gained newly located references [19]. A community GitHub repository for the database is hosted under his account [29]. He also argued that systematic tool use makes negative results reportable: a search that finds nothing is worth recording, and rarely gets recorded when a human does it [19].

## AlphaEvolve and machine-driven exploration

Tao is a coauthor of "Mathematical exploration and discovery at scale", posted on 3 November 2025 with Bogdan Georgiev, Javier Gómez-Serrano and Adam Zsolt Wagner, which applies DeepMind's [AlphaEvolve](https://aiwiki.ai/wiki/alphaevolve) evolutionary coding agent to 67 problems across analysis, combinatorics, geometry and number theory [20]. The system "rediscovered the best known solutions in most of the cases and discovered improved solutions in several", and in some instances generalized results from finitely many input values into a formula valid for all of them [20]. The paper also combines AlphaEvolve with Deep Think and AlphaProof so that proof assistants and [reasoning models](https://aiwiki.ai/wiki/reasoning_models) supply automated proof generation on top of the search [20].

## Benchmarking research-level mathematics

Tao's UCLA group operates one of the AI harnesses evaluated by First Proof, an independent initiative directed by Mohammed Abouzaid that tests AI systems on research-level questions and has the submissions refereed by experts [21][22]. Reporting the second batch on 10 June 2026, Tao wrote that across four harnesses, 7 of the 10 problems received at least one publication-level solution, while his own team's harness solved 2 at an acceptable level, reached roughly "minor revisions needed" on 3 more, and drew rejections or major revisions on the other 5 [21]. The UCLA harness performed slightly better than an out-of-the-box frontier model, but at a few hundred dollars of compute per question rather than tens [21].

He listed the weaknesses the referees exposed without softening them: "the general failure to cite appropriate relevant literature, and having poor exposition", including one correct solution flagged for spending far too much time on trivial steps [21]. He closed by saying he hoped to see many more scientifically rigorous benchmarking exercises of this kind [21].

## Advocacy and everyday use

Tao contributed feedback to an early version of the Leiden Declaration on Artificial Intelligence and Mathematics, which opened for signatures on 2 June 2026, though he was not part of the working group that drafted it [24]. He described its purpose as making explicit the goals and values that the mathematical community had previously left implicit, on the grounds that "increasingly powerful AI can be set to optimize (or over-optimize) many of the goals that are explicitly presented to them" [24].

He also uses the tools for ordinary software work. In July 2026 he reported that a coding agent had ported roughly two dozen of his Java applets from 1999 into working JavaScript "in a matter of hours", that he had found only one minor bug in the ported code, and that the agent had identified two bugs in his original 1999 code that he had not known about [25].

## Selected AI-related activity

| Date | Activity | Outcome |
|---|---|---|
| June 2023 | Essay for Microsoft's AI Anthology | Predicted "2026-level AI" would be a trustworthy co-author [7] |
| November 2023 | PFR conjecture proved, then formalized in Lean 4 | Formalization completed in three weeks [8][10] |
| July 2024 | Commentary on AlphaProof and AlphaGeometry 2 | Called IMO geometry "effectively a solved problem" for specialized tools [16] |
| September 2024 | Hands-on evaluation of OpenAI o1 | "Mediocre, but not completely incompetent" graduate student comparison [15] |
| September 2024 | Launched the Equational Theories Project | 22,028,942 implications resolved and formalized by 14 April 2025 [12][13] |
| November 2024 | Interviewed for and contributed problems to FrontierMath | Expected it to "resist AIs for several years at least" [6] |
| July 2025 | Commentary after the 66th IMO | Warned against uncontrolled model-versus-human comparisons [18] |
| October 2025 | AI-assisted literature review on erdosproblems.com | Six problems reclassified from open to solved [19] |
| November 2025 | Coauthored AlphaEvolve mathematics paper | 67 problems; improved solutions found in several [20] |
| June 2026 | First Proof second batch, UCLA harness | 2 of 10 solved acceptably; weak literature citation and exposition [21] |
| June 2026 | Report on autoformalization | Formalization queue cleared within hours, but proofs bloated [23] |

## See also

- [Lean](https://aiwiki.ai/wiki/lean)
- [Mathematical reasoning](https://aiwiki.ai/wiki/mathematical_reasoning)
- [FrontierMath](https://aiwiki.ai/wiki/frontiermath)
- [AlphaProof](https://aiwiki.ai/wiki/alphaproof)
- [AI gold medals at the IMO 2025](https://aiwiki.ai/wiki/ai_imo_gold_2025)
- [AI for science](https://aiwiki.ai/wiki/ai_for_science)

## References

1. Terence Tao, curriculum vitae, Department of Mathematics, UCLA. https://www.math.ucla.edu/~tao/cv.html
2. MacArthur Foundation, "Terence Tao", MacArthur Fellows Class of 2006. https://www.macfound.org/fellows/class-of-2006/terence-tao
3. "Terence Tao", Wikipedia. https://en.wikipedia.org/wiki/Terence_Tao
4. Ben Green and Terence Tao, "The primes contain arbitrarily long arithmetic progressions", arXiv:math/0404188, 8 April 2004. https://arxiv.org/abs/math/0404188
5. President's Council of Advisors on Science and Technology, member list, Biden White House archives. https://bidenwhitehouse.archives.gov/pcast/members/
6. Elliot Glazer et al., "FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI", arXiv:2411.04872, 7 November 2024 (interviews with mathematicians in section 6). https://arxiv.org/abs/2411.04872
7. Terence Tao, "Embracing Change and Resetting Expectations", Microsoft AI Anthology, 12 June 2023. https://unlocked.microsoft.com/ai-anthology/terence-tao/
8. W. T. Gowers, Ben Green, Freddie Manners and Terence Tao, "On a conjecture of Marton", arXiv:2311.05762, 9 November 2023. https://arxiv.org/abs/2311.05762
9. Terence Tao, "Formalizing the proof of PFR in Lean4 using Blueprint: a short tour", What's new, 18 November 2023. https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/
10. Terence Tao, post on Mastodon announcing completion of the PFR formalization, 5 December 2023. https://mathstodon.xyz/@tao/111526765350663641
11. teorth/pfr, "Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)", GitHub. https://github.com/teorth/pfr
12. Terence Tao, "A pilot project in universal algebra to explore new ways to collaborate and use machine assistance?", What's new, 25 September 2024. https://terrytao.wordpress.com/2024/09/25/a-pilot-project-in-universal-algebra-to-explore-new-ways-to-collaborate-and-use-machine-assistance/
13. Equational Theories Project contributors, "The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale", December 2025. https://teorth.github.io/equational_theories/paper.pdf
14. Equational Theories Project, project home page. https://teorth.github.io/equational_theories/
15. Terence Tao, Mastodon thread on OpenAI o1, 13-16 September 2024. https://mathstodon.xyz/@tao/113132502735585408
16. Terence Tao, Mastodon thread on AlphaProof and AlphaGeometry 2, 26 July 2024. https://mathstodon.xyz/@tao/112850716240504978
17. Google DeepMind, "AI achieves silver-medal standard solving International Mathematical Olympiad problems", 25 July 2024. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
18. Terence Tao, Mastodon thread on AI performance and competition formats, 19 July 2025. https://mathstodon.xyz/@tao/114881418225852441
19. Terence Tao, Mastodon thread on AI-assisted literature review and the Erdős problems site, 16 October 2025. https://mathstodon.xyz/@tao/115385022005130505
20. Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao and Adam Zsolt Wagner, "Mathematical exploration and discovery at scale", arXiv:2511.02864, 3 November 2025. https://arxiv.org/abs/2511.02864
21. Terence Tao, Mastodon post on the First Proof second batch, 10 June 2026. https://mathstodon.xyz/@tao/116727977488589991
22. First Proof, project home page. https://1stproof.org/
23. Terence Tao, Mastodon thread on autoformalization and proof bloat in the IEANTN project, 21 June 2026. https://mathstodon.xyz/@tao/116789373239346609
24. Terence Tao, Mastodon post on the Leiden Declaration on Artificial Intelligence and Mathematics, 2 June 2026. https://mathstodon.xyz/@tao/116681023979910132
25. Terence Tao, "Old and new apps, via modern coding agents", What's new, 11 July 2026. https://terrytao.wordpress.com/2026/07/11/old-and-new-apps-via-modern-coding-agents/
26. teorth/analysis, "A Lean companion to Analysis I", GitHub. https://github.com/teorth/analysis
27. Terence Tao, Mastodon post on the conclusion of the 66th IMO, 19 July 2025. https://mathstodon.xyz/@tao/114877789298562646
28. Clay Mathematics Institute, "Terence Tao", Research Fellows profile. https://www.claymath.org/people/terence-tao/
29. teorth/erdosproblems, "A community database for the problems on the erdosproblems.com site", GitHub. https://github.com/teorth/erdosproblems
30. Terence Tao, profile page (joined November 2022), mathstodon.xyz. https://mathstodon.xyz/@tao
31. Institute for Pure and Applied Mathematics, "Integrated Explicit Analytic Number Theory Network", special project page, UCLA. https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/