How Terry Tao Became an Evangelist for AI in Math | Quanta Magazine

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.”

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.