Terence Tao's prediction from 12 years ago has now been fulfilled with the help of AI
Facts have proven that Fields Medalists sometimes double as prophets.
Twelve years ago, a prediction made by Terence Tao on the stage of the first Breakthrough Prize in Mathematics was regarded as a wild fantasy:
One day in the future, we may no longer write papers using LaTeX, but instead use a formal language that computers can understand.
That year, the Transformer hadn't been invented yet, and ChatGPT didn't even exist.
Unexpectedly, the boomerang hit the target. In the past year, AI has suddenly started to speed up crazily in the field of mathematics.
From OpenAI solving open problems to DeepMind cracking mathematical conjectures in batches, more and more mathematical proofs are being written into formal systems and handed over to computers for automatic verification.
Looking back, the first person to see the trend clearly and get involved in practice himself was Terence Tao.
In the past decade, he has successively promoted large - scale collaborative mathematics, Lean formal proofs, and launched the Equational Theories project. Facing 22 million mathematical problems, relying on "AI + human collaboration", more than half of them were solved in just 48 hours.
With the help of AI, the project's efficiency reached its peak, and often he didn't even need to get involved.
In fact, Terence Tao is also using practical actions to prove that the best way to predict the future is to create it with your own hands.
A child prodigy, but more infatuated with collaboration
When it comes to Terence Tao, many people's first reaction is his legendary experience:
He taught older kids to count at the age of 2, started learning calculus at 7, became the youngest bronze medalist in the history of the International Mathematical Olympiad at 10, became one of the youngest tenured professors in the history of UCLA at 24, and won the Fields Medal at 31.
△ 72 - year - old Paul Erdős and 10 - year - old Terence Tao. Image source: Quantamagazine
In the public's impression, people like him are often "genius lone wolves".
But Terence Tao himself is the opposite.
Compared with working alone, he has always been more interested in another thing:
Can mathematicians collaborate like open - source software developers?
If one person knows A and another person knows B, will new things that neither of them could think of alone emerge if their knowledge is combined?
This idea later had a profound impact on his entire career.
In 2009, he participated in the Polymath project, an experiment that brought mathematical collaboration to a public forum.
In this project, anyone could log in, take on sub - problems, submit ideas, and work together.
Problems that originally required a few experts to spend months or even years to complete were quickly advanced under the open - collaboration model.
This experiment finally successfully solved a combinatorial mathematics problem, proving that large - scale collaboration in mathematics is not a fantasy.
The Polymath project was successful, but Terence Tao soon discovered a bigger problem:
All error checks were placed on the core person in charge.
The more participants there were, the greater the review pressure; the larger the scale of collaboration, the higher the organizational cost.
Without an automatic verification tool, the speed of manual error correction could never keep up with the scale of collaboration. The upper limit of collaborative mathematics was held down.
To break through this ceiling, another way had to be found.
In 2014, on the stage of the first Breakthrough Prize, he described his vision of future mathematics, which were three predictions that sounded rather unreliable at that time:
Large - scale mathematical collaboration involving hundreds of people would become the norm;
Computers would be able to automatically verify mathematical proofs;
LaTeX would be replaced by a formal language that machines could read.
Looking at it today, these three judgments almost correspond to all the main lines of the development of AI in mathematics.
But at that time, they sounded too far - ahead.
Although the Polymath project proved that collaborative mathematics was feasible, without automating the "verification" process, it would be difficult for mathematical research to truly achieve large - scale collaboration.
And the answer he was waiting for finally appeared in a tool called Lean.
After ten years of making predictions, he decided to give it a try himself
The turning point came in 2023.
That year, Terence Tao met mathematician Kevin Buzzard in an exchange. Buzzard was also an early promoter of Lean.
Lean is an interactive theorem - proving system that describes mathematical proofs in a formal language, allowing computers to verify the logic of each step line by line.
This concept exactly hit the problem that Terence Tao had been thinking about for years. So, encouraged by Buzzard, 48 - year - old Terence Tao decided to get involved in practice himself.
On October 9, 2023, he posted a status on social media:
I've finally decided to start learning the Lean4 interactive proof system (using AI assistance if necessary).
The Fields Medalist originally thought it wouldn't be too difficult, so he picked a problem about the Maclaurin's inequality as a practice project, intending to use it as material to try to formalize the proof with Lean.
He first completed a 10 - page handwritten - style proof in the traditional way, and then began to translate it into Lean code. According to his estimate, it would take about a week to finish.
Then, he hit a wall.
After getting started, he found that formalized proof and writing a mathematical paper are two completely different thinking modes.
In a traditional paper, a statement like "the sum of three numbers greater than 1 is greater than or equal to 3" would hardly attract anyone's attention, but Lean doesn't work that way:
You must clearly tell the system where the conclusion you're referring to comes from and which lemma it corresponds to.
Many seemingly obvious steps require a large number of formalized details to be filled in. A few lines of paper - based derivation can easily turn into hundreds of lines of code.
A month later, Terence Tao finally completed his first formalized proof.
Although the code wasn't elegant, from that day on, he truly became a member of the formalized mathematics community.
The PFR project: the first realization of the prediction
Not long after he started learning Lean, a new opportunity emerged.
On November 9, 2023, Terence Tao and his collaborators Ben Green, Tim Gowers and others completed a paper on the PFR conjecture.
This is a number - theoretic proposition about the additive structure of sets, which had been unsolved for many years.
After the paper was written, he didn't stop. Then, he posted a message in the Lean community:
Hello everyone, I'm going to launch a project to formalize the latest proof of the PFR conjecture in Lean4... Everyone is welcome to participate.
The biggest difference from the Polymath project this time is that Lean is in charge of the review.
This time, he divided the paper into independent sub - tasks and opened them up to the global community.
Everyone completed their own part, and the system automatically verified it. Only after passing could it be merged into the main line.
As a result, all the formalization work was completed in just three weeks.
Even, Terence Tao posted an additional small task, and a community member completed and submitted it in less than an hour.
This was also the first time he saw the collaborative mathematics model he had envisioned more than a decade ago actually work.
Determine most of the 22 million mathematical relationships in 48 hours
After tasting the sweet fruit, he placed a bigger bet.
On September 25, 2024, Terence Tao launched the Equational Theories project, aiming to systematically determine the logical implications between about 22 million algebraic equations.
Simply put, it's about figuring out which equations can be derived from which other equations.
This time, Terence Tao used a new combination: AI helps write proofs, Lean is in charge of checking for errors, and the global volunteer community tackles specific problems separately. The three parties work together to advance the work.
The workflow of the automated proof assistant. Image source: Quantamagazine
This time, the results came out even faster! Within 48 hours, the large - scale screening was basically completed, and a large number of problems were on the verge of being solved.
In the first 9 days, the overall progress had reached 99.866%. On the 57th day, the main project was declared basically completed, with only 162 implication relationships waiting to be finalized.
Even, this project gave birth to a brand - new mathematical concept magma cohomology during the process.
This concept is a cohomology theory tailored for magmas without axiomatic constraints. Its core is to define the cohomology groups H¹ and H² that depend on equations, which are used to classify magma extensions, construct counter - examples, and distinguish different magmas. It is a generalization of the classical group cohomology and is used to study the most general algebraic structures.
In addition, the self - operating ability demonstrated by the Equational Theories project also delighted Terence Tao.
Relying on AI assistance and automated verification, even if he didn't follow the whole process, all the work could still progress steadily.
In the past two years, Terence Tao has increasingly incorporated AI into his research process and has constantly advised young scholars to master the ability to collaborate with AI.
What we can see from Terence Tao is that the best prophets are actually the pioneers -
They don't just predict the future, but also put it into practice and turn their once - envisioned ideas into reality step by step.
Now, this pioneer has also become the most staunch evangelist for AI in mathematics.
Reference links:
[1]https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/
[2]https://terrytao.wordpress.com/2023/11/
[3]https://gowers.wordpress.com/2009/03/10/
This article is from the WeChat official account “QbitAI”, author: Wen Le. It is published by 36Kr with authorization.