How Terry Tao Became an Evangelist for AI in Math
Automated proof-checkers such as Lean can provide ironclad assurances that mathematical proofs are valid.
Samuel Velasco/Quanta Magazine. Code courtesy of Alex Kontorovich
Introduction
The following has been adapted from The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett.
Terry Tao has never been afraid of unconventional ideas. In November 2014, he was on a panel of five distinguished mathematicians, all inaugural recipients of the Breakthrough Prize in Mathematics, which came with a $3 million award. The laureates’ conversation ranged from whether mathematics is invented or discovered — most of the mathematicians agreed that, at the very least, it feels like an act of discovery — to an assessment of the odds that we’re living in a digital simulation. “Yeah, I think we’re actually not real,” said Maxim Kontsevich, who did his most important work in the 1990s at the intersection of math and physics.
Yet over the course of the 40-minute discussion, the statements that drew the most incredulity were Tao’s. He predicted that in the future, instead of working alone or in small teams of two or three, mathematicians might work on projects with hundreds of other people at a time. And when these collaborations were over, he said — in his modest, understated way — the results might be checked not by human referees but by computers. “One day we may actually write our papers not in LaTeX, but in some language which some smart software will convert to a formal language, and every so often you’ll get a compilation error — the computer does not understand how you derived this step,” he said.
The statement was greeted by the event moderator and the other laureates as preposterous enough to make the simulation hypothesis seem reasonable by comparison. Even more surprising than the idea of hundreds of mathematicians working together was the fact that such a collaboration would appeal to Tao — because if anyone in the world seemed well suited to going it alone, it was him.
Tao was born in 1975 in Adelaide, Australia, three years after his parents immigrated to the country from Hong Kong. The first signs that their firstborn son was different came early. When Tao was 2 and his family was visiting friends, his parents found him gathered with several 6-year-olds, demonstrating how to count using wooden blocks. Asked how he’d learned to count things, he responded that he had seen it on Sesame Street. Five years later, when Tao was 7, he began learning calculus.
For three weeks in the spring of 1985, Tao’s parents brought him to the United States, where he met with Julian Stanley, director of the Study of Mathematically Precocious Youth, then at Johns Hopkins University. Stanley described Tao as having the greatest mathematical ability he had ever seen. That same year Tao met the acclaimed mathematician Paul Erdős during the latter’s visit to Adelaide. A famous picture shows the grandfatherly Erdős, 72 at the time, reading a document in his lap while Tao, 10 years old with thick black hair, looks on intently, fingers raised thoughtfully to his chin.
Tao’s young legend grew when he entered the International Math Olympiad in 1986. He won a bronze medal that first year, becoming, at the age of 10, the youngest competitor ever to achieve that result. In the two succeeding years he became the youngest-ever silver medalist and finally the youngest person ever to win a gold medal. His formal education proceeded at a similarly accelerated pace. He graduated from the local Flinders University in Adelaide when he was 15 and, in the fall of 1992, boarded a plane with his father for New Jersey, where he started a Ph.D. in math at Princeton University. Erdős had endorsed Tao’s early admission to the program, writing in a letter of recommendation, “I am sure he will develop into a first-rate mathematician and perhaps into a really great one.”
Paul Erdős, 72 at the time, with a 10-year-old Terrence Tao.
Billy Grace Tao
Erdős was right. By the time Tao was 24, he had made enough new discoveries to have his choice of permanent faculty positions; he ultimately decided to settle at the University of California, Los Angeles. Around that time, he met a young English number theorist named Ben Green. The two began collaborating on a proof that certain kinds of patterns called arithmetic progressions — in which the numbers in a set increase by a fixed interval, like 7, 10, 13, 16 — inevitably appear in large collections of prime numbers, despite the fact that primes appear to be scattered randomly along the number line. Their proof would become the signature result of Tao’s early career, contributing to his winning the Fields Medal in 2006, and propelling him to the upper echelons of mathematics.
Tao could have built a successful career without collaborating with anyone, but that’s not the way he liked to work. He viewed working with other researchers as a primary way to discover new ideas — take what you know, pair it with what I know, and see what happens.
This approach led Tao’s mathematical research to range over an unusually broad set of topics, from analytic number theory, including the Green-Tao theorem about prime numbers, to analysis, where he studied properties of the Navier-Stokes equations that describe the behavior of fluids, to algorithms for constructing MRI images from digital data. (The MRI collaboration developed during conversations Tao had with Emmanuel Candès, a statistician then at the California Institute of Technology, while they were both dropping off their kids at preschool.) This thirst for collaborative discovery also led Tao to do a lot of his work in public. In 2007, he started a blog, where he began publishing regular updates about his research. By that point, Tao was one of the most famous mathematicians not only in his field but in the world. His posts received a lot of attention and sometimes led to long exchanges in the comments section, where Tao enthusiastically participated. He did it because he found it fun, and because he hoped the conversation might generate new ideas.
Around that time, another early math blogger had a similar thought. Like Tao, Timothy Gowers was a prominent research mathematician with a taste for public exchange. But rather than trusting serendipity to strike in his blog’s comment section, Gowers wanted to channel public energy in a focused way. In January 2009, he published a blog post announcing his desire to facilitate a new kind of “massively collaborative mathematics.” He would propose a problem in an open online forum, and “anybody who had anything whatsoever to say about the problem could chip in.” He named it the Polymath Project.
Tao jumped in. Like Gowers, he understood that some math problems were more amenable than others to being solved through large-scale collaboration. The key, as Tao wrote in a comment on Gowers’ initial post, was to find problems that could “generate a number of simpler sub-problems … which can largely be worked on in parallel.” By breaking big problems into individual cases, different teams or individuals could work on their own and then assemble their results as pieces of a bigger whole. At the same time, Tao knew that perhaps the biggest challenge with the Polymath model would be organizing: moderating contributions and checking to make sure that all the contributions were correct.
For the first Polymath project, Gowers proposed improving a result called the Hales-Jewett theorem, which was about patterns that appear when you shade cells in a grid with one of two different colors. After a few months of work, coordinated through thousands of comments by dozens of mathematicians, the group had proved a more exact statement about how those coloring patterns emerge. That fall, they released the work as a first-of-its-kind math paper with the pseudonymous byline “D.H.J. Polymath.” Gowers’ experiment had been a success. It allowed many mathematicians — professional and amateur alike — to work together and yielded a proof in the end.
Over the next decade, there were 15 more Polymath projects, some of which Tao led, and the initiative attracted mainstream attention. On October 29, 2011, The Wall Street Journal ran an article called “The New Einsteins Will Be Scientists Who Share” and reported that the Polymath Project had “pioneered a new approach to problem-solving.”
Samuel Velasco/Quanta Magazine
Yet in other ways, the Polymath Project was an idea before its time. Tao found it exhilarating to be at the center of a frenzy of mathematical activity, but he recognized that the comments section of a blog was a limited platform for collaboration. Massive open collaboration increased the likelihood of a certain kind of serendipitous discovery, but at the same time it heightened the odds that any one of the many participants would contribute a mistake. The only way to guard against error was for a moderator to carefully check all the work. But that kind of moderation bottleneck undermined the Polymath vision.
What Tao was really after was an efficient new form of scientific discovery. And after a while, he came to understand that the Polymath model was not it. To make it real, he thought, some kind of computer verification would be needed — a way to check contributions automatically, rather than by hand. But given the state of technology in the 2010s, he might as well have wished for passenger service to Mars.
Tao had been aware of computer-verified mathematics for years. He knew about a few success stories, but he also knew that formal math was still impractical, requiring far more effort than it was worth in most cases. Nevertheless, Tao was intrigued by its potential. Almost uniquely among the world’s elite mathematicians, he saw the potential in new methods for doing mathematics.
In July 2022, in part to satisfy his curiosity, he began to organize a workshop on all the different ways computers were assisting mathematical research. He brought on a team of co-organizers, including Kevin Buzzard, who was at the time the world’s most visible evangelist for formal mathematics.
Going into the conference, Tao regarded Lean, software that allows mathematical proofs to be written and checked as computer code, as a complicated program that would take months to learn. Buzzard convinced him to give it a try. Along with that encouragement, Tao felt a strong responsibility to lead by example — if he was going to continue promoting machine-assisted proof, he needed to start trying it himself.
On October 9, 2023, Tao posted on social media, “I have decided to finally get acquainted with the #Lean4 interactive proof system (using AI assistance as necessary to help me use it).”
On MathOverflow, a popular online discussion forum for mathematicians, Tao found a question about something called Maclaurin’s inequality. He decided to answer it as an experiment in formalization. First, he wrote up the proof as a typical math paper. It was short, only 10 pages long. Then he turned his attention to his real goal: seeing if he could formalize the simple proof in Lean.
Initially, Tao thought he might be able to do it in a week, but he was quickly confronted by the differences between writing math by hand and typing it in Lean. Tao observed that the hard parts of the proof were easy to formalize in Lean, while the simple parts took a surprising amount of work.
In the regular paper, Tao spent no time at all asserting that if you have three numbers, all of which are greater than 1, their sum is necessarily at least 3. But Lean doesn’t abide assertions, and Tao had to spend time digging up a lemma in Mathlib — a digital library of already-formalized mathematics that Lean users draw on when writing proofs — that proved the self-evident relationship. Similarly, in informal math, it’s not necessary to always specify which number system you’re working in. The number 3, for example, is simultaneously an integer, a natural number, and a real number. In his original paper, Tao could simply write “3” without specifying what kind of 3 he had in mind. However, in Lean he had to spell it out. Tao found his proof kept failing to compile because he had neglected to specify the correct type at different points in the formalization. It wasn’t until nearly a month later, on November 6, that Tao posted in a comment on his blog, “Just a remark that I have managed to formalize the results of this paper in Lean4.” The result was minor, and the Lean code he had written to formalize it was terrible. Yet Tao was now officially a contributing member of the Lean community.
At the same time he was learning Lean, Tao continued work on a host of other research projects. These included one with his longtime collaborators Ben Green and Tim Gowers, as well as Freddie Manners, a former student of Green’s and now a professor at the University of California, San Diego. It was an elite set of collaborators — Gowers, like Tao, had won a Fields Medal, while Green was among the most decorated number theorists in the field.
The group had a particular problem in their sights, one that revolved around a mathematical object called a sumset. If you have a collection of numbers, it can be used to form another, related collection: its sumset. The sumset is made by taking the sum of every unique pair of numbers in the first set. All those sums together form the sumset of the original set.
If the original set is full of random numbers, then its sumset will be comparatively large. A set of 10 random numbers has a sumset of about 50 numbers (and a set of 1,000 numbers has a sumset of about 500,000 numbers). But if, instead of containing random numbers, the original set follows some kind of pattern, its sumset will be much smaller because many sums will appear multiple times (and you only include each sum once in the sumset). The set of the numbers 1 to 10 is one example — its sumset only contains 17 numbers (not 50, as you’d expect if it were a random collection of 10 numbers), because many of the sums repeat (1 + 6, 2 + 5, and 3 + 4 all equal 7, and you only enter 7 once in the sumset).
In addition to having a small sumset, the numbers 1 through 10 are an example of an arithmetic progression because they increase by a constant interval. A conjecture with roots in the 1960s by the computer scientist Katalin Marton asserts that this isn’t a coincidence. She predicted that sets that produce small sumsets must also include long arithmetic progressions. Gowers, Green, and Tao had made headway on a refined version of this problem called the polynomial Freiman-Ruzsa conjecture in the early 2000s but eventually got stuck. Then, in 2023, Tao, Green, and Manners picked it up again with an eye toward introducing techniques from probability theory that Manners had developed.
They realized that by combining those techniques with Gowers’ earlier ideas, they might be able to solve the whole thing. They brought Gowers into the collaboration, and the quartet made steady progress through the summer of 2023. By late fall, they had it. On November 9 — just three days after Tao uploaded his first formal Lean proof to GitHub — they uploaded their proof to arxiv.org.
With Lean on his mind, Tao suggested to his three co-authors that they could try formalizing their paper. The work seemed like a good candidate for formalization both because it was an important result and because it relied on relatively simple techniques. They wouldn’t have to spend months adding prerequisite material to Mathlib — most of the necessary definitions were already there.
However, Green, Gowers, and Manners weren’t especially interested in taking the time to learn Lean. So Tao set off on his own — though he knew he likely wouldn’t be alone for long. Any project he led was likely to draw attention.
On November 13, Tao kicked off a new channel in a Lean-focused chat group. “Hi everyone. I am thinking of starting a project to formalize in Lean4 the recent proof of Timothy Gowers, Ben Green, Freddie Manners, and myself of the polynomial Freiman-Ruzsa (PFR) conjecture,” he wrote. He would use the channel to coordinate activity on the project and would be “happy to accept volunteers to contribute to this project in whatever capacity they feel able.” It was a reboot of the Polymath Project, only this time they were formalizing an existing result rather than trying to prove a new one — and all the work would be verified by Lean, meaning Tao wouldn’t have to check it himself.
Within a day, Yaël Dillies, a Ph.D. student at Stockholm University, had set up a rough blueprint for the project that divided the proof into 13 sections. Within each section, Tao identified the sequence of lemmas and definitions that needed to be formalized. In a typical math paper, lemmas — simpler results that help build toward the proof of a larger theorem — might be about 20 lines long, but for the PFR formalization, Tao broke the proof down into five-line lemmas. His goal was to make the proof as modular as possible, allowing many people to make small contributions.
For the first week, most of the activity on the thread was about formalizing basic concepts from probability theory that the proof required but were not yet in Mathlib. In particular, they had to formalize Shannon entropy — a measure of the uncertainty or disorder in a data source, like a set of numbers. But along with formalizing math, Tao and the others spent that first week figuring out how to work together. Initially, the conversation was free-form, with Tao posting about what he thought needed to be done and others chiming in with ideas about how to do it, much as the Polymath projects had unfolded in blog comments.
On November 22, Tao posted a list of 22 outstanding lemmas and wrote, “If you want to claim one or more of these lemmas, please do so by replying in this thread.” The replies flooded in: “I’d like to claim the entropy of a uniform random variable :),” wrote Paul Lezeau, a Ph.D. student at the London School of Geometry and Number Theory. “I’m gonna take a stab at the general fibring identity,” replied Aaron Anderson, a Ph.D. student at UCLA.
Drawn by word of mouth, more and more mathematicians joined the effort. By the end of November, Tao, like a harried volunteer coordinator, was writing little Lean code himself, instead focusing on finding tasks for others to do. On November 28, he wrote, “Given that we may temporarily have a surplus of volunteers for the PFR project as it nears completion, I thought of one additional small task that someone might be willing to work on.” Forty-six minutes later, Kim Morrison replied that they had completed the task. “Wow, that was quick! Thanks!” Tao answered.
Even before the formalization was complete, the Lean community began discussing what it meant. In particular, they debated whether the efficiency of the project signaled a new era of fast formalization, or whether it reflected the singular influence of Terry Tao. In a wrap-up post in the group thread, Tao reflected that he had not written much of the code himself. “This is actually quite encouraging to me, as it suggests to me that it will be possible for mathematicians to lead Lean formalization projects without requiring extensive Lean programming skills (though one may need at least enough expertise to be able to state lemmas, if not prove them).” Eight minutes later, Johan Commelin, a mathematician at Utrecht University and the director of the Mathlib initiative, replied, “I don’t want to immediately hijack this thread,” before going on to question whether the lessons Tao had learned during the project were broadly applicable. “Of course you got a lot of help with this project because of its high-profile nature,” he wrote.
Commelin also noted that while projects like PFR were fun and exciting to take part in, contributing to them was not the kind of thing young mathematicians were recognized for when they applied for academic jobs. “At the moment, it is still not clear how formalizers (for lack of a better job description) will be credited by the mathematical community, and how these activities will be valued on the job market.” Tao replied, “For what it’s worth, I’m more than happy to mention contributions to this project in letters of reference as appropriate.”
By 2024, Tao had become the most prominent public voice touting the potential of machine-assisted mathematics. He was three years into his tenure on President Joe Biden’s President’s Council of Advisors on Science and Technology and had become co-chair of a working group on generative AI. In a pair of high-profile speeches in 2024, he expressed his vision for a new kind of mathematical collaboration: one that combined human insight, the creativity of large language models, and the guarantees of correctness provided by formal verification systems.
He came to this view in part because he saw clear limits on what current AI tools could do. They excelled at solving straightforward problems or tasks with plenty of prior data, but at the frontier of mathematics — where there were few published results and little data to train on — AI faltered. In his early experiments with LLMs, he observed that they behaved like overconfident undergraduates, offering suggestions without the expertise to tell the difference between good and bad ideas.
Yet Tao had a way forward in mind. He didn’t think AI would replace human mathematicians anytime soon, but he did consider it particularly well suited to helping solve certain types of complex mathematical problems: ones that could be broken into thousands of small, manageable subproblems — essentially the same class of problems that worked well for Polymath projects. At that scale, mathematicians could employ AI to solve large swaths of the easiest subproblems, with its results outputted as formal proofs that Lean could check, and step in to handle the most difficult remaining questions themselves. In 2024, Tao was promoting this vision to anyone who would listen, and following the PFR project, he had realized that if he really believed in the work, he needed to step up and lead it himself. He also knew right away which problem he would start with.
It was a question that he had stumbled upon a year earlier. In July 2023, a user on MathOverflow posed a seemingly simple puzzle. Consider an operation like addition, the user wrote. It might follow certain fundamental algebraic laws like the commutative law, which says x + y = y + x, or the associative law, which states that (x + y) + z = x + (y + z). In many cases, there’s no relationship between one law and another — the commutative law doesn’t imply the associative law, for example.
The MathOverflow question concerned the relationship between two particular laws, and another user answered it quickly.
But the question of how laws relate to each other in general caught Tao’s curiosity. Rather than solving puzzles one by one, Tao began sketching out a rough diagram that showed how different possible algebraic laws relate to one another. It became clear the picture might be quite complicated.
He saw that if he restricted his study to algebraic laws involving operations applied exactly four times, there were about 4,694 laws he had to account for. Each law could potentially imply or fail to imply any other law, creating 22 million logical implications to check. Once he had checked them all — either by proving they held or by finding a counterexample in which they failed — he would have a complete picture of how all 4,694 of those laws relate to each other. It felt like exactly the right scale for the new style of mathematics he was proposing.
Tao called his new endeavor “Equational Theories” and announced its formation in a post on his personal blog on September 25, 2024. He opened by ticking through the main reasons large-scale public math collaborations had been hard in the past and then wrote, “Proof assistant languages, such as Lean, provide a potential way to overcome these obstacles.”
To start, Tao and the growing number of volunteers who joined him tested the more than 4,000 laws against simple mathematical structures known as magmas. Magmas are stripped-down versions of arithmetic that made for a useful starting point because any law that failed to hold for magmas couldn’t possibly imply other, more complex laws. The participants quickly tested millions of these simplified systems using basic Python scripts and within days had resolved more than 99% of the 22 million potential implications. Tao posted on day 2 — September 27 — that he was astonished at how rapidly the project was advancing: “This project has moved far, far quicker, and scaled up much much faster, than I had expected — only 48 hours in and already a large fraction of the implications are likely to be resolved soon! I thought the 3-week PFR project was fast, but this is an insane additional level of speed.”
Once the simplest implications were resolved, the Equational Theories volunteers moved in a decentralized way to automated theorem provers that could search for solutions to problems all on their own, without interactive help. These provers, along with old-fashioned human ingenuity, knocked down the open questions one at a time.
Like a scientist watching his own creation come to life, Tao admired the work as it unfolded. “The project seems to be successfully decentralizing; in particular, there is now a lot of activity going on now that I am not fully aware of,” he wrote.
To many mathematicians, Tao’s project was intriguing but odd. Buzzard followed along, fascinated by the social experiment though bored by the mathematical content of Equational Theories. He thought it was both elementary and weird, though he admired Tao’s inventiveness. John Baez, another prominent mathematician, was more blunt. He remarked, “This seems like a colossal waste of time to me,” before acknowledging that he felt the same way about college football, and plenty of people liked that, too.
Within a month, the Equational Theories group had narrowed 22 million questions down to 238. By late November, they were down to 138. As they chipped away at the remaining cases, progress slowed. When the new year began, about 30 implications were left unresolved, and the rate of progress slowed even further. By the end of March, they had been stuck for several weeks on just four. Contributors tried their hand at the remainder, but with so few implications left, many people drifted away; Tao’s updates slackened from their near-daily cadence to once every few weeks.
But settling every single one of the 22 million implications had never really been the goal of Equational Theories. Out of sheer curiosity Tao had wanted a map of the complete landscape, and now he had that, minus a few details. More importantly, he viewed Equational Theories as a pilot project for a fundamentally new way of doing mathematics — and in that regard it was an unqualified success.
Equational Theories, in Tao’s view, was the opening act of what he hoped would become a new era of “experimental” mathematics. He had in mind the kind of transformation that had already come to fields like physics. Physics had once been a largely theoretical discipline where solitary thinkers or small groups of collaborators tackled one or two problems at a time — in other words, it used to look a lot like math still did. But with technological advancements came a new, experimental branch of the field — massive collaborations at laboratories like CERN’s Large Hadron Collider, where hundreds or even thousands of researchers with specialized skills worked together and generated huge volumes of data. These experiments didn’t replace theory but complemented it, with new results washing between the two modes of investigation.
Tao imagined a similar evolution happening in mathematics. He trusted that novel forms of inquiry would inevitably lead to novel insights, as they always had before. As the Equational Theories team methodically crossed implications off their immense table, they stumbled onto genuinely new mathematical constructions — like “magma cohomology,” an alien extension of the concept of group cohomology, a deep and well-studied field describing when groups can or cannot be enlarged in certain ways. Tao reached out to John Baez — the Equational Theories naysayer and an expert in cohomology — to ask if this construction had been seen before. Baez admitted he had never encountered it.
To Tao, that was exactly the point. The project had shown that mathematics could be conducted differently, experimentally — and in doing so, it had turned up something genuinely new. Tao had never expected Equational Theories to unearth a revelation; he wanted it to demonstrate the efficacy of a new kind of mathematical machine. And in that sense it worked. Terry Tao had found a new way of doing mathematics, and he showed no signs of going back.
Excerpted from The Proof in the Code: How a Truth Machine Is Transforming Math and AI by Kevin Hartnett. Copyright © 2026 by Kevin Hartnett. To be published on June 9, 2026, by Quanta Books in partnership with Farrar, Straus and Giroux. All rights reserved.
