Terence Tao

#SLMath, formerly MSRI, has launched the search for the next Deputy Director. This key position is a close advisor to the Director and shares in the internal management of the scientific team and programs at SLMath. This position is ideal for an experienced professional with a PhD in mathematical sciences seeking a new opportunity to leverage their strengths in program and grant management, financial management, and people management.

https://www.slmath.org/jobs#deputydirector

(Disclosure: I am currently the Vice-Chair of the board of trustees of SLMath.)

The ability to make complex distinctions with high accuracy after ingesting a sufficient amount of training data is a signature feature of machine learning algorithms. But humans also have this ability, even if they are not always consciously aware of it. One of my favorite illustrations of this is the learned ability to determine (qualitatively) the temperature of water from its sound, which almost all of us have acquired purely through training data: https://www.youtube.com/watch?v=Ri_4dDvcZeM

We even have the learned ability to accurately predict the next word in a sentence, even when we do not understand the semantic content of the sentence itself. Some (rather frustrated) examples of this occur in the later stages of the classic "Who's on first?" sketch: https://www.youtube.com/watch?v=r9t097tbeT0

This is an expansion of a point I initially wrote in the context of a MathOverflow question https://mathoverflow.net/questions/487041/collaborative-repositories-on-open-problems/487065#487065, but also has relevance to the role of AI in activities such as mathematics where ideation is important.

It is commonly accepted that one of the impediments to further progress in mathematics is a shortage of new ideas. Naively, one can model this hypothesis by proposing that

(number of new ideas) (*)

is the key factor determining the rate of progress, and then try to support efforts to maximize the quantity (*).

However, in the era of increasingly large amounts of AI-generated mathematics, the _quality_ of these ideas becomes increasingly relevant. Only a small fraction of new ideas tend to be good and fruitful ones; a bad idea can actually impede progress by wasting more time than it saves. So, a more realistic model would be that it is the actually the product

(number of good new ideas) * (signal-to-noise ratio of the idea pool) (**)

that is the important factor which is worth maximizing. (This is still a massive oversimplification - for instance, it assumes a binary classification of ideas into "good" and "bad" - but will serve as a minimal toy model that suffices to illustrate the broader points that I wish to make here.) (1/3)

Another post on the #cosmicdistanceLadder instagram of Tanya Klowden and myself, this time comparing the many ways cartographers have projected the (mostly) spherical Earth onto flat planes. No planar projection can faithfully reproduce *all* the geometric features of a sphere, so each projection is a compromise; but some projections are still preferred over others for specific applications. https://www.instagram.com/p/DVC9SvxkXDs

Just a brief announcement that I have been working with #QuantaBooks to publish a short book in popular mathematics entitled #SixMathEssentials, which will cover six of the fundamental concepts in mathematics -- numbers, algebra, geometry, probability, analysis, and dynamics -- and how they connect with our real-world intuition, the history of math and science, and to modern practice of mathematics, both in theory and in applications. The scheduled publication date is Oct 27, but it is currently available for preorder. https://us.macmillan.com/books/9780374621797/sixmathessentials/

In a day or so, the mathematicians behind the #1stproof challenge at https://1stproof.org/ will reveal their solutions to the 10 challenge problems they posted recently. (I am not directly involved in this challenge, although I know most of the authors personally and approve of their experiment.) It seems likely that there will be many claims, both trustworthy and dubious, of proofs of these problems by various AI-generated means.

The Erdos problem web site, having dealt with this type of thing for several months now, has come up with several guidances on how to increase confidence in the correctness of an AI-generated proof: https://github.com/teorth/erdosproblems/wiki/I-think-I-managed-to-get-my-favorite-AI-tool-to-solve-an-open-Erd%C5%91s-problem!--What-do-I-do-next%3F The wording there is specific to Erdos problems, but much of the advice can be applied more broadly.

I would like to highlight in particular the additional correctness guarantees provided by formalizing the argument in Lean. When used correctly, a Lean formalization of a proof can provide extremely high confidence that a given proof correctly proves the desired claim. However, if the Lean proof is itself AI-generated without supervision from an expert in Lean, there are still ways in which a supposed "Lean certificate" of correctness is unsatisfactory or even worthless. These include:

1. A Lean proof that adds additional axioms in the proof beyond the standard three, or which relies on malicious metaprogramming.
2. Subtle errors in the formalization of the *statement* of the result to be proved, that allows the claim to be proven on a technicality. (This is a particular risk if this statement formalization is also AI-generated.)

See https://leanprover-community.github.io/did_you_prove_it.html and https://lean-lang.org/doc/reference/latest/ValidatingProofs/#validating-proofs for best practices on guarding against such issues.

Rado Kirov has been one of several people working through the exercises in my Lean formalization of my Analysis I textbook at https://github.com/teorth/analysis . For several months he proceeded by hand, teaching himself Lean; see https://rkirov.github.io/posts/lean3/ and https://rkirov.github.io/posts/lean4/ . But recently, he switched to using Claude Code, significantly accelerating the process, to the point where all the exercises in three section could be formalized in a weekend, with only a few hours of active intervention: https://rkirov.github.io/posts/lean5/ . This is already notable, but I found Rado's description of his precise workflow, and the carefully curated prompt at https://github.com/rkirov/analysis/blob/main/CLAUDE.md he used, to be particularly interesting, with an emphasis not on just solving the exercises, but aligning it to his desired writing style, and identifying "pitfalls" in the formalizing process (which were recorded separately at https://github.com/rkirov/analysis/blob/main/TACTICS.md ). These sorts of experiments suggest that using these automated tools to take over tedious tasks such as formalization may not necessarily reduce our own capability to achieve these tasks; with the proper workflows, they could actually enhance our understanding of the process.

A curious phenomenon over at the #Erdos problems web page and repository. We've had a hectic two months or so in which we received a flood of new solutions to these problems, coming from a mix of human efforts, purely AI-generated proofs, and hybrid approaches. Some of these turned out to be incorrect, and others ended up being similar to existing solutions, but nevertheless many checked out, leading to nearly 50 more problems being marked as solved on the site during this period.

But in the last week, submissions have dropped to nearly zero. It is not clear exactly what the reason is, but I can think of at least three explanations: (a) the burst of media attention around the Erdos problems has dissipated. (b) all the easy "low-hanging fruit" of obscure Erdos problems amenable to current AI tools have already been harvested. (c) The time-sensitive "First Proof" challenge that came out last week is now absorbing all the attention of AI-prover enthusiasts.

Perhaps it is a combination of all three factors.

A few days ago, I noted the revival of one archaic mathematical practice, namely that of encrypting one's proofs (or announcements). Today, as part of the ongoing Integrated Explicit Analytic Number Theory Network project https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/ , we found ourselves reviving another archaic piece of mathematical infrastructure: the logarithm table.

These tables, pioneered by Napier in the 17th century, were a mainstay of mathematical computation until eventually supplanted first by calculators and then by modern computers. But we are finding that verifying in Lean that, say, ln 2 is equal to 0.693147 to six decimal places is somewhat fiddly and computationally expensive to formally verify (one has to use a Taylor series with explicit remainder and figure out where to cut off the series).

Eventually we settled on what is basically the 17th century solution, modernized for the era of formal proof verification: the project now sports a file `LogTables.lean` which systematically gathers formally verified calculations of logarithms via a new interval arithmetic package. Similar to a precomputed log table, this file is intended to be typechecked once (as a laborious calculation), and then imported as needed by all other files.

It is a fascinating paradox that cutting edge technology can sometimes make obsolete practices relevant again, albeit with a modern spin. (Yet another example: the capability of current AI tools has revived the in-person class exam, which we had just started to move away from in the COVID era.)

This experiment (authored by several well-known mathematicians) revives an archaic practice (last seen in the era of Gauss) of posting encrypted proofs before revealing them: https://arxiv.org/abs/2602.05192 . Here, the challenge is to see whether 10 research-level problems (that arose in the course of the authors research) are amenable to modern AI tools within a fixed time period (until Feb 13).

The problems appear to be out of reach of current "one-shot" AI prompts, but were solved by human domain experts, and would presumably a fair fraction would also be solvable by other domain experts equipped with AI tools. They are technical enough that a non-domain-expert would struggle to verify any AI-generated output on these problems, so it seems quite challenging to me to have such a non-expert solve any of these problems, but one could always be surprised. It will be interesting to see if there were any notable outcomes to this experiment by the expiration of the time linit.

It will still be a few months before AlphaEvolve is fully released to the public, but we at least now have a small gallery of AlphaEvolve experiments one can showcase, including some of my own: https://alphaevolve-examples.web.app/ae/gallery

I doubt that anything resembling genuine "artificial general intelligence" is within reach of current #AI tools. However, I think a weaker, but still quite valuable, type of "artificial general cleverness" is becoming a reality in various ways.

By "general cleverness", I mean the ability to solve broad classes of complex problems via somewhat ad hoc means. These means may be stochastic or the result of brute force computation; they may be ungrounded or fallible; and they may be either uninterpretable, or traceable back to similar tricks found in an AI's training data. So they would not qualify as the result of any true "intelligence". And yet, they can have a non-trivial success rate at achieving an increasingly wide spectrum of tasks, particularly when coupled with stringent verification procedures to filter out incorrect or unpromising approaches, at scales beyond what individual humans could achieve.

This results in the somewhat unintuitive combination of a technology that can be very useful and impressive, while simultaneously being fundamentally unsatisfying and disappointing - somewhat akin to how one's awe at an amazingly clever magic trick can dissipate (or transform to technical respect) once one learns how the trick was performed.

But perhaps this can be resolved by the realization that while cleverness and intelligence are somewhat correlated traits for humans, they are much more decoupled for AI tools (which are often optimized for cleverness), and viewing the current generation of such tools primarily as a stochastic generator of sometimes clever - and often useful - thoughts and outputs may be a more productive perspective when trying to use them to solve difficult problems.

The current administration in the US has, through various funding agencies such as the NSF and NIH, has recently suspended virtually all federal grants to my home university, UCLA (including my own personal grant, although that is far from the most serious impact of this decision), on the grounds that UCLA was “failing to promote a research environment free of antisemitism and bias”. One can certainly debate whether these grounds were justified, or whether they merit the extremely draconian damage to the very research environment that this decision is claiming to protect, but if nothing else this unprecedented decision does not appear to have followed the usual standards of due process for actions of this nature; for instance, there appears to have been no good faith effort by the administration to receive a response from UCLA to its allegations before implementing its decision.

The suspension of my personal grant has a non-trivial impact on myself (in particular, my summer salary, which I had already deferred in order to allow the previously released NSF funds to support several of my graduate students over this period, is now in limbo), and now gives me almost no resources to support my graduate students going forward; but this is only a fraction of a percent of the entire amount being suspended. A far greater concern is the impact on the Institute for Pure and Applied Mathematics (IPAM) https://www.ipam.ucla.edu/, which despite receiving preliminary approval earlier this year for a new five-year round of funding (albeit at significantly reduced levels) from the NSF, now only has enough emergency funding for a few months of further operation at best if the suspension is not lifted. (1/4)

"In the end, the Party would announce that two and two made five, and you would have to believe it. It was inevitable that they should make that claim sooner or later: the logic of their position demanded it. Not merely the validity of experience, but the very existence of external reality, was tacitly denied by their philosophy. The heresy of heresies was common sense. And what was terrifying was not that they would kill you for thinking otherwise, but that they might be right. For, after all, how do we know that two and two make four? Or that the force of gravity works? Or that the past is unchangeable? If both the past and the external world exist only in the mind, and if the mind itself is controllable—what then?" - George Orwell, "Nineteen Eighty-Four". (1/6)

One of my papers got declined today by the journal I submitted it to, with a polite letter saying that while they found the paper interesting, it was not a good fit for the journal. In truth, I largely agreed with their conclusions, and the paper is now submitted to a different (and hopefully more appropriate) journal.

Rejection is actually a relatively common occurrence for me, happening once or twice a year on average. I occasionally mention this fact to my students and colleagues, who are sometimes surprised that my rejection rate is far from zero. I have belatedly realized our profession is far more willing to announce successful accomplishments (such as having a paper accepted, or a result proved) than unsuccessful ones (such as a paper rejected, or a proof attempt not working), except when the failures are somehow controversial. Because of this, a perception can be created that all of one's peers are achieving either success or controversy, with one's own personal career ending up becoming the only known source of examples of "mundane" failure. I speculate that this may be a contributor to the "impostor syndrome" that is prevalent in this field (though, again, not widely disseminated, due to the aforementioned reporting bias, and perhaps also due to some stigma regarding the topic). So I decided to report this (rather routine) rejection as a token gesture towards more accurate disclosure. (1/2)