Terence Tao

I decided to convert one of the points in my ICM 2026 slides https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf into a meme format.

The advent of capable AI tools has highighted a variant of Simpson's paradox https://en.wikipedia.org/wiki/Simpson%27s_paradox : a technological advance can improve the quality and volume of each individual's output, and yet the average quality (signal-to-noise ratio) of the aggregate output can deteriorate as a result.

I can illustrate this phenomenon with a toy numerical model (all numbers here are made up to simplify the exposition). Let's take the task of solving a mathematical problem, and then writing it up properly to a professional standard. (Here for simplicity I ignore the intermediate stage of verifying the proof.) Before the advent of an AI, suppose that it took on the order of six months to generate a solution to the problem, and then an additional month to write things up. This was a lot of work, and so relatively few projects would even get as far as the solution generation stage. But, on the other hand, an author who has already invested six months on the problem would usually be willing to invest the additional month to write things up for the added value; few projects would be abandoned between the proof generation and the proof exposition stage. (1/4)

In my recent ICM talk in https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf, I highlighted the five stages of proof development and maturation: proof generation, proof verification, proof exposition, proof publication, and proof canonicalization. This developmental cycle is somewhat analogous to the developmental cycle of a living being, from an infant, to a child, to an adolescent, and finally to an adult; cf. Cedric Villani's popular book "Birth of a Theorem". As mentioned in those slides, it is the final "adult" stage of having canonical, textbook proofs that is the most valuable for applications (and for generating further proof methods).

To continue this analogy, the authors of a proof have traditionally played a role somewhat similar to that of parents or caretakers, first bringing a proof into the world, and then investing significant effort into growing and improving that proof in various dimensions, such as readability, conceptual clarity, or insightfulness. The acclaim that mathematicians have historically received for creating a difficult new proof is based in part on this expectation of continued investment in the development of that proof, and its surrounding ideas and theory. (1/2)

I had recently made an analogy between the developmental cycle of a proof and the developmental cycle of a child, and noted the strong cultural preference for a "traditional" parenting model in which a single set of parents is responsible for all aspects of the childrearing process, from conception all the way to adulthood. In a similar vein, we have a traditional authorship model in which a single set of authors is responsible from a proof all the way from generation up to at least publication, although we do normalize the phenomenon of a different set of authors then writing the definitive textbook on the subject.

But, pursuing the analogy further: in the case of parenting, we have a number of social, legal, and/or medical mechanisms, such as in vitro fertilization, surrogate mothers, adoption agencies, godparents or foster parents, divorce and remarriage, or child protective services, to handle cases in which the traditional parenting model, for one reason or another, is not viable. These mechanisms can be controversial, and are not necessarily a complete substitute for a traditional parenting model, but it is still better to have them than to rely on completely ad hoc procedures when traditional parenting becomes unavailable.

I am reluctantly coming to the conclusion that some similar formal mechanisms may be needed for mathematical results in the age of AI. In particular, we may need a mechanism in which an author is willing to take a proof through some partial stage of the proof development cycle (generation, verification, exposition, publication, and canonicalization) but then explicitly "gives it up for adoption" for a different set of authors to continue with.

As an experiment, I directed a coding agent to sort through recent #arXiv posts for similarity in topic or keywords to my own research papers, with additional weighting for papers authored by my former collaborators or mentees (such papers are marked with a star in the lists provided below). I also asked the agent to assess the degree of AI assistance in each paper using robot emojis, with one emoji denoting minor assistance, two denoting major assistance, and three denoting near-total automation. (A computer emoji is also used to indicate more traditional computer assistance, e.g., in numerics.) The lists produced by the agent for the months of July and of August respectively are provided below. (It is important to stress that the AI-generated rankings here are based on proximity to my own interests, and should not be regarded as an absolute ranking of importance of the result.)

The generation of these listings is highly unscientific and tailored to my own personal preferences (and there was at least one annotation error, in that the author Van Khu Vu was confused with my collaborator Van Ha Vu), but it does indicate to me the increasing adoption of AI assistance, at least in my own fields of interest.

I have uploaded my slides for the public #ICM lecture talk I just gave at https://teorth.github.io/tao-web/slides/age-of-ai-icm-2026.pdf . The recording will likely be forthcoming in a day or two.

In the meantime, I have decided to use an AI to collate and summarize a hundred or more previous posts, interviews, or videos I gave on the topic of AI, and also to "interview" me about any topics not covered in that past material. I instructed it to be somewhat hard hitting with its interview, and I was somewhat surprised by the results of that instruction, which one can find at https://teorth.github.io/tao-web/ai-views-interview.html . The summary can be found at https://teorth.github.io/tao-web/ai-views.html . I will update it once the recording of the current lecture is available.

Announcing the Palomar registry of Lean formalized mathematics: https://palomar-registry.org/ . See also my blog announcement at https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ and the Lean Zulip channel at https://leanprover.zulipchat.com/#narrow/channel/621638-Palomar.

#SAIR is launching a Lean Kernel challenge on September 15, with pre-registration now open at https://competition.sair.foundation/competitions/lean-kernel-challenge . The precise rules and format are still being finalized, but the competition is aimed at finding the fastest way to perform (verified) computations in Lean of benchmark mathematical challenges, such as computing digits of pi or computing a hash.

The long-awaited "Leiden Declaration" on Artificial Intelligence and Mathematics is now live and seeking signatories: https://leidendeclaration.ai/

This declaration stemmed from a workshop in Leiden University last September on "Mechanization and Mathematical Research", where it became clear how important it was in the age of AI to make explicit the goals and values of the mathematical community. Many of these goals have long been left implicit, being disseminated informally from advisor to student, or through mechanisms such as the peer review process. So long as the community was largely driven by internal decisions, this implicit system sufficed, and we only needed to share a few explicit goals with the broader public, such as working on unsolved problems, discovering new mathematical phenomena, or applying mathematics to the sciences or other real-world situations.

But in an era where increasingly powerful AI can be set to optimize (or over-optimize) many of the goals that are explicitly presented to them, such an informal state of affairs becomes inadequate, and so the Leiden working group gathered extensive input from the mathematical community to find consensus on what we truly value in mathematics, and how we recommend individual mathematicians, mathematical institutions and external organizations to act. I myself contributed some feedback to an early version of the declaration, but was not part of the working group. (1/2)

"I have only made this letter longer because I have not had the time to make it shorter." (Blaise Pascal, often misattributed to Mark Twain)

I have previously written about the evolving impedance mismatch between proof generation, proof verification, and proof digestion in mathematics. This has led to the following unintuitive breakdown of monotonicity, already noticed by Pascal as far back as 1657: it is now easier to generate long correct proofs than it is to generate short correct proofs! However, it is far more challenging to *verify* and *digest* such proofs, thus exacerbating the impedance mismatch.

I have encountered this phenomenon personally with the Integrated Explicit Analytic Number Theory Network (IEANTN) project https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ . As part of this project, a large number of lengthy technical papers in explicit analytic number theory are to be formalized. This was a tedious task, involving a lot of numerical verifications, and until recently was the bottleneck for the project; I could assign individual lemmas to formalize as tasks, and expect it to take weeks before a volunteer would claim them and prove them. Because the task of formalization by hand was difficult, the volunteer would naturally strive to make the proofs short, efficient, and natural, and as such they were easy to review by myself. (1/3)

A new AI benchmarking math challenge, inspired by FirstProof: the Ramanujan Challenge https://www.ramanujanmachine.com/ramanujan-challenge/ , which is a call for AI-generated proofs of 10 Ramanujan-type numerical identities whose proofs are known to the authors of the challenge, but are currently not public. Submissions are accepted until August 1, 2026.

My talk on "New Mathematical Workflows" at Stanford last week is now online: https://www.youtube.com/watch?v=Uc2zt198U_U

One key recommendation in the talk is to now de-prioritize the historical emphasis on competing to be the first to provide a proof for a given unsolved mathematical problem. When we were in the proof scarcity era, the "local" goal of obtaining any proof at all for a problem was fairly well aligned with the more "global" goal of collectively advancing our understanding of mathematics as a community. However, now that the ability to optimize this local goal has increased rapidly to the point of "proof abundance", we have now reached the point where Goodhardt's law https://en.wikipedia.org/wiki/Goodhart%27s_law has kicked in, and further unrestricted overoptimization of this goal will no longer create genuine mathematical progress, and may in fact inhibit it in various ways. However, there is scope for more controlled, and still meaningful, optimization in this direction along carefully chosen workflows (such as mathematics competitions) that are specifically designed to accommodate heavy AI use.

John Jones, Jen Paulhus, David Roe, Andrew Sutherland, and I have launched the third SAIR challenge, this time aimed at attacking the notorious inverse Galois problem: https://competition.sair.foundation/competitions/igp24/discoveries https://terrytao.wordpress.com/2026/06/16/third-sair-competition-inverse-galois-challenge/ . We are focusing on the degree 24 case, which is almost the first unsolved case (excluding the notorious problem of whether the Mathieu group M_{23} is a Galois group).

The first stage of the competition is focused on "brute forcing" as much of the 25000 Galois groups as possible (taking full advantage of modern AI tools), before launching a more focused second stage in which we make a more mathematically sophisticated attack on those groups that end up being resistant to brute force methods.

I wrote a blog post on the proposed rule changes for the administration of federal grants: https://terrytao.wordpress.com/2026/06/09/on-the-proposed-rule-changes-to-the-administration-of-federal-grants/

The results of the First Proof "second batch" are now out: https://1stproof.org/assets/docs/report.pdf

Ten research-level questions (many being part of forthcoming papers) were tested locally by the First Proof team against four AI harnesses, including one from my UCLA team, and then the submissions refereed by experts. In aggregate, 7 of the 10 problems were deemed to have at least one publication-level solution generated between the four harnesses.

The UCLA harness had a somewhat mixed performance: 2 problems solved at an acceptable level, 3 more reaching a level roughly equivalent to a "minor revisions needed" submission to a journal, and with either "reject" or "major revisions needed" on the other 5. We did perform slightly better than the out-of-the-box frontier model, but at much higher compute costs (a few hundred dollars per question, rather than tens). Still, some of the solutions generated contained some interesting novelty.

Significant weaknesses in our own harness revealed by the testing included the general failure to cite appropriate relevant literature, and having poor exposition (one solution in particular, while correct, was flagged by referees for spending far too much time on trivial steps and not enough on the key components of the argument). These look like addressable issues for our harness, and we also plan to incorporate more use of tools (such as symbolic computation and literature search) which were used more effectively by one of the competing teams. Improving the compute efficiency will also need to become more of a priority.

While our own performance was slightly disappointing, I hope to see many more scientifically rigorous benchmarking exercises like this in the future.

A few weeks ago, I recieved a detailed referee report on a lengthy paper my coauthors and I submitted, with many suggested corrections (both minor and major) spread out over many sections. We agreed to each claim some of the sections to revise based on the recommendations of the referee, and (because we were using Github as our version control system) were able to easily merge together all the revisions and have them done in a matter of days.

Today, I received a response from the referee who was largely satisfied with the changes, but had a dozen further minor corrections (mostly of the nature of typos or LaTeX labeling issues) that still needed to be addressed. This time around, I uploaded the report to the Claude Code agent, which was able to inspect the report, the LaTeX source, and the PDF version of the paper, identify the corrections, and propose unambiguous fixes for eleven of the twelve corrections (pointing out one typo on the referee's part in the process), while for the twelfth correction it offered two possible viable fixes. I then reviewed all proposed changes, made the selection for the twelfth fix, and asked Claude to implement them all; the entire process took less than fifteen minutes.

If I were to do the first round of revisions again, I think I would ask an agent to go through the report and identify all of the minor issues (at a typo level) that it could unambiguously fix, review and implement these fixes, and then isolate the more substantive comments that required human attention, before splitting the work amongst the co-authors as before.

Alberto Alfarano, François Charton, Yongzheng Jia, Kristin Lauter, Cathy Li, Emily Wenger and I are launching a second challenge at SAIR, this time focused on seeing how efficiently neural networks can execute simple modular arithmetic operations : https://competition.sair.foundation/competitions/modular-arithmetic-challenge/overview . A more detailed blog post is at https://terrytao.wordpress.com/2026/06/08/modular-arithmetic-challenge/