A top mathematician quit the field in tears: The doctoral-level problem he had spent years working on was solved by AI in just a few weeks.
A top-tier mathematics scholar, with the help of AI, has consecutively solved his PhD research topics that he had struggled with for years within just a few months.
This is undoubtedly a good thing.
However, he surprisingly announced his withdrawal from the academic circle!
This man, named Rishikesh Gajjala, has just completed his postdoctoral research at New York University Abu Dhabi.
Just yesterday, he posted a message on X that sent shockwaves across the entire mathematics community: I have decided to leave the academic world of mathematics.
Over the past few months, AI has helped him make successive breakthroughs on the problems he cared most about and had spent years studying during his PhD.
Under the original pace, these difficult problems would have taken him several more years to solve. For most people, this achievement would have made them more convinced that mathematics is their destined career.
Yet the opposite happened. Every passing week made him feel more and more like a redundant person in this field.
Gajjala said that the meaning of mathematics to him never lies in the answers themselves. It lies in the months or even years of exploration before arriving at the answer, the countless dead ends, the long hours of arduous work, until the hidden structure finally emerges. That struggle is what makes the results truly his own.
Now he believes that we are rapidly approaching a world where most of the answers in the Book of God are just a single prompt away.
After realizing this, he suddenly found no point in spending most of his life trying to find those answers a little earlier than others.
A beautiful proof is no different from garbage before verification
But a question kept haunting him.
How do you know this oracle is correct?
As artificial intelligence becomes more capable and cheaper by the day, mathematical papers are flooding out, but there is a severe lack of verification.
The proofs generated by these AI systems can be extremely sophisticated, and their errors can also be hidden very deeply.
It sometimes takes him several days to determine whether a seemingly brilliant breakthrough is valid or not.
Gajjala put forward a bold statement: Before being verified, a beautiful proof is no different from garbage.
This remark sounds harsh, but he is not the only one who thinks so.
Terrence Tao, one of the greatest mathematicians of our time, delivered a speech titled "Mathematics in the Age of AI" at the 2026 International Congress of Mathematicians (ICM), which talked about almost the exact same issue.
He coined the term "proof indigestion" — the speed at which AI generates proofs has far outpaced the speed at which humans can review them, and mathematics is rushing from an era of scarce proofs to an era of excess proofs.
He specifically mentioned that websites dedicated to collecting difficult mathematical problems are already flooded with AI-generated proof submissions. Many of them are likely correct, but no human mathematician has the time to verify them one by one.
To put it bluntly, AI writes papers at the speed of light, while humans read papers at the speed of a snail. When papers flood in, "correct answers" that no one has read are no different from non-existent ones.
Intelligence is becoming the cheapest commodity, but verifiable and trustworthy intelligence remains the most valuable.
From finding answers to building verification systems
After realizing this, Gajjala made a decision: he would no longer pursue answers, but build systems that can certify the correctness of those answers.
He switched to the field of formal verification, using Lean (a theorem proving assistant language) to formalize long-standing conjectures and Erdős problems discovered with the help of large language models one by one.
He then joined PramaanaLabs, which had just closed a $27 million seed round led by Khosla Ventures, shifting his research focus from "discovering mathematical truths" to "building certification systems that can prove the correctness of AI-generated answers."
Someone asked Gajjala in the comment section: Won't AI soon be able to build the verification systems themselves at superhuman speed too?
He replied: I don't believe that yet. If one day I do think that's the case, I'll go find a new job.
Formal verification means rewriting proofs into a machine-readable language, so that computers can check them line by line.
Humans may overlook details, get tired, or be distracted by elegant writing. But when machines verify proofs line by line, they have no emotions and will not be impressed by the author's writing style.
Meanwhile, the most remarkable achievement in this field to date has been released.
The 246 Theorem: The closest humanity has ever gotten to the twin prime conjecture
Axiom Math used its multi-agent system AxiomProver to complete the first automatic formal verification of the proof of the "246 Theorem".
Founding mathematician Ken Ono said, This theorem represents the absolute boundary of humanity's current knowledge about prime numbers.
What does 246 mean here?
2, 3, 5, 7, 11, 13... Prime numbers become sparser as you go further along the number line, but some are very close to each other, such as 3 and 5, 11 and 13, which differ by 2. These pairs of prime numbers are called twin primes.
In the 19th century, French mathematician Alphonse de Polignac put forward a conjecture: No matter how far you go along the number line, such pairs will always pop up again. That is, there are infinitely many pairs of twin primes.
Even elementary school students can understand this conjecture, but no one has been able to prove it to this day.
In 2013, Yitang Zhang made a breakthrough. He proved that there are infinitely many pairs of primes with a difference of no more than 70 million. 70 million is still far from the target of 2, but this is the first time in human history that it has been proven that this gap is finite, which shocked the entire mathematics community.
A few months later, James Maynard from the University of Oxford adopted a new method and cut the 70 million gap down to 600. This work contributed greatly to him winning the Fields Medal, the Nobel Prize of mathematics, in 2022.
After that, Maynard and Terrence Tao collaborated on the Polymath8b project, and further reduced the gap to 246.
It took ten years to go from 70 million to 600 and then to 246. 246 is the closest humanity has ever gotten to the target of 2.
What AxiomProver verified as correct this time is exactly this theorem — there are infinitely many pairs of prime numbers with a difference of 246.
More importantly, the team did not stop at demonstrating their technical capabilities. They packaged a batch of prime number gap results into a reusable open-source library, with the 246 Theorem as its flagship. This means that other AI systems that conduct research on prime number problems in the future can directly call this set of machine-verified infrastructure.
The world is about to run on code that no one has ever read
A mathematics scholar withdrawing from the academic circle may seem like nothing more than an individual's career choice.
But the underlying logic of this story is completely different.
The world is about to run on computer code that no human being has ever read.
In his ICM speech, Terrence Tao also put forward a striking judgment: he was relatively confident in predicting the trends of the next three years back in 2023, but that sense of certainty has now vanished.
"I am not sure that anyone can reliably predict what will happen even a year from now."
Gajjala left the academic world of mathematics, but he did not abandon mathematics. He just changed from a person who pursues mathematical truths to a person who certifies these truths.
In an era where AI is accelerating the rewriting of everything, this may be the most urgently needed role of all.
This article is from the WeChat official account "AI Insights", author: ASI Revelation, published with authorization from 36Kr.