Terence Tao

As with many other real-world distributions, the class of open problems in mathematics has a "long tail" - a large number of problems which would be relatively easy to prove or disprove, but which have not recieved significant attention from the (limited) number of expert mathematicians available. To switch metaphors, this tail can thus contain a large amount of "low-hanging fruit" of new mathematical results that could be obtained if there was some way to automatically attack these problems at scale. I saw this first-hand when running the Equational Theories Project last year, in which 22 million implications in universal algebra were attacked (and ultimately resolved). Initial passes with low-tech automated methods resolved a large percentage of these implications within days, with increasingly sophisticated methods brought to bear to pick off the more stubborn holdouts that resisted earlier sweeps. The final few implications took months of human effort to settle:

GitHub

Terence Tao's personal log

A project to map out the relations between different equational theories of Magmas. - teorth/equational_theories

(1/3)

A new paper with Bogdan Georgiev, Javier Gomez-Serrano, and Adam Zsolt Wagner: "Mathematical exploration and discovery at scale"

arXiv.org

Mathematical exploration and discovery at scale

AlphaEvolve (Novikov et al., 2025) is a generic evolutionary coding agent that combines the generative capabilities of LLMs with automated evaluati...

, 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

GitHub

GitHub - google-deepmind/alphaevolve_repository_of_problems

Contribute to google-deepmind/alphaevolve_repository_of_problems development by creating an account on GitHub.

and further discussion is at

What's new

Mathematical exploration and discovery at scale

Bogdan Georgiev, Javier Gómez-Serrano, Adam Zsolt Wagner, and I have uploaded to the arXiv our paper “Mathematical exploration and dis...

Another interesting example of modern computer assistance in mathematics, again involving the

Erdős Problems

site: Problem #707 (

Erdős Problem #707

), previously marked as "open", is now "disproved" - with the disproof formalized in Lean :

Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof

. But the path towards that disproof was quite unusual, not fitting neatly into any of the standard narratives about AI in mathematics: * The authors' initial proof used some numerical computer experiments, but did not get much help from LLMs initially, with even the code generated by hand. * The authors then found a disproof by conventional human arguments (and also obtained some stronger results of a similar nature), and did not turn up any prior solution to this problem in their literature searches. Even the modern AI deep research tools did not locate any hits. * Nevertheless, as part of the process of writing the paper, they found a solution to the problem (slightly different from theirs) had been obtained by Hall, thirty years before Erdos even posed the problem! * Perturbed by this, the authors then decided to formalize both their result and Hall's result in Lean. (1/3)

I am increasingly of the opinion that the most productive near-term adoptions of AI in mathematics will primarily come not from applying the most powerful models to the most challenging problems (although we will see a few isolated examples of progress along those lines, especially when large amounts of computational resources and expert attention are applied), but from using medium-powered tools to accelerate and scale up more mundane and time-consuming, but still essential, research tasks, using the accumulated human experience with (and understanding of) such tasks to guide, verify, and safely incorporate the AI output into one's workflows. In such use cases, the output of the AI tool could also have been produced (with increased expenditure of time and attention) by a human expert - but this is actually a feature rather than a bug, as it allows for the AI output to be readily and reliably assessed, confirmed, and converted to a format that such experts are already comfortable working with. An example of such a mundane task is literature review: locating relevant prior literature on a given problem. If the problem already has a commonly agreed upon name, as well a well-established community of researchers working on it, then existing web search and bibliographic search tools are already more than adequate to find both past and current literature on the problem: in particular, the citation graph between the literature will be dense enough that one can start with one key paper in the subject and perform both forward and backward citation searches to obtain a reasonably complete picture of the current state of knowledge on the problem. (1/4)

I was able to use an extended conversation with an AI https://chatgpt.com/share/68ded9b1-37dc-800e-b04c-97095c70eb29 to help answer a MathOverflow question

MathOverflow

Is the least common multiple sequence $\text{lcm}(1, 2, \dots, n)$ a subset of the highly abundant numbers?

I've been comparing the sequence of the Least Common Multiple of the first $n$ integers, $L_n = \text{lcm}(1, 2, \dots, n)$, with the sequence of H...

. I had already conducted a theoretical analysis suggesting that the answer to this question was negative, but needed some numerical parameters verifying certain inequalities in order to conclusively build a counterexample. Initially I sought to ask AI to supply Python code to search for a counterexample that I could run and adjust myself, but found that the run time was infeasible and the initial choice of parameters would have made the search doomed to failure anyway. I then switched strategies and instead engaged in a step by step conversation with the AI where it would perform heuristic calculations to locate feasible choices of parameters. Eventually, the AI was able to produce parameters which I could then verify separately (admittedly using Python code supplied by the same AI, but this was a simple 29-line program that I could visually inspect to do what was asked, and also provided numerical values in line with previous heuristic predictions). Here, the AI tool use was a significant time saver - doing the same task unassisted would likely have required multiple hours of manual code and debugging (the AI was able to use the provided context to spot several mathematical mistakes in my requests, and fix them before generating code). Indeed I would have been very unlikely to even attempt this numerical search without AI assistance (and would have sought a theoretical asymptotic analysis instead).