Terence Tao

Professor of #Mathematics at the University of California, Los Angeles #UCLA (he/him).

Public Key

npub1hsf727dlfy55vvm5wuqwyh457uwsc24pxn5f7vxnd4lpvv8phw3sjm7r3k

NIP-05 Address

tao@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqstcyl90xl5j22xxd68wq8zt660w8gv92snf6ylxrfk6lskxrsmhgcpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsvjaa89

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1hsf727dlfy55vvm5wuqwyh457uwsc24pxn5f7vxnd4lpvv8phw3sjm7r3k

Show more details

Last Notes

2026-02-25 01:57:54 UTC

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

2026-02-12 18:35:36 UTC

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 suspicious, 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.

2026-02-08 23:21:06 UTC

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. (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.)

2026-02-06 06:14:11 UTC

An interesting experiment that revives an archaic practice (from 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 faor 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 interesting outcomes to this experiment by the expiration of the time linit.

2026-02-04 19:19:50 UTC

- reply

@nprofile…sz8l No, although they supply the compute resources for the AlphaEvolve experiments I have run.

2026-02-03 18:50:51 UTC

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

2026-01-11 19:07:35 UTC

- reply

@nprofile…mf6h We have some statistics and graphs for the Erdos problem database as a whole; see https://github.com/teorth/erdosproblems . But for now, it seems the most productive setup is to have individual web pages and discussion forums for each problem, see https://www.erdosproblems.com/forum/

2026-01-11 19:04:37 UTC

- reply

@nprofile…zhv7 An update: as it turns out, the AI-generated solution to https://www.erdosproblems.com/728 can be modified to also answer the closely related problem https://www.erdosproblems.com/729; and as part of the community discussion of these results, a previously unreported link to another similar problem https://www.erdosproblems.com/401 was unearthed, which seems likely to be solved by these AI tools soon as well. A more challenging variant problem https://www.erdosproblems.com/400 is now being looked at, which would likely require more sophisticated arguments. With these developments, I would revise my previous assessment; while the solution of just 728 would not be sufficient for a research-level paper, a broader paper developing some general results that can handle all of these problems (and perhaps some other questions not posed by Erdos) in a unified fashion would be a reasonable candidate for a paper publishable in a reputable journal.

2026-01-10 16:04:16 UTC

- reply

Addendum: as portions of my text above have been quoted out of context, I would like to also draw attention to the various caveats listed at https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems regarding the extent to which one can draw broader conclusions about AI mathematics capabilities from the progress in solving Erdos problems.

2026-01-10 06:52:18 UTC

- reply

@nprofile…zhv7 By itself, I would not rate this as a publishable result, but it could become part of a more substantial paper surveying the state of various related problems involving these sorts of binomial coefficient divisibility problems, describing what the standard methods can accomplish (including the solution to this problem as an example), and discussing the remaining open problems in the field (https://www.erdosproblems.com/376 is a fairly well known one for instance). I could see AI tools playing a role in systematically exploring the application of such well understood methods reasonably large classes of problems like at a scale which would either be impracticable or inefficient to have human mathematicians work out by traditional means.

2026-01-07 21:03:47 UTC

Recently, the application of AI tools to Erdos problems passed a milestone: an Erdos problem (#728) was solved more or less autonomously by AI (after some feedback from an initial attempt), in the spirit of the problem (as reconstructed by the Erdos problem website community), with the result (to the best of our knowledge) not replicated in existing literature (although similar results proven by similar methods were located).
This is a demonstration of the genuine increase in capability of these tools in recent months, and is largely consistent with other recent demonstrations of AI using existing methods to resolve Erdos problems, although in most previous cases a solution to these problems was later located in the literature, as discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 . This particular case was unusual in that the problem as stated by Erdos was misformulated, with a reconstruction of the problem in the intended spirit only obtained in the last few months, which helps explain the lack of prior literature on the problem. However, I would like to talk here about another aspect of the story which I find more interesting than the solution itself, which is the emerging AI-powered capability to rapidly write and rewrite expositions of the solution. (1/5)

2025-12-15 07:18:01 UTC

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 amazing magic trick can dissipate 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 do not seem to be correlated nearly as much for AI tools, 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.

2025-12-05 16:23:32 UTC

Over on Kevin Buzzard's blog, Boris Alexeev has written a guest post on the state of the art on autoformalization in practice, focusing in particular on the improved speed and efficiency of formalization when applied to the problems in the Erdos Problems database, and how these efforts have begun to resolve some of the lower hanging fruit in that database. https://xenaproject.wordpress.com/2025/12/05/formalization-of-erdos-problems/

2025-12-05 05:06:27 UTC

The Communications of the Association for Computing Machinery (ACM) has compiled a list of articles from leaders in the profession on the importance of federal investment in basic research in the technology sector. https://www.acm.org/media-center/2025/december/cacm-federal-funding

2025-11-27 06:33:08 UTC

This two-dimensional image has been circulating recently as an metaphor for the current state of AI technology. It is admittedly an improvement over one-dimensional narratives in which AI development is presented as a linear progression from sub-human intelligence to super-human intelligence. However, it is still a significant oversimplification. The space of cognitive tasks is not well modeled by either one-dimensional or two-dimensional spaces, but is instead extremely high-dimensional. There are now indeed many directions in this high-dimensional space in which AI tools can, with minimal supervision, achieve better performance than human experts. But, as per the "curse of dimensionality", such directions still remain very sparse. Also, human performance is also very spiky and diverse; representing this by a single round disk or ball is also somewhat misleading.
In high dimensions, the greatest increase in volume often comes from taking combinations of smaller, spikier sets. A team of humans working together, or humans complemented by a variety of AI tools, can achieve a significantly greater performance on many tasks than any single human or AI tool could achieve individually, particularly if they are strong in "orthogonal" directions. On the other hand, the choice of combination matters: the wrong combination could lead to a misalignment between the objective and the actual outcome, in which the stated goal may be nominally achieved, but at the cost of several unwanted secondary effects as well.
TLDR: the topic of intelligence is high-dimensional for any low-dimensional narrative to be perfectly accurate, and one should take any such narratives with a grain of salt.
https://media.mathstodon.xyz/media_attachments/files/115/620/202/193/141/274/original/cb4966685b1ef97a.png

2025-11-25 02:48:31 UTC

#IPAM (The Institute for Pure and Applied Mathematics) is soliciting applications from industry to sponsor projects in its Research in Industrial Projects for Students (RIPS) program, in which talented undergraduate students, with a postgraduate mentor, work on industry-sponsored projects over a 9-week program while at residence at IPAM. Details about the program can be found at https://www.ipam.ucla.edu/all-upcoming-programs/rips-sponsor-information/

2025-11-07 17:06:28 UTC

- reply

@nprofile…z3hk In our experiments we have been incentivizing AlphaEvolve to come up with solutions that are as interpretable as possible, and have as clear a dependency on the parameter n as possible, so the general solutions that have been found are ones which a human could generalize from seeing the code to generate them for small n (although in the finite field Kakeya and Nikodym examples, if a human was just given the raw set of points rather than the code used to procedurally generate them, it would be significantly harder to discern the pattern).

2025-11-06 21:31:00 UTC

#IPAM is running an Industrial Short Course on Generative AI Algorithms for Mar 5-6, 2026. Registration is now open: https://www.ipam.ucla.edu/programs/special-events-and-conferences/industrial-short-course-generative-ai-algorithms/

2025-11-06 16:06:25 UTC

- reply

@nprofile…z3hk IMO 2025 problem 6 https://google-deepmind.github.io/alphaevolve_repository_of_problems/problems/65.html was an interesting case of this: see the discussion in section 43 where AlphaEvolve discovered the construction in Figure 34. The majority of human participants at the 2025 IMO, and none of the AI tools applied to the problem, were able to obtain such a construction. (But one should make the caveat that locating the optimal construction is only one half of this problem; the other half is to prove that the construction is optimal, and AlphaEvolve had no capability on its own to accomplish this. On the other hand, one could imagine that a human attacking this problem who was given this example by AlphaEvolve could use it as inspiration to try to establish a rigorous proof of optimality.)

2025-11-06 03:42:20 UTC

A new paper with Bogdan Georgiev, Javier Gomez-Serrano, and Adam Zsolt Wagner: "Mathematical exploration and discovery at scale" https://arxiv.org/abs/2511.02864 , in which we record our experiments using the LLM-powered optimization tool #AlphaEvolve to attack 67 different math problems (both solved and unsolved), improving upon the state of the art in some cases and matching preivous literature in others. The data for these experiments can be found at https://github.com/google-deepmind/alphaevolve_repository_of_problems and further discussion is at https://terrytao.wordpress.com/2025/11/05/mathematical-exploration-and-discovery-at-scale/

2025-11-04 21:58:57 UTC

- reply

There was one major exception, which was the step where one had to verify that the graph indeed had 44 edges. The graph was the union of five disjoint subgraphs, each of which GPT was able to count more or less correctly (modulo minor technical fixes), but did not supply any valid reason why the number of edges in the union was the sum of the number of edges in each component subgraph. I ended up spending about an hour looking up the Mathlib tools on sum types and Finset cardinality before making this part of the argument work (using a different approach than the one GPT suggested). But with this and the other more minor changes, I ended up with a typechecking proof at https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_613.lean (3/4)

2025-11-04 21:58:42 UTC

- reply

The initial steps went quite well: ChatGPT correctly specialized Pikhurko's construction to the degree 5 case and gave a very readable explanation as what the construction was and why it worked. (With this version of GPT, every query took ten to twenty minutes to answer, so I did this asynchronously, attending to other matters while checking back on GPT every so often.) It also formalized an essentially correct definition of the graph and of the problem statement, and supplied mostly working Lean code for each requested step. It was somewhat hindered by not having direct access to my own Lean repository, and appeared to be trained on older versions of Mathlib with slightly different syntax, so a certain amount of cleanup was required to make everything typecheck, but I had enough expertise in Lean to fix these issues. Some lines did not compile at all, but in most cases the statement to prove was obvious enough that I could supply a different proof by hand (in many cases, powerful reasoning tactics such as `aesop` or `grind` - neither of which GPT used for some reason - finished off those statements immediately). (2/4)

2025-11-04 21:58:32 UTC

Inspired by the recent successful "vibe coding" in Lean of a solution to an Erdos problem at https://arxiv.org/abs/2510.19804 , I tried my hand at formalizing the disproof (by Pikhurko in 2001) that had recently been unearthed by Quanyu Tang of another Erdos problem https://www.erdosproblems.com/613. This was a simple finite counterexample: a graph of 44 edges on 15 vertices that could not be split into a bipartite graph and a graph with max degree 5. The paper of Pikhurko is just 9 pages (and also constructs more general counterexamples with larger choices of parameters, as well as some reasonably matching lower bounds), so this looked like within reach of modern AI tools. I therefore uploaded the paper to ChatGPT Pro and asked it first to summarize the construction in informal language, and then formalize step by step. (1/4)

2025-10-28 21:35:35 UTC

- reply

Update: the discussion has been moved to a web-public forum: https://ai-math.zulipchat.com/#narrow/channel/539992-Web-public-channel---AI-Math/topic/Best.20practices.20for.20incorporating.20AI.20etc.2E.20in.20papers/near/546518354

2025-10-27 22:03:44 UTC

- reply

@nprofile…nxdw Hmm, that appears to be a typo, I will contact IAS to get that fixed.

2025-10-27 19:34:45 UTC

The Salem prize for 2025 is awarded to Hong Wang and Vesselin Dimitrov https://www.ias.edu/math/2025-salem-prize-winners . (I chair the scientific committee for this prize.) Congratulations to both winners!

2025-10-22 22:43:59 UTC

Yet another recent example of AI assistance in mathematics: my colleague Ernest Ryu here at UCLA was able to solve an open problem in optimization theory (roughly speaking, an asymptotic convergence result for a certain class of ODEs) in large part through an extended conversation with a large language model, serving both as a "rubber duck" and a stochastic generator of proof ideas. https://x.com/ErnestRyu/status/1980759528984686715 Many of the ideas generated were not usable, but a non-trivial fraction of them did contain some viable strategies that had not been immediately evident to Ernest. There was a significant pruning process to isolate the small number of useful ideas and discard the larger set of non-useful ones, but even so, the tool provided a net time saving in reaching a working argument, which Ernest then polished by hand into a two-page proof. (1/2)

2025-10-22 18:11:54 UTC

Now that we are beginning to see some isolated examples of serious, responsible AI assistance in mathematical research papers, it seems an opportune time to start a discussion about what the best practices for incorporating, disclosing, and mitigating risks of such use should be. I started such a discussion at https://ai-math.zulipchat.com/#narrow/channel/514953-general/topic/Best.20practices.20for.20incorporating.20AI.20etc.2E.20in.20papers

2025-10-15 16:40:56 UTC

In https://mathoverflow.net/questions/463937/what-mathematical-problems-can-be-attacked-using-deepminds-recent-mathematical/463940#463940 I asked whether current AI technology could provide a usable tool to test whether various inequaliies involving infinite series of non-negative quantities could be determined to be true or not, with some certificate of proof provided in the former case. An experimental tool of this type has just been launched by Ayush Khaitan at https://o-forge.com/ , which could be a useful tool for analysts needing quick confirmation of such inequalities without having to do any sophisticated programming (or prompt engineering). The user interface is still very much in development; feedback can be given for instance as responses to this blog comment https://terrytao.wordpress.com/2025/05/09/a-tool-to-verify-estimates-ii-a-flexible-proof-assistant/comment-page-1/#comment-688872

2025-10-10 19:00:14 UTC

- reply

So the problem looks out of reach of my box of tools, and remains open; but for the "large scale" metric of gaining understanding of the problem, the AI use did help, though mostly in an indirect sense of allowing me to more quickly work through, and then discard, an approach which I now believe to be unsuitable for the problem; I also now know a few more differential geometry facts that I was not aware of.
It is interesting to compare with my previous experiment https://mathstodon.xyz/@tao/115306424727150237 where I gave the AI a task in which I had quite a good intuition on the outcome. Here, the AI was more creative and supplied inputs that I did not know; but it was also significantly harder to trust and guide the AI in productive directions. There does seem to be some value in interacting with AI on problems slightly outside of one's area of expertise, but one certainly has to proceed with caution and situational awareness. (8/8)

2025-10-10 19:00:01 UTC

- reply

On the other hand, because of this retrospection, I now have a much clearer idea of what the "enemy" in the problem is that one has to deal with - spheres that are very far from round, and which would contain extremely long cylinders, sheets, or other "thin" objects that do not contribute much volume but will stretch out the geometry considerably. As such, most of the techniques I had in mind, which were optimized towards "roundish" objects, were inappropriate for this task. The one tool I am familiar with that might still be useful is a flow approach (based on something like mean curvature flow), and this in fact works in the two-dimensional case due to the nice properties of curve shortening flow in that setting, but it seems difficult to get enough control on these flows (particularly when singularities form) to make such an approach work.
The star-shaped case ended up being actually one of the easiest cases of the problem; I have since learned that a two-dimensional version of the argument appears in a paper of Pankrashkin https://doi.org/10.1007/s00013-015-0804-z , and an alternate treatment in three dimensions appears in this recent paper of Qiu https://arxiv.org/abs/2507.06245. (7/8)

2025-10-10 18:59:50 UTC

- reply

On comparing this new intuition with the strategy I had pursued, I found that I made a mistake in assuming that the (intrinsic) diameter of the immersed sphere was bounded (which was implicitly used in the coercivity analysis). The numerical approach I had in mind might conceivably resolve the problem in finite time for all immersed spheres of a given diameter, but would not handle the general case.
The AI had not flagged this issue, instead exhibiting the usual AI behavior of largely agreeing with everything I had said. So, at the "medium scale" of directing strategy, the AI was mildly unhelpful, in that it reinforced the bad intuition that I had on the problem instead of pushing back on it. (6/8)

2025-10-10 18:59:39 UTC

- reply

So, at the "small scale" of fulfilling the requests asked of it, the AI performed very well, with only minor mistakes, and contributing several useful ideas that were in the literature, but which I was not aware of. At this point I felt though that further progress required input from actual differential geometry experts to avoid a very tedious brute force check, decided to write up the key results (in my own words, and checking step by step) and post them to the site.
After doing so, I noticed in commentary for the original problem that the two-dimensional version of this problem was a classical result of Pestov and Ionin, which is famous enough to get its own Wikipedia page: https://en.wikipedia.org/wiki/Pestov%E2%80%93Ionin_theorem . But a glance at the picture on that page showed me that my intuition was quite wrong: in addition to "nearly round" sets, there were important cases where the set was very far from round, but instead resembled some roundish objects joined together by very long thin tubes. (5/8)

2025-10-10 18:59:28 UTC

- reply

The AI performed well here too, basically working out that an elliptic coercivity estimate would indeed imply that the theorem was true if the curvatures were sufficiently close to 1 on average. Though it did point out unprompted that this was not actually a new result, because the hypothesis of curvatures being close to 1 actually implied star-shapedness! (It did slightly mishandle the estimation of a perturbative nonlinear term, but not in an unfixable fashion; it was comparable to a mistake that a human expert in nonlinear PDE might initially make.)
To me, this resembled a "small data" result in PDE, leaving only the "large data" case remaining. The elliptic nature of the problem, combined with the bounded curvature, suggested to me that there was enough compactness to the problem that the problem could be reduced to a large finite computation using numerical PDEs. I suggested this approach to the AI, who agreed and gave an outline of how such a program might proceed. However, the approach would be extremely messy and unenlightnening, essentially a brute force enumeration of all possible shapes. (4/8)

2025-10-10 18:59:15 UTC

- reply

This impressed me, but I of course needed to verify the various steps of the proof. I found some online resources that restated Minkowski's formula, but did not easily locate a proof; but upon asking the AI, two satisfactory proofs were provided (one along the lines I suggested to it using the divergence theorem, and one based on a flow method that I had not thought of).
So far, so good. The argument also suggested that the round sphere was the only minimizer, with the volume getting larger as one moved away from the round case. This was quite encouraging, so I then asked the AI to analyze the perturbative "almost round" situation in which the curvatures were close to 1 on average. I had in mind to treat this as a perturbative elliptic PDE problem, and in particular use some elliptic regularity or coercivity estimates to finish off this case. (3/8)

2025-10-10 18:58:54 UTC

- reply

Previous comments on the problem had indicated that the convex case was too easy to be interesting, so I decided to look at the slightly larger class of star-shaped objects. Here I suspected that one could express the hypothesis and conclusion of the problem in terms of various integrals on the surface, and I was hoping to use some integral inequalities (e.g., Sobolev embedding) to then proceed. However, my differential geometry was rather rusty, so I asked the AI to perform these calculations for me.
Somewhat to my surprise, the AI not only computed all the quantities I requested, but actually gave a complete proof of the problem in the star-shaped case. The proof manipulated the various integrals that arose using various inequalities and identities, some of which I recognized (Stokes' theorem and the Willmore inequality / Gauss-Bonnett), but there was one which was new to me (Minkowski's first integral formula). With all of these inequalities (and also the arithmetic mean-geometric mean inequality relating mean curvature to Gauss curvature), the proof of the star-shaped case was in fact a one-line argument. (2/8)

2025-10-10 18:58:10 UTC

I experimented with using a more powerful AI (ChatGPT5 Pro) to attempt an open problem https://mathoverflow.net/questions/425509/sphere-with-bounded-curvature which is not quite in my area of expertise (specifically, differential geometry): https://chatgpt.com/share/68e85cba-7228-800e-8804-a0f41aa64e14 . The outcome was surprisingly nuanced, and illustrates a point I made in an earlier post https://mathstodon.xyz/deck/@tao/114501120421010793 that one has to measure the usefulness of a tool at multiple scales. In summary: AI assistance was very useful at small scales, somewhat unhelpful at medium scales, but somewhat helpful again at large scales; the problem remains unsolved, but I understand it much better now.
The problem asks, if a smooth immersed sphere in R^3 has both principal curvatures bounded in magnitude by 1, must it enclose at least a large a volume as the round unit sphere? This looked to me like a variational problem in which the round sphere would be the minimizer, so the problem naturally splits into a "perturbative" regime in which the immersed sphere is close to round, and the "non-perturbative" regime in which the immersed sphere is far from round. Lacking much geometric intuition on this problem, and knowing that most of my analysis-based toolkit was geared towards pertburative cases, I guessed that the perturbative regime would be the more important case, and chose to focus efforts there. (1/8)

2025-10-06 04:03:14 UTC

- reply

Barring some new development, I think the project will wind down soon, with the complete set of examples submitted to the OEIS, and some data sets (and perhaps Lean code) verifying the arguments placed in some repository. Overall it was quite an enjoyable experience - and, playing out in a matter of days, far faster than a traditional research project; while the specific problem here was not of particular significance, it is perhaps a harbinger of the type of collaborative mathematical projects fully utilizing modern tools that we will see more of in the near future. (3/3)

2025-10-06 04:02:28 UTC

- reply

At this point, AI assistance has definitely taken a back seat; progress is proceeding largely by manually written code (though perhaps some participants are taking advantage of AI-powered autocomplete features, or a chatbot to generate some quick back-of-the-envelope calculations), and some new theoretical arguments. One participant did experiment with giving the problem to the highest reasoning mode of ChatGPT, and letting it run autonomously, it was able to correctly locate a counterexample at n=97, but also incorrectly claimed that this was the minimal such example (when instead n=71 is the minimizer). This seems broadly consistent with my own experience with frontier models when not supervised tightly in a step-by-step fashion by a domain expert. On the other hand, while we did not have to contend with AI hallucinations, we did experience some setbacks due to good old-fashioned human errors in calculation, though the large number of participants did help in identifying these "bugs". (Perhaps in the future when Lean formalization can actually be performed in real time, rather than near-real-time, even these errors will become a thing of the past.) (2/3)

2025-10-06 04:02:11 UTC

A second update on my previous posts https://mathstodon.xyz/@tao/115306424727150237 https://mathstodon.xyz/@tao/115316787727719049 on the #MathOverflow problem https://mathoverflow.net/questions/501066/is-the-least-common-multiple-sequence-textlcm1-2-dots-n-a-subset-of-t that had a first initial counterexample located with #AI assistance, and then the minimal counterexample obtained through a crowdsourced effort. As has happened with several previous projects, the crowdsourced effort has acquired a life of its own. In particular, the task of classifying *all* the counterexamples - which I had previously dismissed in my previous post as "somewhat tedious to perform", has in fact been completed (with the problem alternating between true and false for n between the first counterexample 71 and the last example 172, before settling down to a unending string of counterexamples. We now have some very efficient ways to either prove or disprove that a given number is highly abundant; some of the asymptotic analysis initially required some high powered number theory hypotheses such as the generalized Riemann hypothesis (GRH), but as our arguments became more efficient, this became unnecessary. We even have some recent contributions from the Lean community, formalizing some of the counterexamples in Lean, almost in real-time! (1/3)

2025-10-04 16:17:40 UTC

- reply

So, was AI-assistance "better" than crowdsourcing the problem, or working on the problem alone? It seems the answer is highly situational. For this particular problem, there was a key juncture where there was a significant "activation energy" required to make further progress, in which both individual or crowdsourced human attention was not sufficient to overcome; but this obstacle had favorable conditions for AI use, namely a well-understood task, decomposable into simpler steps, that could be verified externally. But through the "beat the AI" challenge, this AI use also made the crowdsourcing option available, leading to more creative (and more socially enjoyable) solutions that no longer required any AI assistance. It is conceivable that increased AI usage at this stage could have accelerated the final solution further by a few hours, but this was not a time-sensitive project, and I think it was a better outcome for the rest of the project to develop organically now that it had become unblocked. (5/5)

2025-10-04 16:17:28 UTC

- reply

I played with this final problem, again using AI assistance https://chatgpt.com/share/68e1444f-902c-800e-ab87-35a6d7a6e203, though most of my exploration was conducted outside of this chat by experimenting with the Python code that the AI tool had initially provided. This led me to suggest introducing a certain "score function" that could filter the number of cases to check down to a somewhat feasible number (I estimated around 2^30 cases or so). However, actually coding (and debugging) this search manually would have been time-consuming with my level of coding proficiency, and I did not trust my ability to verify AI-generated code here (in contrast to the problem of *disproving* the highly abundant property, where verification was simple). I therefore posted my score function suggestion to the MathOverflow discussion and called it a night. This morning, I checked the site to find that Matthew Bolan had completed the case check (presumably via manual coding) to confirm that 𝑛=67 was not a counterexample, thus definitively establishing that the first counterexample occurred at 𝑛=71. So now the problem can be considered definitively solved (technically, one might still want to verify that every 𝑛 > 71 is also a counterexample, but this looks overwhelmingly likely from our calculations, and somewhat tedious to perform). (4/5)

2025-10-04 16:16:49 UTC

- reply

Within a few hours, several responses were received, using more traditional computer code to locate counterexamples first at 𝑛=13757, then at 𝑛=4483, then 𝑛=3499. These approaches used the same method I had gotten the AI to perform to avoid several hours of work; but now that some feasible parameter choices were already known, the task of modifying these parameters was significantly faster, and I suspect the other contributors were also more adept at manual coding tasks than I was.
A breakthrough then came from another participant (Max Alekseyev), who introduced a new idea (utilizing small primes) to obtain a counterexample at 𝑛=113. This was swiftly optimized by Gergely Harcos to 𝑛=71. The only remaining candidate for a minimal counterexample then turned out to be 𝑛=67. After some near-misses provided by yet further participants, it became plausible that in this case the quantity of interest was in fact highly abundant. But this quantity was quite large (specifically, it was 79211881234889091923261227200), and beyond the range of brute force verification. (3/5)

2025-10-04 16:16:15 UTC

- reply

At this point, I performed a pen-and-paper (heuristic) asymptotic analysis that suggested that the conjecture was in fact false for sufficiently large 𝑛. However, this analysis did not supply me with specific numerical parameters to yield a concrete counterexample, and there seemed to be little interest from the rest of the MathOverflow community in pursuing this direction, so in the absence of AI assistance, I would have had to spend several hours either making the heuristic analysis rigorous, or coding (and debugging, and performing trial-and-error parameter selection on) a Python program to search for an explicit counterexample. It is then that I used AI to perform the latter step, as discussed in the previous post. As previously noted, the risks of hallucination and other nonsense was minimal, due to the ability to easily verify the output by a separate program, and because the overall task was well understood and could be broken down into several smaller steps.
The outcome of this AI use was that, after an hour, I had produced a counterexample for 𝑛=200000. However, the heuristic steps leading up to that counterexample suggested that there was significant room to lower n much further. I considered continuing the AI conversation to try to optimize parameters, but having already spent an hour on this problem, I was ready to move on, and proposed instead a "beat the AI" challenge to the rest of the MathOverflow community to see how a crowdsourced approach would compare against an AI-assisted approach to the problem. (2/5)

2025-10-04 16:15:39 UTC

An update on my previous post https://mathstodon.xyz/@tao/115306424727150237 regarding how I was able to use modern AI to help solve a MathOverflow problem. Superficially, this story favors the "you should use AI whenever possible" narrative over the "you should avoid AI whenever possible"; but, as I hope the discussion below will show, the more accurate narrative lies in between these two extremes. The story is told more or less completely at the MathOverflow page https://mathoverflow.net/questions/501066/is-the-least-common-multiple-sequence-textlcm1-2-dots-n-a-subset-of-t , but the responses are not arranged in chronological order, and so the history may be a little hard to follow from that page.
The original MathOverflow problem, posed on October 1, asked if a certain statement was true for all natural numbers 𝑛. The precise statement here is not important for this story, except that it involved verifying that a certain quantity 𝑙𝑐𝑚(1,...,𝑛) depending on 𝑛 was "highly abundant", which was a property that was difficult to verify for large numbers (requiring a large csae check), but relatively easy to disprove (requiring only a single counterexample to a certain inequality). Initial responses to this problem noted that OEIS data confirmed the conjecture for 𝑛 up to 66, and noted the difficulty of verifying the highly abundant property, thus suggesting that the conjecture was true, but likely very difficult to prove. (1/5)

2025-09-06 02:17:16 UTC

Earlier this year, the second #AIMO (artificial intelligence mathematical olympiad) concluded, with the winning team solving 37/50 in the final set of math problems (that had been selected to be harder for AI than the first AIMO).
The competition was restricted to open source models and run with a limited amoutn of compute. The AIMO has now conducted a retest of these problems both for the top two teams from that competition (NemoSkills and imagination research), as well as OpenAI's o3 model, both with comparable levels of compute resources, and with high resources. Unsurprisingly, the high resource models did better, with the high resource o3 model scoring as high as 47/50, or even 50/50 if given two tries at each question. On the other hand, the gap between the open source models and the commercial models for a fixed amount of compute was relatively slight.
More details of this experiment are available at https://aimoprize.com/updates/2025-09-05-the-gap-is-shrinking

2025-08-25 01:30:30 UTC

- reply

While `grind` does have some additional tuneable parameters and options that I could try to tweak to try to coax it to work, I am finding that the optimal way for me to use this tool is not to try to explore too much the "intermediate modes" in which I try to repeatedly reconfigure the tool: if I cannot use `grind` to close the goal after one or two such attempts, I simply move on. I still find the tool to be a non-trivial time-saver in many contexts, but in some circumstances the way it saves time is by promptly signaling that it is not the appropriate tool for the task at hand.
Are there any prominent examples of chatbots that are tuned to report failure modes instead of intermediate modes when the confidence level of their answer is low? I hypothesize that these may actually be a more useful and less frustrating assistant to incorporate into complex workflows, despite being seemingly less "powerful". (3/3)

2025-08-25 01:30:14 UTC

- reply

In contrast, AI chatbots are usually tuned to avoid a "failure mode" as much as possible, at the expense of increasing the occurrence of "intermediate modes" where the chatbot response looks potentially useful, and invites further interaction from the user, but is not exactly providing what the user wants, and could contain hallucinations or some fundamental misunderstanding of the task that would take significant effort to uncover. Paradoxically, such tools may become significantly more useful if they simply reported that they were unable to provide a high quality answer to a query in such cases.
A comparison may be drawn with the increasingly advanced, but stringently verified, "tactics" used in a modern proof assistant such as Lean. I have been experimenting recently with the new tactic `grind` in Lean, which is a powerful tool (inspired more by "good old-fashioned AI" such as satisfiability modulo theories (SMT) solvers, than modern data-driven AI) to try to close complex proof goals if all the tools needed to do so are already provided in the proof environment; roughly speaking, this corresponds to proofs that can be obtained by "expanding everything out and trying all obvious combinations of the hypotheses". When I apply `grind` to a given subgoal, it can report a success within seconds, closing that subgoal in a Lean-verified fashion and allowing me to move on to the next subgoal. But, importantly, when this does not work; I quickly get a "`grind` failed" message, in which case I simply delete `grind` from the code and proceed by a more pedestrian sequence of lower level tactics. (2/3)

2025-08-25 01:30:01 UTC

Developers of AI tools often focus on trying to create a useful "success mode" for their tool, where the tool accomplishes the task that the user requested. But having a clearly identified "failure mode" is equally important, and does not always receive a corresponding amount of attention.
To give an analogy: if one is looking for some piece of information (e.g., obscure quote from a film that one has forgotten the name of), one can type some half-remembered version of the quote into a search engine and see what happens. If one is lucky, one activates the "success mode" where a useful hit is returned. Or, one can have a clear "failure mode" in which some message along the lines of "no relevant matches found" is shown, and one can either switch to a different way of searching for the information, or abandon the search entirely. However, there are also more ambiguous "intermediate modes" in which the search engine returned some hits that partially matched one's query, but do not seem to be exactly what one wants. This can lead to a somewhat frustrating and time-wasting exercise of investigating false leads and continuing fruitless queries (which could happen for instance if one had misremembered a key detail of the information one is trying to search for, and misconfiguring the search queries accordingly). This is often a significantly worse user experience than if the search engine had simply displayed a "failure mode" immediately. (1/3)

2025-08-18 15:45:37 UTC

I wrote an op-ed on the world-class STEM research ecosystem in the United States, and how this ecosystem is now under attack on multiple fronts by the current administration: https://newsletter.ofthebrave.org/p/im-an-award-winning-mathematician

2025-08-14 02:19:12 UTC

In response to a recent court ruling, the NSF has unsuspended its various grants to UCLA, including the one to IPAM (and my own personal grant). There is however the possibility of an appeal; and the (somewhat larger) funding from tne NIH to UCLA remains suspended at this time.
Over the last week or so I have been involved in emergency fundraising (mostly on behalf of IPAM), and am heartened by the broad and significant support we have received, both for immediate funding needs, as well as offers to sponsor some future events at the institute. It is a small silver lining to know that there was a reservoir of goodwill and private resources that one could tap into in times of crisis, although the time and energy required to perform this fundraising was significant.
In any event, this is no way to govern a country with a world-class research ecosystem, with quite unnecessary injections of uncertainty and chaos into what had been a predictable funding enviroment conducive to long-term planning.

2025-08-04 00:50:08 UTC

- reply

Addendum: the situation with compressed sensing can be compared with the current situation with modern large language models and related AI tools. Here, the field is almost entirely dominated by empirical research, often from industry rather than from academics. As such, there is a lot less clarity on what the key ingredients are to make a given AI technology suitable for a given use case; there are spectacular successes that cannot be replicated, next to seemingly promising uses that hit an unexpected wall (or, conversely, unlikely applications for which AI tools are far more effective than anticipated). With the notable exception of the mathematics of optimization and numerical linear algebra which are both somewhat mature, most of the theoretical mathematical framework needed to explain the strengths and weaknesses of AI is still in its infancy. (Though I would say here that the main bottleneck is not exactly lack of funding in basic research in the foundations of AI, but more that the mathematics itself is not understood to anywhere near the level we would like.)

2025-08-04 00:26:10 UTC

- reply

Another key input that the mathematical analysis added to the subject was that of abstraction. Already by the 1970s, the seismologist Jon Claerbout, working with the Stanford Exploration Project, had developed a technique to more accurately perform seismic imaging, that nowadays is viewed as a prototype of modern compressed sensing algorithms. However, their results were presented within the framework of seismology, and had very little impact outside of that field; to the extent that other scientists were aware of it at all, they may have believed it to be some sort of special "trick" that was specific to the seismology context that could not be transferred to, say, astronomy or medical imaging.
By reformulating the measurement problem into the abstract language of linear algebra - which is part of the mathematical language common to all the sciences - and through the efforts of several key scientists in translating this language into terms that could be easily grasped by experts in various scientific domains - it became possible to persuasively communicate the essential insights of compressed sensing across disciplines, and in particular to unlock the otherwise field-specific nuggets of understanding that isolated research communities had uncovered, and share them far more broadly. All in all, compressed sensing is a great success story involving the collaboration of mathematicians, scientists, engineers, industry, and public funding agencies, that I am very proud to have contributed to; and the return on public investment has been substantial (especially on the pure mathematical side, as research expenses here tend to be somewhat lower than in other scientific disciplines). (4/4)

2025-08-04 00:26:01 UTC

- reply

This was quite a practical consideration, since in order for the manufacturers of expensive MRI machines (Siemens, GE, Phillips, Toshiba, etc.) to actually invest significant R&D resources into trying to implement compresssed sensing algorithms into their latest models (which they have all now done), they needed a high level of assurance that they would not run into fundamental obstacles in actually making the theoretical arguments work in practice. Here, it was not just any individual theorem produced by myself or others, but the remarkable breadth of compressed sensing results in the mathematical signal processing literature (using quite diverse areas of mathematics to reach the same conclusions), as well as empirical compressed sensing experiments in other disciplines that the mathematics now indicated were analogous to the medical imaging context, that were key in persuading these companies that the risks were low enough that it made fiscal sense to actually make the needed investments. (3/4)

2025-08-04 00:25:49 UTC

- reply

In this case, what the mathematical theorems brought to the field was a clarity, insight, generality, and level of trust that was not being produced just from the empirically derived results alone. In many cases, the observed efficiencies of compressed sensing type algorithms that had been empirically reported could not be reliably reproduced by other researchers, for a number of reasons, but one of which was that the key insight that compressed sensing required *three* crucial ingredients to work (sparse representation of data, incoherent sampling, and nonlinear reconstruction), and would fail if only one or two of these ingredients was present, was not clearly communicated in these works. The empirical results may have mentioned one or two of these ingredients as a possible speculative explanation of the compressed sensing phenomenon, but it required mathematical analysis to identify all three, and to clarify the types of measurement problems for which compressed sensing could work, and the ones for which it would not. (2/4)

2025-08-04 00:25:35 UTC

A followup to my recollections on the early history of compressed sensing from my previous post. Regarding the mathematical contributions of Candes, myself, Romberg, Donoho, and others to the subject, it has been argued that the rigorous theorems that guaranteed with mathematical certainty that compressed sensing algorithms actually worked (assuming three key hypotheses, of which more later) was not as necessary as advertised, since researchers in medical imaging (as well as in other fields, such as seismology, astronomy, and statistics) were empirically discovering very similar algorithms at various times (including some that predate my own work by decades).
This question is one of the main themes of this talk by David Donoho at the 2018 ICM on the occasion of his receiving the Gauss prize: https://www.youtube.com/watch?v=mr-oT5gMboM&ab_channel=RioICM2018 . I recommend the entire talk (and the special shout out to IPAM he gives halfway through, and the role of federal funding more broadly), but can summarize some of the points here. (1/4)

2025-08-02 02:37:05 UTC

- reply

IPAM (pictured here in a photo I took today), as one of the six NSF-funded math institutes, has been a great success since its founding in 2000. Its specialty is creating three-month programs where participants (both junior and senior) from two or more fields of mathematics, science, or industry interact through workshops, participant-driven seminars, and informal interactions, centered around a theme that had been identified as particularly fertile for bringing together two or more otherwise disparate communities.
One well-known example that I was involved many years ago was the 2004 program https://www.ipam.ucla.edu/programs/long-programs/multiscale-geometry-and-analysis-in-high-dimensions/ on Multiscale geometry and analysis in high dimensions, where the organizers had identified the potential for bringing together pure mathematicians whose work involved geometry at multiple scales with scientists interested in such applied topics as signal processing or the accurate modeling of materials. I participated extensively in this program, and in particular interacted quite a bit with one of the organizers (Emmanuel Candes) as well as Justin Romberg, leading to several foundational papers in the field now known as "compressed sensing", which permits (in certain circumstances) the rapid acquisition of high-resolution images or other information from a relatively small number of measurements. (Perhaps the most well known applications of the compressed sensing algorithms that came out of the work of Emmanuel, myself, Justin, David Donoho, and others was the ability to speed up the time required for a medical-grade MRI scan by up to an order of magnitude.) (2/4)
https://media.mathstodon.xyz/media_attachments/files/114/956/842/222/491/398/original/aabc63ba52fb02b8.jpg

2025-08-02 02:36:27 UTC

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 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 percentage 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)

2025-07-25 19:49:59 UTC

- reply

Many of the proposed use cases for AI tools try to place such tools in the "blue team" category, such as creating code, text, images, or mathematical arguments in some semi-automated or automated fashion, that is intended for use for some external application. However, in view of the unreliability and opacity of such tools, it may be better to put them to work on the "red team", critiquing the output of blue team human experts but not directly replacing that output; "blue team" AI use should only be permitted up to the capability of one's "red team" to catch and correct any errors generated. This approach not only plays to current AI strengths, such as breadth of exposure and fast feedback, but also mitigates the risks of deploying unverified AI output in high-stakes settings.
In my own personal experiments with AI, for instance, I have found it to be useful for providing additional feedback on some proposed text, argument, code, or slides that I have generated (including this current text). I might only agree with a fraction of the suggestions generated by the AI tool; but I find that there are still several useful comments made that I do agree with, and incorporate into my own output. This is a significantly less glamorous or intuitive use case for AI than the more commonly promoted "blue team" one of directly automating one's own output, but one that I find adds much more reliable value. (3/3)

2025-07-25 19:49:47 UTC

- reply

The blue team / red team distinction extends beyond cybersecurity to many other disciplines as well. In software engineering, for instance, "blue teaming" might correspond to the generation of new computer code, while "red teaming" would consist of such tasks as quality assurance and testing of such code. In mathematics, "blue teaming" could involve coming up with speculative ideas to solve a math problem, while "red teaming" checks the arguments for formal errors, and also raises heuristic objections to a blue team approach being viable. (See also my discussion about "local" and "global" errors in mathematics at https://terrytao.wordpress.com/advice-on-writing-papers/on-local-and-global-errors-in-mathematical-papers-and-how-to-detect-them/ ).
I like to refer to these two teams in mathematics as the "optimists" and "pessimists"; in my experience, the strongest collaborations arise when there is a roughly equal split between the optimists and pessimists in the collaborations. (Depending on the collaboration, I myself have sometimes played the optimist, sometimes the pessimist, and sometimes a mixture of both.) (2/3)

2025-07-25 19:49:34 UTC

In the field of cybersecurity, a distinction is made between the "blue team" task of building a secure system, and the "red team" task of locating vulnerabilities in such systems. The blue team is more obviously necessary to create the desired product; but the red team is just as essential, given the damage that can result from deploying insecure systems.
The nature of these teams mirror each other; mathematicians would call them "dual". The output of a blue team is only as strong as its weakest link: a security system that consists of a strong component and a weak component (e.g., a house with a securely locked door, but an open window) will be insecure (and in fact worse, because the strong component may convey a false sense of security). Dually, the contributions to a red team can often be additive: a red team report that contains both a serious vulnerability and a more trivial one is more useful than a report that only contains the serious issue, as it is valuable to have the blue team address both vulnerabilities. (But excessive low-quality reports can dilute attention from critical issues.)
Because of this, unreliable contributors may be more useful in the "red team" side of a project than the "blue team" side, though the blue team can still accommodate such contributors provided that the red team is competent enough to catch almost all of the errors that the contributor to the blue team might make. Also, unreliable red team contributions only add value if they _augment_ the output of more reliable members of that team, rather than _replace_ that output, and if their output can be effectively filtered or triaged by more experienced red team members. (1/3)

2025-07-19 18:56:04 UTC

- reply

In each of these formats, the submitted solutions are still technically generated by the high school contestants, rather than the team leader. However, the reported success rate of the students on the competition can be dramatically affected by such changes of format; a student or team of students who might not even reach bronze medal performance if taking the competition under standard test conditions might instead reach gold medal performance under some of the modified formats indicated above.
So, in the absence of a controlled test methodology, one should be wary of making 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. (3/3)

2025-07-19 18:55:45 UTC

- reply

But consider what happens to the difficulty level of the Olympiad if we alter the format in various ways:
* One gives the students several days to complete each question, rather than four and half hours for three questions. (To stretch the metaphor somewhat, consider a sci-fi scenario in the student is still only given four and a half hours, but the team leader places the student in some sort of expensive and energy-intensive time acceleration machine in which months or even years of time pass for the student during this period.)
* One gives the students unlimited access to calculators, computer algebra packages, textbooks, or the ability to search the internet.
* One has the six student team work on the same problem simultaneously, communicating with each other on their partial progress and reported dead ends.
* The team leader gives the students prompts in the direction of favorable approaches, and intervenes if one of the students is spending too much time on a direction that they know to be unlikely to succeed.
* Each of the six students on the team submit solutions, but the team leader selects only the "best" solution to submit to the competition, discarding the rest.
* If none of the students on the team obtains a satisfactory solution, the team leader does not submit any solution at all, and silently withdraws from the competition without their participation ever being noted. (2/3)

2025-07-19 18:55:27 UTC

It is tempting to view the capability of current AI technology as a singular quantity: either a given task X is within the ability of current tools, or it is not. However, there is in fact a very wide spread in capability (several orders of magnitude) depending on what resources, assistance, and reporting methods one uses to assess the tool.
One can illustrate this with a human metaphor. I will use the recently concluded International Mathematical Olympiad (IMO) as an example. Here, the format is that each country fields a team of six human contestants (high school students), led by a team leader (often a professional mathematician). Over the course of two days, each contestant is given four and a half hours on each day to solve three difficult mathematical problems, given only pen and paper. No communication between contestants (or with the team leader) during this period is permitted, although the contestants can ask the invigilators for clarification on the wording of the problems. The team leader advocates for the students in front of the IMO jury during the grading process, but is not involved in the IMO examination directly.
The IMO is widely regarded as a highly selective measure of mathematical achievement for a high school student to be able to score well enough to receive a medal, particularly a gold medal or a perfect score; this year the threshold for the gold was 35/42, which corresponds to answering five of the six questions perfectly. (1/3)

2025-07-19 03:32:34 UTC

The IMO is concluding today in the Sunshine Coast of Australia with the prize ceremony, which I will be participating in.
There was not an official controlled competition set up for AI models for this year’s IMO, but unofficially 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 to arrive at the solutions: https://imo2025.au/news/the-66th-international-mathematical-olympiad-draws-to-a-close-today/ . Hopefully by next year we will have a controlled environment to get some scientific comparisons and evaluations, possibly using the AIMO format.

2025-07-05 15:57:53 UTC

"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/5)

2025-06-14 23:59:55 UTC

Earlier this year, I sat down for an extended interview with Lex Friedman on a variety of topics in mathematics, proof formalization, and AI. The edited (and nicely illustrated) form of the video, clocking in at over three hours, is now available: https://www.youtube.com/watch?v=HUkBz-cdB-k

2025-06-13 18:57:43 UTC

Maryna Viazovska is launching a project to formalize a proof of her well-known result that the E_8 lattice is the optimal sphere packing in eight dimensions. The announcement can be found at https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Sphere-Packing/with/523951357 where you can also find a talk by Viazovska describing the project.
Among other things, the project will develop some of the classical theory of modular forms and complex analysis, which is only partially in Lean's Mathlib at present. For instance, Cauchy's theorem is only currently available for rectangular contours, which means that the valence formula for modular forms (which is usually proven using Cauchy's theorem applied to a non-rectangular contour) is not yet formalized.

2025-05-31 17:23:59 UTC

I have just launched a "Lean companion" to my real analysis undergraduate textbook "Analysis I" at https://github.com/teorth/estimate_tools/blob/master/EstimateTools/analysis/README.md . This gives a Lean translation (or paraphrasing) of the various definitions, theorems, and exercises in the textbook into Lean, thus allowing for an alternate way for students to work through the text. It is also designed to gradually transition into the standard Lean library Mathlib, thus also potentially serving as an introduction to that library as well.
Further discussion at https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/

2025-05-31 17:06:30 UTC

- reply

@nprofile…4xpp The plan is to provide extensive data of AlphaEvolve's attempts at a given problem over time (generally AE tries a variety of tehcniques, including calling up existing optimization methods from libraries which we provide it). The interface for exploring AE's tree of attempts is currently being developed but should be available in a few months.

2025-05-30 16:33:56 UTC

One of the numerical exponents that was improved via Deepmind's AlphaEvolve (AE) program (as part of a collaboration I am involved in) has just been improved: https://arxiv.org/abs/2505.16105
The question concerns the best exponent θ for which one can construct large sets of integers A,B with |A+B| = O(|A|) and |A-B| >> |A|^θ. The previous best construction, due to Gyamarti, Hennecart, and Ruzsa in 2007, gave a lower bound of 1.14465; our group was able to use AlphaEvolve to obtain the improvement 1.1584; and this new paper obtains 1.173050. (The best known upper bound is 4/3.)
All constructions proceed by first locating an auxiliary finite set U of integers with good properties. The original construction of Gyamarti et al. was a set of cardinality 30000 or so, constructed according to a specific recipe; AE did an unconstrained search and found a better example of cardinality 54265 that gave the better bound; and the new paper returns to (a modification) of the original construction but with much larger parameters to find (with computer assistance) a set with more than 10^43546 elements.
It is tempting to simplify this to a zero-sum narrative of "winners" and "losers", but I think it is great that different approaches can complement each other here to make mathematical progress. The advantages of an AE-type approach are more in the direction of breadth rather than depth; one can scan large ranges of problems to identify places where the literature could be improved, and then human experts can then focus attention on these problems to make further progress.

2025-05-29 14:52:52 UTC

- reply

@nprofile…mnlf @nprofile…rrr0 If this were a software tool rather than a data repository then I would share these concerns, but as it stands the repository is relatively easy to fork into a community project (which I believe is permissible under the licensing here, which is a mix of Apache 2.0 and CC-BY) and I view the risk of lock-in here to be low. To me it is the data set of formalized conjectures that is the main valuable resource, rather than the precise format, standards, or interface used for that data set; even if in the future Deepmind decides to make the latter proprietary and/or closed-access for their version of the repository, a community fork of the last open-source version of the data set would still be usable and of value to the community.
In any case, I expect there to be many more repositories of formalized theorems and conjectures (both from the community and from private entities) than this one in the future (there are already some small databases of this type for, say, Putnam problems), and I don't think we will end up in anything close to a monopoly situation with regards to such databases.

2025-05-29 01:48:33 UTC

- reply

@nprofile…rrr0 I'm not sure I understand the issue in 1): the conjectures listed in this database are all drawn from public sources, and are already part of the scientific commons. I see no reason why a private company should not be allowed to access this common resource, or to use that resource to build databases in a fashion that is non-exclusionary to other parties.
2) Actually in recent years the fraction of mathematics that can be formalized in Lean's Mathlib has expanded significantly. Just to give one example, the notion of a perfectoid space is formalized: https://leanprover-community.github.io/lean-perfectoid-spaces/ . While formalizing the _proofs_ of the core theory of mathematics is still far from reality, the goal of formalizing the majority of the _statements_ of key concepts and conjectures seems quite feasible to me within a few years (particularly with AI assistance).
In general, I would view these developments in positive-sum terms rather than zero-sum terms. If a contribution to mathematics is positive across all subfields, but has a stronger positive contribution in one subfield than in another, I would still view this as a net positive for mathematics, especially given that in time the subfields which could not immediately utilize the contribution can eventually figure out how to do so.

2025-05-28 17:12:54 UTC

Google #DeepMind has launched an open repository of formalized mathematics conjectures https://github.com/google-deepmind/formal-conjectures . For instance, the four Landau problems in analytic number theory are formalized at https://github.com/google-deepmind/formal-conjectures/tree/main/FormalConjectures/LandauProblems . They are soliciting further contributions to the database.
It is of course far easier to state an open problem than it is to prove it, but having some sort of standardized formulation of such problems is important first step if one is to hope to use automated tools to help make progress on these problems. If one naively asks an AI tool to formally solve an informally specified problem, it is far more likely that it could succeed on a technicality by establishing a formal statement which contains a trivial edge case that can be established (e.g., if some key parameter is intended to be non-zero, but the formalization permits the parameter to vanish), than it is to solve the problem as intended.

2025-05-25 14:42:37 UTC

The NSF has reduced spending on the basic sciences by 50% or more in 2025, with similar cuts proposed for next year as well. For instance, through to May 21 of this year, the funding awarded to the mathematical sciences is currently $32 million, compared to the 10-year average of $113 million. (These are of course large numbers for to an individual, but with the US population of 340 million, this amounts to spending less than 22 cents per American per year on basic mathematical research, compared to the 10-year average of 80 cents per American per year.) https://www.nytimes.com/interactive/2025/05/22/upshot/nsf-grants-trump-cuts.html
I myself have been fortunate to be supported by a small fraction of this 80 cents for almost the entirety of my professional career, allowing me to conduct research in the summer, invite speakers to my department, and to support graduate students. For now, I can continue these activities at a minimal level using by existing (and relatively modest) NSF grant https://www.nsf.gov/awardsearch/showAward?AWD_ID=2347850 , but already I do not have the resources to put into any future long-term projects. For instance, my experiments with using new technologies for mathematical workflows is being conducted purely by myself and contributions from unpaid online volunteers; I am applying for funding from several sources for these projects, but I am expecting the process to be extremely competitive. (1/3)

2025-05-14 20:17:54 UTC

I've been working (together with Javier Gomez-Serrano) with a group at Google Deepmind to explore potential mathematical applications of their tool "AlphaExplore", a successor of their earlier tool "Funsearch" that was publicly announced today: https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/ . Very roughly speaking, this is a tool that can attempt to extremize functions F(x) with x ranging over a high dimensional parameter space Omega, that can outperform more traditional optimizations when the parameter space is very high dimensional and the function F has non-obvious structural features.
Some of the preliminary problems we have tried this on, including problems involving harmonic analysis inequalities, additive combinatorics, and packing, were already mentioned in the announcement; we are now gradually moving on to more challenging problems where the parameter space has a sparser set of good solutions. The work is still ongoing, but I hope to be able to report more upon it when we are closer to completion (probably a few months from now).

2025-05-13 15:00:43 UTC

- reply

I think the conclusion to draw is that the optimal level of automation is actually somewhere strictly between 0% and 100% - enough automation at each scale to reduce the amount of tedious repetition of effort, but still enough of a "human in the loop" at each scale to review and fix local issues in order to allow the human to retain a sense of the structure of the task at all scales. Benchmarking excessively at a single scale of this process may, ironically, end up being detrimental to the longer term goal of scaleable, usable, and illuminating formalization of the entire corpus of informal mathematics (cf. "Goodhart's law").
(2/2)

2025-05-13 15:00:27 UTC

One lesson I am learning from my autoformalization experiments is that even if one focuses purely on efficiency (and only accepting formalizations that actually compile in the proof assistant and produce the desired result), the scale at which one measures the efficiency is now making a significant difference. Consider the following four different measures of efficiency, at different scales of proof sizes:
1. Making it faster to formalize any individual line in the proof.
2. Making it faster to formalize any individual lemma in the proof.
3. Making it faster to formalize any individual proof of a theorem.
4. Making it faster to formalize an entire textbook of results.
What I am realizing is that many of the current automation tools can accelerate formalization at one of these scales, but
- counter-intuitively - that overreliance on such a tool may end up degrading one's ability to formalize at other scales. For instance, the dependent type matching tool `canonical` can excel at the scale 1 task of formalizing an individual line, but by blindly accepting `canonical`'s resolution of that step and then moving on to the next step, I lost a personal sense of how the steps of the proof tied together, making it a little more difficult to diagnose and fix errors at scale 2. On the other hand, the exercise of fixing such errors gave me some sense of how lemmas interacted with each other, and helped with the task at scale 3. (1/2)

2025-05-02 04:38:26 UTC

- reply

@nprofile…k6c8 The crucial difference is that we have formal proof verifiers that can verify with near-absolute certainty that a given AI-generated proof is correct, which can make it acceptable for mathematical applications no matter how many "vibes" went into generating it.
(That said, one still has to make sure that the formalization of the _statement_ of one wants to prove is correct. This may still need to be largely done (or at least reviewed by) expert humans in the near to medium term. However, the task of formalizing the statement of a theorem can be considerably easier than that of formalizing its proof (example: Fermat's last theorem), so this already could lead to a massive efficiency gain in formalization.)

2025-05-01 17:35:34 UTC

DARPA's "Exponentiating mathematics" (expMath) program, which is launching a challenge to develop and evaluate "AI collaborators" for assist in either decomposing a large informal mathematical proof into smaller lemmas, or formalizing these lemmas, is now taking short abstract proposal submissions: https://sam.gov/opp/869c8d7351c04234be43c45e2082b846/view

2025-04-10 00:03:26 UTC

Perhaps this does not need to be said, but $\Delta \tau_i = \frac{x_i - m_i}{\epsilon * \varphi * m_i$ is, in no shape or form, anything remotely resembling a solution to a mean field equation in a highly non-perturbative and non-linear regime.

2025-03-26 23:35:00 UTC

- reply

As with previous advances in mathematics automation, students will still need to know how to perform these operations manually, in order to correctly interpret the outputs, to craft well-designed and useful prompts (and follow-up queries), and to able to function when the tools are not available. This is a non-trivial educational challenge, and will require some thoughtful pedagogical design choices when incorporating these tools into the classroom. But the payoff is significant: given that such tools can free up the significant fraction of the research time of a mathematician that is currently devoted to such routine calculations, a student trained in these tools, once they have matured, could find the process of mathematical research considerably more efficient and pleasant than it currently is today. (3/3)

2025-03-26 23:34:24 UTC

- reply

Today, it is increasingly commonplace for human mathematicians to also outsource symbolic tasks in such fields as linear algebra, differential equations, or group theory to modern computer algebra systems. We still place great emphasis in our math classes on getting students to perform these tasks manually, in order to build a robust mathematical intuition in these areas (and to allow them to still be able to solve problems when such systems are unavailable or unsuitable); but once they have enough expertise, they can profitably take advantage of these sophisticated tools, as they can use that expertise to perform a number of "sanity checks" to inspect and debug the output of such tools.
With the advances in large language models and formal proof assistants, it will soon become possible to also automate other tedious mathematical tasks, such as checking all the cases of a routine but combinatorially complex argument, searching for the best "standard" construction or counterexample for a given inequality, or performing a thorough literature review for a given problem.
To be usable in research applications, though, enough formal verification will need to be in place that one does not have to perform extensive proofreading and testing of the automated output. (2/3)

2025-03-26 23:34:12 UTC

In the first millennium CE, mathematicians performed the then-complex calculations needed to compute the date of Easter. Of course, with our modern digital calendars, this task is now performed automatically by computers; and the older calendrical algorithms are now mostly of historical interest only.
In the Age of Sail, mathematicians were tasked to perform the intricate spherical trigonometry calculations needed to create accurate navigational tables. Again, with modern technology such as GPS, such tasks have again been fully automated, although spherical trigonometry classes are still offered at naval academies.
During the Second World War, mathematicians, human computers, and early mechanical computers were enlisted to solve a variety of problems for military applications such as ballistics, cryptanalysis, and operations research. With the advent of scientific computing, the computational aspect of these tasks has been almost completely delegated to modern computers, although human mathematicians and programmers are still required to direct these machines. (1/3)

2025-03-17 01:49:28 UTC

A new #CosmicDistanceLadder post, on how the recent lunar eclipse from the vantage point of the Earth becomes a solar eclipse from the vantage point of the Moon: https://www.instagram.com/p/DHR1tuWonDR/

2025-03-15 22:07:48 UTC

- reply

Another role that mathematical negative results can play is to focus attention on the minimal component of a proposed technology that is in conflict with such results. For instance, regardless of whether the law of conservation of energy holds or not, it is a mathematical theorem (assuming additivity of energy) that if a machine fails to conserve energy, then at least one of its components must do so as well. And so, if forced to evaluate some complex "Rube Goldberg" design of a perpetual motion machine, it becomes natural to insist that the inventor identify at least one atomic component of this machine that violates this law. (There is a similar technique when reading papers claiming to prove a difficult result: see https://terrytao.wordpress.com/advice-on-writing-papers/on-the-strength-of-theorems/ ) (6/7)

2025-03-15 22:07:37 UTC

- reply

But also, by mathematically identifying the precise hypotheses and axioms needed to establish a negative result, one can gain valuable clues as to how to find a substitute positive result. For instance, by identifying the role of conservation of money axiom in preventing the global profitability a pyramid scheme, one can see how it is possible, in economies where wealth can be created over time via long-term investment, to create social insurance schemes (such as Social Security in the US) that can generate broad social benefits despite having some superficial resemblance to a pyramid scheme. (This is not to say that such schemes are guaranteed to be sustainable over the long term, especially if mismanaged or designed badly; but it is not mathematically impossible for this to be the case.) Or: mathematical compression of all data is impossible; however, this reveals the possibility that compression of specific types of data, such as text, is still feasible, but must somehow utilize the structural properties of that data. (5/7)

2025-03-15 22:05:21 UTC

But also, by mathematically identifying the precise hypotheses and axioms needed to establish a negative result, one can gain valuable clues as to how to find a substitute positive result. For instance, by identifying the role of conservation of money axiom in preventing the global profitability a pyramid scheme, one can see how it is possible, in economies where wealth can be created over time via long-term investment, to create social insurance schemes (such as Social Security in the US) that can generate broad social benefits despite having some superficial resemblance to a pyramid scheme. (This is not to say that such schemes are guaranteed to be sustainable over the long term, especially if mismanaged or designed badly; but it is not *mathematically* impossible for this to be the case.) Or: mathematical compression of all data is impossible; however, this reveals the possibility that compression of specific types of data, such as text, is still feasible, but must somehow utilize the structural properties of that data. (5/7)

2025-03-15 22:04:55 UTC

- reply

The value of a positive technological breakthrough is obvious. Negative results however are also valuable and important, though in significantly less intuitive fashions. Firstly, they allow for more efficient allocation of resources: with the knowledge of negative results, scarce R&D funding can be allocated away from, say, the design of perpetual motion machines and towards more feasible goals, such as increasing the fuel efficiency of engines (though given the residual uncertainties and the potential payoffs, it is still rational to allow for a very small and lightly funded amount of research activity into proper mathematical and scientific analysis of possible loopholes in the conservation of energy argument). (4/7)

2025-03-15 22:04:41 UTC

- reply

Mathematical arguments come the closest to providing a completely bulletproof negative result, although even mathematical reasoning must rely on some axioms. For instance, it is mathematically impossible to design a pyramid scheme in which everyone involved profits monetarily at the end of the scheme, if one assumes the axiom that the total amount of
money in the system is preserved. The "strategy stealing argument" similarly shows that, with some basic axioms concerning the free market, it is not possible to create a publically describable strategy to play the stock market with guaranteed positive returns, based only on publicly available information. Information theory shows that it is not possible to design a compression algorithm that can compress every single type of data input into a smaller size. And so forth. (3/7)

2025-03-15 22:04:21 UTC

- reply

There are a small number of physical laws that are considered so fundamental and universally applicable that they provide much stronger negative results. Famously, the law of conservation of energy prohibits the existence of a perpetual motion machine that produces more energy output than energy input over extended periods of time, while Einstein's theory of special relativity (together with basic axioms of causality) prohibits faster than light travel for any object capable of carrying information. Even in such cases, though, some loopholes remain. For instance, there are mathematically viable (though practically impossible) "warp drives" that exploit the spacetime-distorting effects of extremely massive objects to achieve travel that is faster than light at global scales, despite not exceeding the light speed limit at any local point in the trajectory. (2/7)

2025-03-15 22:04:04 UTC

Science and technology can produce positive results that can be extremely convincing: a successful demonstration of heavier-than-air flight, for instance, is hard to refute (assuming of course that no fraudulent manipulation of the presentation was made, such as editing of the video recordings). Negative results, by their nature, are much more provisional in nature. Suppose for instance that a prototype heavier-than-air machine fails to take flight. This can be useful experimental data for future designs, but it does not provide strong evidence that such flight is physically impossible.
Empirical laws of nature can provide stronger negative evidence, but they are still not ironclad, as many such laws have limitations on their range of applicability. For instance, Archimedes law of bouyancy is an empirically valid law which does seem to provide a strong obstruction to heavier-than-air flight; but of course such powered flight is still possible, as one needs to recognize that Archimedes' law only applies to fluids in static equilibrium, as opposed to dynamic fluid flows where additional effects such as aerodynamic lift are in play. (1/7)

2025-03-11 17:04:25 UTC

The National Academies is now taking nominations for the 2025 Eric and Wendy Schmidt Awards for Excellence in Science Communications, which honor exceptional science communicators, journalists, and research scientists who have developed creative, original work to communicate issues and advances in science, engineering, or medicine for the general public. Applications close Mar 31. https://www.nationalacademies.org/news/2025/02/submission-period-now-open-for-the-2025-eric-and-wendy-schmidt-awards-for-excellence-in-science-communications-640-000-to-be-awarded

2025-03-01 22:44:19 UTC

- reply

@nprofile…307x My general impression is that any topic that already has a reasonable Wikipedia page can be accurately summarized by LLM tools, in particular being able to succinctly answer precise basic questions without requiring detailed parsing of longer partly relevant texts, which is particularly important in a lecture environment where one still wants to keep most of one's attention on the talk in real time.

2025-02-27 19:41:03 UTC

- reply

@nprofile…937m Should be fixed now, sorry.

2025-02-27 19:29:16 UTC

Yesterday I attended a lecture on a topic outside of my own area of expertise - the Langlands program and the cohomology of Shimura varieties - and found that it was actually quite helpful to discreetly ask some questions from a large language model during the lecture to help keep up. (A log of my questions can be found here at https://chatgpt.com/c/67bf9fd3-193c-800e-999c-05408cfb8845 .) There is still some cultural resistance to having audience members access their computers and other devices during a lecture, but I think there is some non-trivial value in permitting this sort of augmentation of the lecture so long as it is not disruptive or distracting, and I wonder if cultural norms about this sort of assistance will evolve over time.

2025-02-26 04:48:49 UTC

I am happy to announce that the Kakeya set conjecture, one of the most sought after open problems in geometric measure theory, has now been proven (in three dimensions) by Hong Wang and Joshua Zahl! https://arxiv.org/abs/2502.17655 I discuss some ideas of the proof at https://terrytao.wordpress.com/2025/02/25/the-three-dimensional-kakeya-conjecture-after-wang-and-zahl/

2025-02-24 18:51:10 UTC

I wrote a blog post on how a piece of pure mathematics - the development of the landscape function in PDE - played a part in realizing noticeable savings in household energy bills due to improved LED lighting technology: https://terrytao.wordpress.com/2025/02/23/closing-the-green-gap-from-the-mathematics-of-the-landscape-function-to-lower-electricity-costs-for-households/

2025-02-21 17:04:22 UTC

- reply

The American Mathematical Society has also started a page to coordinate support for professional mathematics, so far focusing on executive orders impacting the National Science Foundation: https://www.ams.org/government/getinvolved-dc#/

2025-02-20 22:11:29 UTC

The current administration has proposed to cap indirect costs (which covers laboratory maintenance, equipment provision and salaries for support and administrative staff) at the National Institute for Health at 15%, from the current levels of 50%-70%, which will likely make many ongoing research projects impossible to continue in their current form.
My own mathematics department receives very little direct funding from the #nih; but already the mere *possibility* of such a drastic cap has impacted us; we have been unable to make a job offer to an outstanding candidate because the budget uncertainty created by this proposal has forced my university to close off almost all discretionary sources of funding for faculty hiring at all departments, regardless of their level of NIH support.
My university, as well as many others, are circulating a letter of support for NIH funding of biomedical research, for which the US is currently an international leader. The letter is available for anyone to sign at https://docs.google.com/forms/d/1Agzz5mQgfEMpLlBhoE4ZyHdiTvdc9O84zF4vNEHyKTI/viewform?edit_requested=true