What is Terence Tao "afraid" of?
When AI starts mass-producing mathematical proofs, how can humans be certain that these proofs are reliable?
On October 9 local time in the United States, Terence Tao, the renowned mathematician and Fields Medal winner, reposted a column article by Thomas Hales on his blog titled "The Lean Theorem Prover for Mathematicians: Reliability and Artificial Intelligence Issues".
Screenshot of the reposted article on Terence Tao's blog
The contradiction of this AI mathematics wave lies in: AI is cracking mathematical problems at an unprecedented speed, and these problems used to require mathematicians to spend years or even decades to complete their proofs.
A typical case is that OpenAI released 722 mathematical manuscripts generated by its internal model at one time on GitHub on October 6, covering 372 result series and about 4000 test problems.
"All the people around me who work on mathematics have switched to recreational mathematics recently," a cutting-edge model researcher joked, "Everyone thinks that doing traditional mathematics is no longer meaningful because they cannot compete with AI. It is better to do some recreational mathematics for fun and teach children."
The researcher added that mathematical research, especially non-applied mathematical research, usually follows a cycle of solving a specific difficult problem, applying for funding to carry out research, applying for new funding after getting phased results, and then pushing forward the research. But now AI has solved these "difficult problems" in batches.
"These 'mathematicians' have lost the 'difficult problems' that they were halfway through researching. They cannot even finish their research projects, let alone apply for subsequent funding," said the researcher.
However, the fact that "difficult problems" are broken through one by one by AI does not mean that Terence Tao will switch to recreational mathematics. Instead, his attitude has changed: he co-signed the declaration "The Serious Misalignment of Artificial Intelligence in Mathematics" initiated by 25 Fields Medal winners, and the "Human Mathematics Association" led by him released a statement calling for stopping cooperation with OpenAI.
"He is also wavering. Terence Tao used to strongly support using AI to do mathematical (research)," said the aforementioned researcher.
01
Problem Solving Is No Longer a Scarce Resource
Terence Tao's change is no accident.
As a Fields Medal winner and professor at the University of California, Los Angeles (UCLA), Terence Tao used to be an active advocate of combining AI with mathematical formalization. However, as the output speed of AI completely surpasses human beings, the focus of the issue has quickly shifted from "whether AI can solve problems" to "how we should treat these massive outputs of conclusions".
Around the time when OpenAI released these manuscripts, Terence Tao posted a series of posts on Mathstodon, putting forward the concepts of "Math 1.0" and "Math 2.0".
He pointed out that traditional mathematics (Math 1.0) attaches great importance to "who solves an open problem first", even if the initial proof is extremely difficult to understand.
However, when this goal is excessively pursued to an unsustainable level, the mathematics community needs to adjust the evaluation criteria, and pay more attention to explanation, community building and opening up new research directions (Math 2.0), instead of blindly pursuing the speed of problem-solving.
In other words, if AI only throws out results that are not carefully considered in batches, and humans no longer read and understand these proofs, and even cannot confirm their authenticity, the value of mathematics will be completely disintegrated.
His vigilance further focuses on a more underlying problem: if humans no longer review the massive proofs generated by AI in person, but rely entirely on computer programs for verification, is this "ultimate referee" itself absolutely infallible?
02
The "Ultimate Referee" Lean and Soundness Bugs
This has to mention the core role Lean in this wave of machine verification.
Lean is a formal language and "interactive theorem prover" initiated by computer scientist Leonardo de Moura during his work at Microsoft Research, which is now widely used in the mathematics community.
In simple terms, if the AI-generated mathematical papers are regarded as human-readable "natural language", Lean is equivalent to an extremely strict "logical compiler" or "computer referee": it requires translating mathematical language into precise code that can be strictly recognized by computers (that is, "formalized code"), and then the core algorithm of Lean checks line by line whether the derivation logic is flawless.
In the past, as long as it passed the verification of Lean, the mathematics community usually believed that this proof had extremely high logical credibility. However, this trust is being severely damaged. Not only the formalized code attached to the batch of OpenAI manuscripts often has disconnections between assumptions and steps when compared with natural language derivations, the more troublesome thing is that the verification tool itself is not inviolable.
In the summer of 2026, Lean exposed multiple soundness bugs one after another, a stage known in the circle as "the summer of Lean soundness bugs".
The most notable one happened in July: with the assistance of AI, someone released a Lean formalized proof that claimed to "disprove the Collatz conjecture". This proof was accepted by both the Lean kernel and the independent checker, but a few days later, people found that it used an implementation defect of the kernel when processing nested inductive types, making the system mistakenly accept contradictory propositions. Handing over proofs to computers does not mean absolute safety.
Similar reliability concerns — withdrawals due to symbolic errors — also happened to OpenAI.
One day after the 722 model-generated mathematical manuscripts mentioned above were released, 3 of them were withdrawn by OpenAI.
The aforementioned researcher emphasized that OpenAI is actually a little irresponsible, "Some proofs are problematic, and after they are released, a large number of mathematicians still have to verify them."
In the view of this researcher, to prove a theorem A, it is necessary to formalize theorem A and then formalize the proof of theorem A. Generally speaking, if the second step is done with Lean and the verification is completed, then the second step must be correct. But it is possible that the first step is wrong, which means that they correctly proved a wrong theorem.
"Cooperate with a group of mathematicians and let them help verify," the aforementioned researcher believes that this is the responsible behavior that OpenAI should take, but this situation brings another paradox — mathematicians are "ending" the work of mathematicians themselves.
03
The Unlost Reason and Unstoppable Pace
The renowned mathematician Hales wrote the article "The Lean Theorem Prover for Mathematicians: Reliability and Artificial Intelligence Issues". He does not deny the great potential of AI to automatically generate and formalize proofs, but what he really worries about is: when AI generates formal proofs on a large scale, and even deeply participates in checking and repairing the verification tools themselves, whether the mathematics community still has a solid enough foundation to judge whether the entire verification chain is credible.
The article raises a more sharp question: since AI has participated in the vulnerability scanning of the Lean kernel, how can we prove that it has not left hidden defects or even backdoors during the scanning or repair process?
What Terence Tao and Hales are really wary of is not that AI proves theorems faster than humans, but that mathematics is gradually losing its core value of "having reliable reasons to believe that the answer is true".
Mathematics not only needs to generate results faster, but also requires someone to explain, understand and be responsible for these results, which is one of the reasons for the "proof indigestion" proposed by Terence Tao.
In the view of the aforementioned researcher, the problem of "proof indigestion brought about by the AI explosion" is not limited to the field of mathematics in the AI era, and many academic fields are facing the same problem. "The number of ICLR submissions has soared to 60,000 this year."
A number of practitioners with mathematical backgrounds all said they can understand Terence Tao's concerns, but they also believe that the AI wave and torrent cannot be stopped.
"Mathematics is the cornerstone of modern civilization. Some practices of institutions such as OpenAI will cause a fault in this field. However, the call to stop cooperation with OpenAI makes no sense, and the impact of AI on all aspects cannot be blocked," a chip entrepreneur with a mathematical background told Tencent Tech.
On the other hand, the capabilities of the model are constantly evolving, and AI is unstoppable, but this does not mean that scientific research and the physical world will explode in a short period of time.
"A more powerful model will not automatically turn into better delivery, nor will it make the physical world iterate at the same speed," Feng Yao, the managing partner of SevenX, wrote in the North American AI interview notes a few days ago.
The aforementioned researcher took the mathematical manuscripts previously released by OpenAI as an example, "It seems that more than 700 articles and more than 300 domain achievements have been released, but it is very likely that the promotion of society will not be as great as imagined in the end. It seems that scientific research achievements are exploding, but in the short term, it will not greatly promote the overall technology of society."
It can be said that human beings are overly anxious about the "false prosperity" and "exaggerated substitution" brought by AI.
"I prefer people-oriented scientific research rather than achievement-oriented scientific research," the researcher added. "I believe that social progress is driven by people, and the goal of scientific research is also to cultivate people, so that people can drive the development and progress of society. Scientific research achievements are only means, and people are the ends."
Back to the concerns of mathematicians such as Terence Tao, as the proofs generated by AI increasingly rely on machine verification, what really needs to be vigilant is not the speed brought by computing power, but whether human beings still retain the ability to independently judge whether a proof is credible and understand why a proof holds when enjoying this speed.
This is a new topic that we have to face.
This article is from the WeChat official account "Tencent Tech", author: Worth Paying Attention To, 36Kr releases it with authorization.