“The product of mathematics is clarity and understanding, not just the theorems themselves.”
Alexander Grothendieck's handwritten diagram
One of my most brilliant theorems, I have never formally written down. The idea took shape one bright morning in Lausanne, Switzerland, when I was preparing my last invited conference presentation. The proof of this theorem seemed so obvious and the conclusion so convincing that I had the temerity to change the slides at the last minute. Time is already very tight, so I can only write this result as an informal note at the bottom of the last slide, rather than writing it as a formal and complete theorem¹.
By then I had left academia and founded a machine learning startup. I knew I would be too busy to put together a clean proof and publish it officially. This became my excuse for perfunctory work. I just wrote that note and threw the slide deck away like a bottle into the ocean.
I once hoped that some talented young mathematician would discover it in the future, formalize this result, and incorporate it into a larger theoretical framework. If you are lucky, due to various accidents of academic affiliation, it may also be called "Bessis' cell decomposition theorem" by future generations.
But this idea is really naive. Once I announced this result to the outside world, the motivation for others to write and write it down disappeared.
If I were to choose my second most satisfying result, it would be Theorem 0.5 under Garside categories in my old preprint. I had high hopes for this article, but I ultimately did not submit it to any journal. The entire creative process exhausted my energy, and I had already left frontline research before I could muster up the courage to polish the preparatory parts.
The second most outstanding result, this theorem is surprisingly simple to prove. As long as the preparatory work is properly handled, only a few pages of very conventional group theory derivation can be completed.
As for those preparations, the difficulty is even lower. You only need to study a dozen classic papers on Garside theory in the unpopular subfield and replace the original axiom system with a set of slightly general axioms. As long as you know what the goal is to do, you will almost never encounter substantial obstacles. It is essentially a large-scale conceptual level search and replace editing. But you'll have to take my word for it here; I just don't want to write the hundreds of pages of necessary detail.
If you think that the core job of a mathematician is to prove theorems, then this example can refute this idea. From the moment I conceived Theorem 0.5, I knew it was true and the proof process would be logical.
So what is the real difficulty? Is it to guess a precise proposition and write it down? Not really. In this case, this step is also not difficult.
The real difficulty is to intuitively realize that there should be "something like Theorem 0.5" and to build a conceptual framework so that this proposition can be expressed concisely. Once the definition is set, the rest will follow naturally.
It’s not always like this in mathematical research, but you do have those light-bulb moments: like stepping on your skis and speeding down the hill in the blink of an eye.
Jean-Pierre Serre has a widely circulated saying: When he wrote his seminal paper on coacervates, he hardly needed to think hard; everything fell into place, as if the typewriter had outputted hundreds of pages on its own, as if the article had already existed.
But I'm not Jean-Pierre Serre, and he won't lend me his typewriter. This is why my brightest mathematical ideas never got published.
Will I feel bad about this? Not really. My preprint is still publicly listed on arXiv and has been cited by dozens of documents, including many high-level papers. The real innovation is not Theorem 0.5 itself, but the language system that supports it, especially Definition 2.4 and Definition 9.3. This conceptual language was later written into a more than 700-page monograph on Garside's theory, which filled in a large amount of missing preliminary content.
To be honest, I have some selfish reasons for shelving this most innovative preprint. In this way, I can devote my energy to another more tedious preprint work: using Definition 9.3 as a key tool to solve the classic conjecture in my field-the 𝐾(π,1) conjecture of the finite complex reflection group. This incident greatly enhanced my academic reputation as a mathematician.
But to be honest, the David who solved the 𝐾(π,1) conjecture is just a social symbol derived from the better David who created Definition 2.4 and Definition 9.3.
Break the unwritten code of honor
In the past few months, faced with the rapid changes in the intersection of AI and mathematics, I have been troubled far beyond my expectation.
On a theoretical level, I should have felt confident and delighted. But in reality, I am full of doubts, worries and sadness at the same time. The part of me that is delighted is really excited to see a change taking place; the part of me that is confident believes that I have foreseen all this from a scientific and epistemological level; the part of me that is confused is stunned by the rapidity of the change and the enthusiasm that comes with it; the part of me that is disappointed misses the work style and value system that I once devoted myself to, but now may be about to disappear.
And the worried part of yourself brings all the feelings together. I had always known that there were many misconceptions about mathematics among the general public, but I never expected that this misunderstanding would evolve into an existential threat to the entire discipline.
In my book Mathematics: The Hidden World of Intuition and Curiosity, I describe this misunderstanding as a contradiction between two sets of mathematical ideas: official mathematics and hidden mathematics.
Official mathematics is expressed as a formal deduction system: starting from the axioms, theorems are mechanically derived. This is an ideal country in the eyes of geeks, where truth is either true or false, reasoning is either valid or invalid, and there is no room for theoretical nonsense.
The hidden mathematics belongs to the human side: why the official mathematics system was born, how humans interact with it, what impact it has on our brains, and what unique mental techniques mathematicians rely on to continuously expand the boundaries of mathematics.
Hidden mathematics never makes it onto the syllabus because it does not have the defining qualities of official mathematics and appears to be of secondary importance. Official mathematics is cold, rigorous, logically complete, and objective, and is passed down as the language of the universe. In contrast, Secret Mathematics is soft, vague, subjective, and seems like little more than cheap pedagogical backstory.
It’s no wonder that professional mathematicians have a fragmented understanding of their work.
“Rule number one of the Intuition Club: No talking about the Intuition Club.
Rule No. 2: If you insist on talking about intuition, do so in a downplayed way, as if it were just ancillary. After all, we are not a psychology department.
The third rule: definitions are worthless, and impression points will be deducted for explanatory work. The best positions are always reserved for those who prove the most difficult theorems. "
If you think I'm exaggerating, consider what G. H. Hardy wrote in his famous but unpleasant book "A Mathematician's Apology":
"There is no contempt more profound than the contempt of the creator for the interpreter, and generally more justified. Interpretation, criticism, appreciation, these are only things done by second-rate minds."
This is the ultimate expression of a divided mentality. Behind closed doors, mathematicians would complain about Hardy's "curse." They will emphasize the value of teaching, even if it is just for their own understanding of knowledge itself; they lament the system's pathological obsession with the priority of theorem proof, but everyone knows that a lot of the really hard work happens outside of proof, in the process of trying to understand the results. However, in public, everyone is still bound by the mathematician's code of honor: prove theorems and talk less!
But there is one exception: after you get the Fields Medal, you can speak freely.
Bill Thurston, the 1982 Fields Medal winner, is a man with a very rebellious spirit. Two years before his death, an undergraduate student who lacked confidence asked a question on MathOverflow, and Thurston participated in a wonderful discussion.
Undergraduate question: What contribution can someone like me make to mathematics?
In my opinion, mathematics was created by people like Gauss and Euler. Even if I could read and understand their work, nothing new would be created. I could rewrite their work into modern language notation, or guide others to learn it, but I never thought that was the most important part of a mathematician's job—that what really mattered was creating new mathematics. In reality, with countless smart people working hard, is there no room left for ordinary people like me? Could it be that my value can only be used as cannon fodder? A large number of people come forward one after another, and some difficulties can always be overcome.
Thurston responded:
What you need to contribute to is not just mathematics itself. The significance of this matter is even more profound: by engaging in mathematics, how can you give back to mankind, and furthermore, how can you benefit the world? This question cannot be answered purely intellectually, and the consequences of our actions are far beyond our comprehension. Humans are deeply social, deeply instinct-driven creatures, and our happiness depends on many things that are difficult to explain rationally. So following your heart and passion is the right choice. Pure reason can lead you astray². None of us are smart and wise enough to see everything through just thinking.
The product of mathematics is clarity and understanding, not just the theorems themselves. For example, even if there are such famous results as Fermat's last theorem and Poincaré's conjecture, what is their real significance? Their value does not lie in the propositions themselves, but in the challenges they pose to human understanding; these challenges have led to mathematical developments and improved our understanding...
Mathematics can only survive in a living community of mathematicians: a community that spreads understanding and gives life to old and new ideas. The real satisfaction of doing mathematics comes from learning from and sharing with each other. All of us can have a thorough understanding of a few things and remain vague about many more. There’s never a shortage of ideas to clarify…
Here we need to briefly ponder metaphysics, because it is easy to dismiss Thurston's remarks as chicken soup or trendy rhetoric.
In my first Substack blog post, I half-jokingly wrote that we had misunderstood mathematics for 2,300 years, stuck in a false binary between formalism (“mathematics is a game of meaningless formal symbols”) and platonism (“mathematics captures the properties of real entities in the world of ideas”).
The conceptual interpretation I propose is a restatement of Thurston's point: mathematics does play this meaningless game of formal symbols, but we play this game because we project meaning onto the symbols.
Meaning is a cognitive phenomenon, a product of our neural architecture, not a direct encounter with transcendent reality.
When we "do math," we manipulate formal expressions and slowly build up an intuition for what the symbols represent, as if the symbols pointed to real objects in Plato's world of ideas. Platonists treat this side effect of neuroplasticity as a fact in itself; formalists treat it as an inconsequential appendage. Conceptualists like me believe that mathematics is a vital cognitive infrastructure for humans.
A natural question is why the conceptual perspective took so long to emerge. Part of the reason is that it conflicts with the prevailing spiritualist worldview, which rejects a physical interpretation of mathematics.
It also goes against the mathematician's code of honor. Hardy's curse is so powerful that even Thurston has trouble completely breaking free. When numerous MathOverflow users thanked him for his insights, he replied:
"Thank you all for your messages. I try to write down how I feel. At this age, I no longer fear how others will judge me, so it is much easier to speak out. If what I think and think has value to others, that will make me happy."
But why has this extremely negative code of honor persisted for so long?
The answer is simple: for the academic world, this set of rules once worked. As the postscript of my book says:
"This system has its own advantages. It reduces subjective arbitrariness and makes mathematicians wary of complacency and nepotism. When the subject studies eternal truths, this set of principles provides a concise set of professional evaluation standards."
This honor code also provides guidance for researchers in evaluating new ideas and directions. Peter Scholze, the 2018 Fields Medal winner, said that concept construction and problem solving, the two sides of mathematics, are in a symbiotic relationship³:
"What I value most is definition. Human beings rely on language to describe mathematics, and they always need precise vocabulary to express ideas clearly... Unfortunately, you can't find a suitable definition just by contemplating it; if you want to find those problems, you can only make progress by isolating new key concepts."
This is how the discipline has operated for thousands of years: mathematicians create value by introducing new concepts, but the reality is that only theorems can be exchanged for bread. This model worked in the past because two things almost always went together. The David who solved the 𝐾(π,1) conjecture and gained fame was precisely the David who created Definition 2.4 and Definition 9.3.
Overcoming a major conjecture is equivalent to a cryptographic proof: proving that you have made a real conceptual innovation.
The reason I'm telling this in the past tense is because this pattern no longer holds true. There is a structural flaw in the mathematician’s code of honor, and AI has begun to systematically exploit this flaw.
Analogy between Go and Chess
What inspired me to write this article was a speech by Jeffrey Hinton, which I didn’t expect:
“I agree with the view of Demis Hassabis, the head of DeepMind, for many years: AI will greatly promote scientific progress...
There is one field in which breakthroughs will be particularly easy to achieve, and that is mathematics, because mathematics is a closed system...
I think that within about ten years, AI will be far better at doing math than humans. Mathematics is very similar to closed systems with fixed rules such as Go and chess..."
I already knew there was a huge misunderstanding among the general public about the nature of mathematics. But I never expected that a Turing Award and Nobel Prize winner would compare mathematics with Go and chess.
I wrote a brief reply on the
About a year ago, I was approached by a young mathematician friend who had a PhD in the same field as mine. He planned to start a business and do AI business for pure mathematics, and I provided him with guidance for a period of time.
Like him, Hinton, and Hassabis, I fully believe that AI will reshape mathematics and even science as a whole. But I still can’t figure out what its business model and minimum viable product are.
Mathematicians look like Luddites, but rarely are. They loved pen and paper and blackboard chalk, but they also readily embraced the TeX typesetting system back then. A century ago, everyone chose to rebuild the entire knowledge system on the new "operating system" of set theory, just in exchange for higher reliability and scalability.
A few decades later, the realization of the Currie-Howard correspondence (the deep structural equivalence between computer programs and mathematical proofs, also known as "propositions as types" or "programs as proofs") led to the construction of the first computers. Deep learning relies heavily on linear algebra and stochastic gradient descent, and is itself a product of mathematics.
In the 1970s, Kenneth Appel and Wolfgang Haken used computers to prove the four-color theorem, sparking a fierce debate in the circle of peer-reviewed journals about the epistemological status of computer-aided proofs. To be honest, the ending does not have much suspense: the "barbarians" win, because there are "barbarians" on both sides of the debate.
Computers have long been a part of my mathematical career⁴, and the prospects brought by AI and automatic formalization have always fascinated me. So when a friend came to me for advice, I was very excited.
I began to study the field of "AI doing mathematics" and was puzzled: Why can these start-ups receive huge amounts of financing? The market size of pure mathematics itself is extremely small, and the scale of investment appears completely disproportionate.
The plan I originally preferred was to create a version of Wolfram Research Institute for the AI era. The market for mathematics that empowers science and technology is far broader than pure mathematics. As Wolfram demonstrated, we can simplify the human experience of interacting with mathematical objects into products. Users will love the product and have strong user stickiness.
But my friend insisted that he only wanted to focus on pure mathematics.
I was speechless for a moment. The only available products I can think of are literature search tools and interactive proof assistants; they are difficult to package, difficult to price, and even harder to sell. I can see a long-term business path, but I am afraid of it: becoming the Elsevier of the AI era, the most hated monopoly giant in the scientific community, repackaging public mathematical knowledge and forcing everyone to use it.
However, there is a third option, which is equally risky and requires a considerable degree of cynicism. I call it the "Luxury Acquisition Entrepreneurship Routine":
- Create products that are eye-catching but of limited practical use;
- Create the illusion that major scientific problems have been solved;
- Pray for rapid mergers and acquisitions by technology giants and large AI laboratories.
Even so, the funding numbers still don't make sense. It is rumored that these AI mathematics start-ups have received hundreds of millions of dollars in investment. There must be a set of investment logic behind them that I fail to understand⁵.
Later I heard that Google had invested huge resources in trying to conquer the existence and smoothness of solutions to the Navier-Stokes equation - this was the Millennium Prize problem. I thought, oh, I get it, the target is the Millennium Award. But wait, the prize is just a million dollars, which is really insignificant. A distinguished mathematician told me that Google may have invested more intellectual resources in this matter than the entire academic world combined in its history.
It wasn't until after listening to Hinton's speech that everything suddenly became clear.
If mathematics is really a closed system, or if all relevant stakeholders are willing to believe this, then the investment rhetoric becomes extremely simple and straightforward: "DeepMind has solved Go and chess, and we have to solve mathematics!"
Major AI laboratories are placing trillion-level bets, believing that humans will soon be eliminated. And conquering mathematics, the crown jewel of mankind, has an irresistible temptation for them.
Take a caliper to the battlefield
On February 5, 11 top mathematicians (including 2014 Fields Medal winner Martin Hare) released the First Proof project (First Proof first-round verification project: mathematicians formed a team to set questions to test the AI (10 research-level mathematical questions to torture the most advanced AI, the answers to the questions were announced on February 13)), and released the manuscript on arXiv:
"This article is our preliminary result, aiming to establish a set of objective and realistic evaluation methods to measure the ability of AI to independently solve research-level mathematical problems. After fully precipitating ideas within the community, we hope to produce a more complete set of benchmark tests in a few months.
One of our core goals is to gain a deeper understanding of the role that AI tools play in the workflow of professional mathematicians. Commercial AI systems are undoubtedly already useful tools for mathematicians. But we still don’t know what level AI can achieve by independently solving research-level mathematical problems without the participation of human experts. "
From a purely scientific point of view, it is beyond reproach. This group of extremely smart people confront real controversies, are open-minded and creative.
Everything the First Proof team did was impeccable, but it was this incident that made me panic.
Let me start by saying: I rate this project very highly. The team represents the best people in the mathematics community, full of curiosity and professional ethics, willing to jump out of their comfort zone to experiment, and has indeed produced truly valuable ideas.
Daniel Litt wrote an excellent article "Mathematics in the Library of Babel" (Mathematics in the Library of Babel - University of Toronto mathematician Daniel Litt talks about the future of AI artificial intelligence and mathematics research), analyzing the First Proof project and sharing his first-hand observations on the field of AI mathematics. He is a staunchly non-Luddite pure mathematician who has worked with large language models for many years and is impressed by recent advances.
He was surprised to find that Google, OpenAI and many other organizations have solved many open problems in First Proof. According to his statistics: summarizing the results of each company, about six to eight out of ten questions were answered correctly. Mathematics research agent Aletheia independently solved the FirstProof challenge with a score of 6/10 - powered by Google Gemini 3 Deep Think
But there is a major warning here: the model and the humans who supervise the model produce a lot of invalid garbage, including many solutions that claim to have been formalized in Lean but are actually wrong. Even the best-performing models and auxiliary frameworks cannot reliably identify when they are outputting meaningless content.
Even if the AI mathematical system can really operate autonomously - which most of them still can't do - humans will still need to intervene in the front and back stages, at least to evaluate the results and filter out garbage. This is not hearsay: the manpower invested by AI laboratories in these projects far exceeds the resources that any real mathematician can mobilize, and the boundary between humans and machines has therefore become blurred. The most convincing example:
OpenAI itself can't tell which of the answers they submitted to First Proof are correct.
In other words, without the free contribution of the academic community, they would never know the truth. (Leeteuk himself also participated in the review.)
It is true that proofs written by humans are also fallible. But there are essential differences between the two. When humans do mathematics, theorem proof and concept construction go hand in hand, which forces the proof itself to be understandable (at least to the author himself).
Here the contradiction at the metaphysical level appears. If mathematics were just a formal game of meaningless symbols, then the very concept of "understandability" would be empty. But real mathematical practice gives the exact opposite answer. It is true that published papers are full of bugs, but most of these bugs are limited and can be fixed; precisely because the proofs written by humans are meaningful and almost always in the right direction. These two points are incompatible with the formalist worldview.
This is not a detail, but a necessity for mathematics to survive as a sustainable enterprise.
As Leeteuk pointed out, the AI answer given by First Proof lacks the core quality of "truth-seeking":
"Many correct answers are extremely poorly written, and their correctness is extremely difficult to verify... In human answers, the core ideas and obstacles that need to be overcome are usually clearly identifiable; while in the content of AI output, key points are often unclear. In the process of writing proofs, human authors often refine new objects and terminology to describe their work; but models will only deduce forward blindly."
So the second piece of the puzzle of the AI mathematical revolution appears: automatic formalization. Convert humans' slightly informal proofs and the output of large language models into impeccable logical derivation written in special languages such as Lean that can be completely verified by machines.
On paper, automatic formalization seems to solve the problem of correctness, eliminating the need for manual verification. But Little also wrote: "Among all the problems, there is only one credible formal solution, which was manually completed by Tom de Groot with a lot of manpower."
Of course, things continue to evolve, the stakes are huge and resources are invested. Large models, auxiliary frameworks, and automatic formalization technologies are all making steady progress.
Imagine that one year later, the First Proof team releases another set of ten questions of the same difficulty. What will happen? Leeteuk did not answer directly, but he expected that in the next few years, AI would be able to independently produce results comparable to top journal papers.
I also have the same sentiment. In my opinion, the head AI laboratory is likely to get full marks by then and automatically provide the correct answers to all ten questions.
Does it mean that by the beginning of 2027, AI has “conquered mathematics”?
Of course not. There are three key reminders that industry insiders can understand at a glance, but ordinary readers can easily ignore.
Warning 1: Heavy ocean
The first point is very straightforward: these "research-level questions" of First Proof are not very profound and have limited difficulty. They prefer technical lemmas, which are intermediate subproblems that arise in the process of proving the big theorem and can be dealt with in a few pages.
From a technical lemma to a serious paper, there is a vast ocean; from a paper to a major breakthrough, there is another ocean; from a major breakthrough to a Fields Medal-level achievement, there are even more oceans. There is a higher realm beyond this.
First Proof’s second batch of questions is being prepared and is expected to use more difficult questions.
From a technical point of view, the choice of this difficulty level for the first batch was reasonable, and this was also clear in hindsight: the final score was between 0-10, which fell right in the sweet spot of its preset goal-to establish an objective and realistic evaluation method.
But releasing a set of benchmarks that doesn't include truly deep and difficult problems is extremely risky. The general public will not read the fine print and many people do not even know what a lemma is. If Google or OpenAI gets perfect scores, the headlines will read:
"Game over: Top mathematicians threw ten research-level problems to the AI, and the AI swept them all."
Similar distortions occur every day on social media, fueling exactly the misunderstandings that First Proof wants to dispel.
Warning 2: Accumulation
The second point is much deeper, subtler, and difficult to explain to the general public.
The problem with unreadable proofs goes far beyond correctness; automatic formalization alone cannot solve this dilemma. Even if the proof itself is correct, an unreadable proof cannot make a cumulative contribution to the mathematical knowledge system.
It sounds outrageous, let me give you an example. A few weeks ago, Math Inc, a well-funded AI mathematics start-up, completed Marina Vyazovska’s Lean formalization of the results of stacking 8- and 24-dimensional spheres. The collaboration between AI and humans ushered in a milestone moment in the field of mathematics - the Fields Medal winning certificate in the 21st century completed formal verification for the first time - IEEE Spectrum's set of results helped Vyazovska win the Fields Medal.
This thing itself is quite shocking: for the first time, a Fields Medal-level theorem has been automatically formalized. 2026.5 Future of Mathematics Seminar Series - Formalization of the Sphere Packing Problem by Maryna Viazovska (2022 Fields Medal Winner) - Stanford FMS However, this feat has been strongly resisted within the formal chemistry community - precisely the group of people who are committed to transplanting human mathematics into machine-verifiable code.
Are they Luddites?
Things are far more complicated than that, as Zulip chat records show⁶. Automatic formalization does not equal a complete formal mathematical solution, just like Tesla's fully autonomous driving does not equal a complete autonomous driving solution.
It sounds counter-intuitive, so it’s easy for outsiders to interpret resistance as resistance to new technology. Alex Kontorovich wrote a good lecture note explaining this. To put it simply: Mathlib, the mainstream Lean library, is a formal mathematics library compiled by humans. It has a clean application interface and abstraction layer; without these, any automatic formalization is impossible. In contrast, the Vyazovska proof produced by Math Inc does not expose any usable and understandable interface. Who in their right mind would want to merge two hundred thousand lines of unaudited, feel-generated code into the main branch of all human science?
Kantorovich came up with a wonderful word: canonization.
"Standardization refers to transforming one-time partial formalization results into library-level mathematics: universal, reusable, self-consistent, efficient, and compatible with other systems... Standardization often changes the system itself: definitions, abstractions, interfaces, and even proposition statements... This matter is extremely energy-consuming and time-consuming."
But this could easily lead to being labeled a Luddite. "Universal, reusable, self-consistent, efficient...Are these just conservative rhetoric made up by narrow-minded humans? Why does AGI care about these? Doesn't automatic formalization by definition solve all the problems of writing code by feel?"
Doesn’t the proven code meet the highest standards for software? Why do you keep moving the goalposts?
Analogies from the software field can help us see the core contradiction clearly. For ordinary software, quality first depends on practicality: it can be compiled, runs stably online, and meets user needs. But Lean code is never "run". It is only stored in the code base, and I don’t know when other theorem formalizations will be imported and called in the future. You can't do "continuous deployment" because its only users are future mathematics researchers. Therefore, from Euclid's "Elements of Geometry" to Zermelo-Frenkel's set theory, and then to Bourbaki, normalization has always been the core concern of the formalist school.
We are back to the metaphysical level. The problem with unreadable mathematics is not that it can go wrong. The real problem is this: it literally loses its meaning. Because it cannot be "compiled and run" on the human brain, the only hardware that can understand and appreciate its value at the moment.
Of course, things can change in the future. There is nothing magical about the human brain. In the future, artificial meaning generation and truth-seeking structures will inevitably be born, surpassing humans in all aspects of mathematical creation, including formal proof standardization. But that is definitely not the reality we live in now, nor can it be arrived at by simply extrapolating existing trends; the conditions for a productive debate are not yet there.
No matter what, as long as humans exist, we will still have a desire to understand the world, and this desire will continue to drive us to study mathematics.
No one knows when general artificial intelligence will arrive. The automatic normalization capabilities of current top models are almost zero. Math Inc's 200,000-line proof of Vyazovska became a lonely, unmaintained block of code.
This is the source of the anger of the Mathlib community. They have been working as a team for many years and were already doing formal work on Vyazovska's results. Math Inc stepped in, taking advantage of previous experience and hyping up its results.
Is this necessarily a bad thing? Now that the automatic formalization of brute force has been completed, why can't the Mathlib community turn to valuable standardization work?
Because Hardy's curse, the mathematician's code of honor, is still in effect. Math Inc has already taken away the honor of being the first to complete the formalization of Fields-level theorems, and there will no longer be any academic reward for cleaning up the follow-up work. Formal mathematics expert Patrick Massot wrote this:
"The status quo is clear: AI companies, especially Math Inc, will completely blow up the field into a radioactive wasteland that will no longer be able to breed new results. We will never get the benefits that formalization is supposed to bring: improved understanding and accessible knowledge. I strongly encourage young people to invest in projects that cannot be easily destroyed in this way."
Even if the overall knowledge base cannot be accumulated, unreadable formal proofs can still have residual value.
To be honest, this problem existed long before the emergence of AI: the four-color theorem, the classification of finite simple groups, and Tom Hales' huge Kepler conjecture work all fall into this category, and the latter also prompted him to embark on the path of formal proof.
In the future, it is likely that two levels will coexist: one is the readable layer represented by Mathlib; the other is what I call Mathslop, a bunch of result libraries whose correctness is known, but no one has read the proof.
Warning 3: The Overhang
When the First Proof questions were first released, my biggest worry was that major AI laboratories would easily solve all ten questions, but the reason was not obvious: the answers to these questions already existed in some form in the existing literature.
Lee Teuk mentioned that among the ten questions, two questions have solutions in existing literature⁷, and many large models can naturally be used; the third question has a proof outline, but no model can solve it.
What about the remaining seven paths? Are they really open questions that remain unresolved? In what sense is it considered open?
My view is that our inability to give a firm answer stems from the structural nature of the mathematical knowledge base itself, a quality that will take center stage in the AI‑mathematics debate. I even suspect that our traditional concepts of "creativity" and "innovation" are fundamentally flawed, and AI will teach us a cruel lesson.
Most mathematicians have a vague sense of this structural quality in their hearts, but no one has completely mapped it, and there is no generally recognized name in the academic world. I call it the Overhang.
I believe that the volume of suspended stock is extremely huge.
I have encountered it many times in my career, and most of them were just ordinary experiences. Only one time I was extremely shocked. I just conceived the core concept in Definition 9.3, which was later called "splitting the Garside category". I think this is a very original idea that can solve the classic conjecture. Subjectively, I felt like a flash of genius at that moment.
When I began to formalize this most creative idea, I was shocked to discover that the invention I was so proud of was essentially equivalent to an existing construction in an obscure document in algebraic K-theory.
In other words, my so-called genius idea has already appeared elsewhere. Or maybe not? Twenty years later, I still regard that moment as the highlight of my career. I don't care if it's strictly original, I don't think that's the most important criterion. What really moved me was the surreal moment when meaning emerged. (This is the cognitive sign of a high-value outcome.)
In any case, an excellent large model, when my research is still in the early stages and I can't see the direction clearly, can capture the similarities at the syntactic level, publish the results first, and "cut off" me.
The profound correspondence between different fields of study is one of the most amazing qualities of mathematics, a source of joy and wonder, and a pure expression of its beauty. Descartes noticed that algebra and geometry were essentially interconnected and built a bridge between them, thus changing the world. Once the Cartesian coordinate system is invented, a lot of old problems are solved, and a lot of interesting new problems are immediately born.
But modern mathematics is vast and complex, and many of these correspondences remain unknown.
Sometimes when you connect the pieces, what you get is not a discovery, but a deeper mystery. A classic example is John McKay's famous observation: 196883 + 1 = 196884. 196883 comes from the study of large demon groups, and 196884 comes from modular form. The two fields were originally unrelated. The conjecture that there was a connection between the two sounded absurd at the time and was called the "Moonlight Conjecture." Richard Borcherds won the 1998 Fields Medal for proving this conjecture.
But sometimes, just correlating existing document fragments is enough to solve major conjectures. The final step in proving a conjecture is often the realization that the missing material is already buried in past papers.
Suspended stock is the potential value of past mathematical creativity that has not yet been realized. It is the dividend that can be released by interconnecting the fragments of the existing knowledge base, and it is also the gift brought by standardization. Mathematician A poses problem A; mathematician B creates concept B; then mathematician Z notices that B can directly solve A, so Z gains this social recognition. But in the process of gaining recognition, Z usually introduces new concepts and new open conjectures, injecting new potential value into the suspended stock.
Large language model training materials can consume all mathematical literature. With their amazing memory and pattern-matching abilities (although not always able to sort out the logic of connections and correctly label sources), they are uniquely equipped to mine this suspended stock. On the other hand, professional mathematicians will read only a few hundred papers in their lifetime. Compared with the millions of documents in the total database, they only account for less than 0.1%.
This event will undoubtedly lead to exciting and important discoveries. But it will also lead to a sad new situation: humans work hard to sort out and accumulate suspended stocks, but AI always intercepts humans at the finish line.
Of course, this scene is still far away, and the event itself is confusing. Leeteuk raised a sharp question: Human beings have this kind of ability and will almost continuously produce amazing theorems; so why haven't models done it yet? What exactly is missing from the model?
The answer is actually obvious: Today’s AI systems and humans process mathematics completely differently. AI is far superior to humans in some aspects and weaker than humans in many aspects.
AI is both "superhuman" and "subhuman" at the same time, depending on your perspective. This is both an affirmation of AI and an affirmation of human beings. This multi-dimensional nature makes the entire benchmark system fragile, even almost unreal. It is entirely possible that AI will achieve a crushing advantage at the problem-solving level before realizing the ability to construct concepts. So what should we call it? "Super intelligence"? Seriously?
This is my core concern about the First Proof paradigm. It is a valuable benchmark for working mathematicians stuck in outdated codes of honor who want to understand what AI can do today.
But why don’t we establish a set of benchmarks that are fairer to humanity? Because we can't. The real value of mathematics is to expand our perspective on the world at the individual and collective levels. This thing is vaguely defined and cannot be quantified. It is precisely this unquantifiable that gave birth to that code of honor.
Grothendieck lamented the difficulty of his Grothendieck-Riemann-Rohe theorem
For thousands of years, we have been accustomed to measuring human intelligence solely in terms of “problem solving” because it is the best objective proxy. Proving theorems is extremely difficult for our cognition. The only way forward is to patiently construct concepts and internalize these new concepts in our minds.
But it is only a proxy indicator after all. What we really care about is something entirely different. Industrial robots are far more powerful than humans, but we still go to the gym. Blenders can chew far better than humans have for hundreds of years, but we don't just rely on straws to eat.
I know it looks bad. Claiming that mathematics is first and foremost about understanding, and that understanding is difficult to measure, sounds like a very contrived excuse. But I didn’t just make this up on the spur of the moment. Five years ago, before the AI wave took off, I wrote on X:
"People usually think of mathematics as the pursuit of universal truths and the pursuit of patterns that are not tied to specific contexts. But on a deeper level, the goal of mathematics is to develop new and advanced ways of seeing and thinking about the world. Mathematics is a journey of transforming ourselves; the yardstick for measuring progress is the change in the way we think, not the external truths we discover."
I quote this passage in my book. Descartes’ 1628 lament was also quoted: Ancient Greek mathematicians, with some harmful ingenuity, “covered up real mathematics” (Descartes equated it with internal cognitive methodology), leaving only some childish and meaningless results. They only publish some barren truths and elegant proofs produced by this method, but do not teach the method itself⁸.
Terence Tao also expressed something similar:
“A lot of times, the process itself is more important than the problems. Problems are just a proxy for measuring progress.”
He also made a striking prediction:
"I think that within ten years, a lot of the work that mathematicians spend a lot of time doing now, and a lot of the content in our papers, can be done by AI. But by then, we will find that those are not the most important part of our work."
Feedback on social media has been overwhelmingly positive. But there have also been unusual objections to the idea that simply solving the problem itself is not that valuable.
For advocates of general artificial intelligence, these words seem to refuse to see the reality before them, and even contain ridicule.
Alerts are not drills
On March 3, Jeremy Avigad, the first director of ICARM, the newly established Institute for Computer-Assisted Mathematical Reasoning, published a five-page article on arXiv entitled Mathematicians in the Age of AI Artificial Intelligence - Jeremy Avigad. The article reviews the conflict between Math Inc and Mathlib in detail, and Avigard himself was a witness. He is also an open-minded researcher who is by no means a Luddite, and is in an excellent position to observe this great change:
“We have to face reality: AI will soon be able to prove theorems better than humans…
We need to remember our strengths: Mathematicians are top problem solvers and theory builders. Don’t resist the use of AI in mathematics, we must take the initiative to control it. It’s not enough to simply keep up with trends and design benchmarks for AI researchers; we need to proactively deploy this technology and shape it according to our goals. "
Talking about the First Proof project, Avigard wrote that he was "surprised" that Google could solve six of the ten problems.
After reading all of the above, I would describe my feelings as "relieved" rather than "surprised". Of course, I was indeed surprised, because I had no intuition about the actual difficulty of these questions, nor did I predict how many questions would be solved.
What really makes me uneasy is Avigard’s slightly relaxed description: “Many AI developers have taken the bait.”
I don't know if this statement is ironic or naive. People who are familiar with the ecology of the technology industry can see clearly: Once this set of questions is released, it will inevitably trigger a crazy competition with the highest priority in the major AI laboratories. Who wants to miss such an opportunity?
OpenAI President Greg Brockman said of First Proof:
"First Proof is a great concept and solution. Congratulations to the entire team and thank you!"
This incident happened on February 14, when OpenAI was conducting a road show to strive for the largest round of private technology financing in history. What’s even more interesting is that during those stressful weeks, more than one person in the OpenAI management team was distracted by this geek-oriented side business. A few days ago, Sam Altman took the time to write some code and lamented that Codex made him feel "useless."
But is this really a “distraction”? You can interpret it as a big fish eating the bait; you can also interpret it as a fox thanking the hen for handing over the key to the henhouse.
To be clear: I don’t think OpenAI or other AI labs are doing anything nefarious. After First Proof made the topic public, they had no choice but to devote all their efforts to participate in the competition and could not accept being outcompeted by their opponents.
In fact, the AI laboratory does have exciting technology, and theorem proving is indeed an attractive application scenario.
The real problem comes from the outside world's interpretation of this matter.
This is what’s so unsettling about Hinton’s speech. He reduced mathematics to a low-hanging fruit, an "exceptionally simple" field, on the grounds that "it is a closed system with rules," "like Go or chess." But Go and chess are not ordinary closed systems; they are two-player limited complete information games with a clear winner and loser. According to the 1913 Zermelo theorem, they have optimal strategies⁹.
But if AI "wins" in "mathematics", who will be the loser? The only opponent in this room is the human mind.
Even though mathematics is not an adversarial game, the rules are still evolving. But as long as the news is sensational enough, it deserves coverage.
Imagine a worst-case scenario: a year later, an AI laboratory forms a secret top team, invests billions of dollars in computing power, and produces a two-million-line Lean proof for the Riemann Hypothesis. How can mathematicians respond?
"This certificate is unreadable." - True, but who cares? The vast majority of humans do not understand most mathematics natively.
"Proof still cannot be separated from human participants." - Yes, but in this case, I will most likely vote against it.
"Billions of dollars, equivalent to the entire mathematical and physical science budget of the National Science Foundation for decades." - Even so, so what? What if the difficulty of this conjecture is actually very low and only requires a small amount of resources?
"But the conjecture itself, together with the entire mathematical system underneath it, including infinite series, complex functions, meromorphic functions, analytic continuations, and the interpretation of the conjecture into profound propositions about the distribution of prime numbers, are all created by the human brain; so far, only humans really care about this issue."
This rebuttal is profound and defensible. But once you look like a loser who can't afford to lose, no one will listen to you.
I didn't expect this exact scenario to actually happen. But in the near future, we will most likely see statements claiming that "AI has conquered mathematics" and "achieved mathematical hegemony." Combined with the current public opinion environment, this evidence will be interpreted as a collapse of human intelligence.
If even Jeffrey Hinton can't see through this layer, then 99.9999% of ordinary people are even less likely to understand it.
When a disaster really strikes, no matter how much you want to speak out in your heart, mathematicians must start practicing expressing it from now on. It may be too late to completely avoid this impact, but at least we still have some time to predict and unite.
A dangerous signal is the trend of young mathematicians, many of whom choose to join AI laboratories. Frankly, I understand their choice; if I were in their shoes, I would probably make the same decision.
Meanwhile, untenured academics express despair. Ashwin Swaminathan, a postdoctoral fellow at Harvard, read Little’s article and deeply agreed with it. He wrote a long post on X, talking about the core issue of teaching:
"Some people would think that research mathematicians can maintain their jobs by teaching. But this ignores the huge impact that AI has had on the teaching field. Now a large number of students use AI to complete homework, and college diplomas will soon depreciate in value. The number of students who come to me for Q&A and participate in office Q&A time has plummeted. Students have good homework scores, but poor exam performance. Many children graduate without mastering real skills."
I want to emphasize that this matter is essentially the same as the dilemma encountered in the research field. Solving problems is only a means to an end. The real reward of pure mathematics is that our worldview is improved at the neurological level; simply copying and pasting ready-made answers cannot achieve this goal.
The misconception that "mathematics is just about proving propositions and obtaining results" has poisoned everyone from the basic education stage.
Especially the widely circulated statement: "AI can already complete PhD-level research." Even if this statement comes true, its persuasiveness is far less powerful than it seems. Doctoral students are still students after all. What responsible supervisors give doctoral students are strategically feasible issues. In fact, the vast majority of published research falls within the category of suspended stock; part of it is real research, and part of it is maintenance work to maintain the cognitive operation of the research community. This is not to belittle my colleagues, but rather reflects the difficulty of cutting-edge mathematics itself. Frontier mathematics can only exist as the spearhead of a collective undertaking, and the foundation of this undertaking is to ensure that the content is understandable to humans.
If proving theorems remains the only hard currency in our system, all research mathematicians will face the risk of being deprived of their value in the next few years.
face reality honestly
What can the mathematics community do? I don't see a miracle solution, but there are some obvious things you can do to mitigate the damage. First things first: we need to finally be honest about what mathematics actually is.
The mathematicians I have cited, from Terence Teru to Avigard, from Little to Kantorovich, are careful to point out that there is more to mathematics than theorem proving. But this is often just a passing mention rather than a significant shift in narrative paradigm.
And this very thing requires a complete change in the narrative paradigm. If this matter is not explained thoroughly, the public will only regard these remarks as an excuse. If you want to reshape a cognitive label that has lasted for thousands of years, you must clearly explain what you are doing, why you are doing it, and what value it can bring to everyone. This matter must be heavy and difficult, and the window period left to us is very short.
This is probably the largest conceptual “product recall” in memory: We sold billions of people a false belief about mathematics, and now the bill is on us.
The only way out is to put the core proposition at the front and reiterate it again and again. I quote Thurston again (Avigard also placed it at the beginning of his article "On Mathematical Understanding"):
"We are not aiming to complete abstract production indicators such as definitions, theorems, and proofs. The measure of success lies in whether what we do can help people understand and think about mathematics more clearly and effectively."
In the long run, this will force us to completely rethink the spiritual core and evaluation standards of this industry. Mathematicians must abolish the honor code and abolish the second rule of the Intuition Club: "If you must talk about intuition, do so lightly, as if it were just ancillary. After all, we are not a psychology department." If Thurston is right, then we should be considered a part of the psychology department.
Easier said than done. The mathematics community is not an organization that can hold emergency closed-door meetings and produce crisis response plans.
We don’t even agree on mathematics itself. Some people truly believe that the whole point of mathematics is to solve unsolved problems; others believe otherwise. I don't agree with either point of view, but ultimately my opinion is just my personal opinion.
Lacking a clear definition and mission statement, the entire community is passive.
Christian Szekedi, co-founder of xAI and Math Inc, once predicted that a “superhuman mathematician AI” would appear before June 2026. Such claims are either empty words (electromechanical calculators have surpassed human computing power for hundreds of years) or they are the ultimate grand narrative. Not surprisingly, Szegedi also said that he believed Terence Tao was "out of touch with the fast-approaching reality."
The problem wasn't the prophecy itself. Szekedi had a solid technical background and the authority to come up with big ideas. The real problem is that the public opinion environment makes it difficult for rational rebuttals to be heard.
An idea pops up repeatedly in my mind: We need a set of mathematical intelligence grading/mathematical automation grading similar to the car's self-driving grading.
This addresses the urgent risk of the moment: benchmarks only measure problem-solving skills and completely ignore comprehension and concept-building abilities. When AI sweeps the new First Proof test set, the press release can read: "AI passed First Proof and reached level 3 (out of 10) in the mathematical intelligence grading."
Mathematicians should not fear subjectivity. This does not amount to cheating; it is about pursuing fairness and avoiding collective self-destruction. In fact, the question itself is full of subjectivity. For First Proof's questions, Erdesh's problem, and the Millennium Prize problem, except for "objectively judging whether a proposition has been proved", there are no purely objective standards for the rest.
As for the more profound dimensions of mathematical creation—raising questions, standardizing, constructing concepts, reconstructing problems, simplifying, conjecturing, and even constructing complete new theories and opening up new branches—there are no objectively verifiable standards for these things, but it does not mean that these activities do not exist, nor does it mean that they are unimportant.
There is also an objective dimension in subjective judgments. When Descartes unified algebraic geometry and Newton and Leibniz invented calculus, it was obvious to their contemporaries that major breakthroughs had occurred. In a sense, the entire technology system, including AI start-ups, is enjoying the dividends brought by these creations.
The ideal grading system should be open-ended, with a seemingly out-of-reach top tier. Because mathematics is not something waiting to be "solved."
Mathematics is endless and the problems are endless, which means there is endless room for improvement. The most urgent thing at the moment is to let everyone understand that mathematics is not a trophy waiting to be snatched.
the future of mathematics
Sadly, a lot of harm is already destined to happen. Even if executed perfectly, we cannot complete a cognitive revolution under the pressure of external timelines. The current environment is extremely unfriendly to basic science, and every nuance will be immediately interpreted as an excuse for the gatekeepers.
Life can get tough for mathematicians. Students will be lost and funding will be cut. Postdocs will ask tough questions, and senior professors must answer them. At parties, others will look at you strangely, as if you are a living fossil.
But the stress will eventually ease. The industry will return to normal, and AI mathematics startups must find their own business models. From a high probability point of view, it will not be to solve the Erdesh conjecture.
To me, that’s the most striking thing about the current era. Despite their great momentum, major AI laboratories have hardly invested in truly understanding mathematics itself and its core issues and significance. Of course, this is understandable, as this is not their job.
When the dust settles—if it ever settles—human mathematics will survive, just in a metamorphosis.
I don’t make time predictions. I don’t know when and which abilities will be achieved and what limitations there will be.
But changes are already happening. This is a true scientific revolution, and the research community is already engaged. When I write this article, I can see a lot of new developments in the information stream every day, and it is too much to be seen.
Pessimists would say that this is just a fear-driven reaction and that similar shifts are occurring in all walks of life. Capital is being reallocated so quickly and on such a large scale that there is no rational way for us to fully prepare for the future.
If I had not left frontline research, I don’t know what I would have chosen. An easily accessible direction is to use AI to generate a formal proof of the cell decomposition theorem that I have not yet written. Then test various bold ideas and conjectures. But these are old-time ways of thinking. I suspect that the collaborative model of future mathematical research, as well as the output itself, will have to change.
My opinion is not very novel: doing mathematics in the future will be inseparable from AI assistance, just as doing mathematics now is inseparable from set theory and LaTeX. This will become a matter of course.
But that doesn’t tell us what the second-order effects will look like. I did some deductions and thought of more than ten possibilities, but not all of them are profound and credible. Here are three that I think are interesting:
My point of view: Purity and application, they represent different optimal balance points in the "understandability-practicality trade-off". It is reasonable to invest tens of billions of dollars in computing power to solve the plasma confinement equation and accelerate the realization of grid-scale fusion reactors, even if it will take another one or two hundred years for humans to fully understand it. But I don’t think this logic applies to the Riemann Hypothesis.
I suspect that the changes AI will bring to mathematics will be similar to the changes brought to the music industry by samplers and sequencers. The technical threshold for mastering cutting-edge concepts will decrease. Brave young mathematicians can use unconventional means to quickly explore an entire new continent of knowledge, astonishing the older generation.
Standing on the shoulders of giant machines, they can see farther than their predecessors.
AI has brought about unexpected real-life consequences, which has begun to affect the cognitive and mental health of the general public. If we don’t understand the cognitive value of comprehensibility, there is no reason to teach mathematics. After all, 99.99999% of the mathematical problems that ordinary people encounter in their lives can be answered by AI at their fingertips at any time.
People are vaguely aware that this will lead to an ignorant society, but they don't know why. We still do not have a teaching and evaluation model that adapts to the reality of the new era.
What’s really worrying is the misperception that there is some “normal” level of math ability, as if some concepts are more real and concrete than others, and that advanced math is just gratuitous abstraction. This illusion makes everyone think that the current mathematics level of ordinary people is the "natural state"; but in reality this is the result of a large amount of teaching investment that is not very efficient, and is not a natural benchmark. It is possible for humans to evolve a culture whose language only has numerals up to five, as is the case with some hunter-gatherer tribes.
Some predict that in the future mathematics will become like chess: a handful of eccentrics working on it with zeal and the masses ignoring it.
This is a short-sighted view that ignores the meaning-making and truth-seeking qualities of mathematics, as well as the huge cognitive benefits that mathematics training can bring. Once you develop an intuitive understanding of numbers, sets, statistics, linear algebra, calculus, differential geometry, machine learning, combinatorics, dynamical systems, model theory, group theory, singularity theory, homotopy theory, lambda calculus, category theory, the way you see the world will become much clearer. (The list can go on indefinitely, but of course it’s not realistic to learn everything in one go.)
This dilemma is not unique to mathematics. Many fields will encounter similar problems when adopting AI. But mathematics has a unique status and aura because it has been deeply bound to the concept of "intelligence" since ancient times.
This is why the issue of "AI doing mathematics" is so important. Handling this matter properly is related to the future of the human species.
Many people hate mathematics and confuse AI with mathematics. They regard everything related to mathematics and computers as a threat to human nature, subjective experience, and living reality.
But they will be pleasantly surprised and grateful to find that mathematicians are actually on their side, fighting for good.
As Carl Gustav Jacobi said:
"Mathematics exists for the glory of the human spirit."
(There are already 120+ comments in the comment area, and the author has made some replies. See the bottom of the original article for details)
https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy/comments
Mathematicians in the era of AI artificial intelligence - Jeremy Avigad
Voices of Mathematicians: What is mathematics and what should mathematics be? Jeremy Avigad2026-8-18
Spoilers for the 1-hour report of the 2026 International Congress of Mathematicians ICM Plenary Session: "The Shape of Future Mathematics" by Alex Kontorovich Alex Kontorovich
Voice of a Mathematician: Daniel Litt Daniel Litt "A New Beginning in Mathematics" 2026-9-14
Mathematics in the Library of Babel - University of Toronto mathematician Daniel Litt talks about the future of AI, artificial intelligence and mathematics research
Exclusive interview with mathematician Daniel Litt: The mathematical capabilities of AI artificial intelligence may be in a state of uneven development for a long time (Part 2)
Exclusive interview with mathematician Daniel Litt: The mathematical capabilities of AI artificial intelligence may be in a state of uneven development for a long time (Part 1)
Machine-translated from the Chinese original 数学家心声：《定理经济的陨落：AI何以几乎毫发无损地摧毁数学》by David Bessis 2026-4-21 (published 2026-04-21). WeChat original ↗