What Is the Role of Mathematicians When AI Can Do Math?

What Is the Role of Mathematicians When AI Can Do Math?

In the mid-2000s, while The Killers and Franz Ferdinand blasted from every bar and nightclub, I was grinding through a PhD dissertation in applied mathematics day and night. My research focused on simulating how special light waves interact inside liquid crystals, using simplified equations to approximate and understand those interactions. Looking back at that thesis now, liquid crystal technology is hardly cutting-edge, and I can easily imagine my research being completed in days — or even hours — with AI assistance.

The same cannot be said, however, for the pure mathematics PhD students who shared a cramped Edinburgh University office with me at the time. I pitied them somewhat back then — they sat at their desks day after day looking furrowed and seemingly making no progress. (I was struggling too, but at least I could feel some forward motion.) After graduation, we scattered, and some hadn't even published a single paper.

Only now, in retrospect, do I understand why they were willing to spend years on abstract mathematical problems that only a handful of people in the world cared about. It wasn't the arrogance I first assumed — a desire to be the first to crack an apparently unsolvable problem and prove superiority. Nor was it my second guess: some form of self-punishing asceticism. I finally understand that what they drew from that long journey of understanding was joy, a sense of achievement, and meaning.

---

"Sometimes, the understanding itself feels very beautiful." — Jeremy Avigad, Carnegie Mellon University

---

"Sometimes, the understanding itself feels very beautiful; sometimes it's like the sense of achievement from completing a marathon," reflects Jeremy Avigad, a mathematician at Carnegie Mellon University. "But it's not quite either of those: when you've been thinking hard about a complex and difficult problem for a long time and suddenly — everything clicks — that feeling is truly wonderful."

This feeling has driven mathematicians across generations. Equally, the ways mathematicians pursue it have changed little over centuries: they perceive or imagine connections, patterns, or properties among numbers, shapes, or logical structures, and formulate conjectures — unproven speculative statements. Then they, or other mathematicians, use logical reasoning and mathematical tools — often in highly creative ways — to prove or disprove those conjectures. Finally, still other mathematicians verify (or challenge) the proofs.

The process typically demands extended periods of deep thought. "I attended a pure mathematics camp where we'd spend half an hour in class facing a difficult problem and no one would speak — everyone was just thinking," says Krystal Maughan, who is completing a PhD in mathematics and computer science at the University of Vermont. "But afterward we'd work together and slowly unravel the problem."

This is the ancient pleasure of mathematics in action. Yet today's AI systems are beginning to encroach on this slow, deliberate process. If the trend is taken to its logical extreme — if AI makes the mathematician's struggle entirely redundant — could humans be pushed to the margins entirely?

AI's Growing Role in Mathematics

Computational tools have been accelerating mathematical progress for decades. It began fifty years ago when mathematicians used computers to prove the Four Color Theorem — that any map can be colored using no more than four colors such that no two adjacent regions share the same color. The answer was yes, but the computer proved it by verifying 1,936 cases, and the controversy was that no human could realistically check the entire process.

Throughout the computational era, however, human mathematicians remained central even in proofs that relied on massive computing resources: humans posed the conjectures, designed the strategies, and validated the results.

Now, AI is challenging that established order. Within just a few years, large language models (LLMs) have evolved from "stochastic parrots" that could only regurgitate basic mathematics found online into sophisticated mathematical reasoning machines.

Last summer, systems from Google DeepMind and OpenAI achieved performance equivalent to the world's top mathematics-gifted high school students at the International Mathematical Olympiad (IMO), winning gold medals. Earlier this year, Google DeepMind's experimental AI system Aletheia reached an even more significant milestone — autonomously producing publishable PhD-level research by computing structural constants in arithmetic geometry, demonstrating complex reasoning capabilities when tackling unsolved mathematical problems. More recently, OpenAI's new general-purpose AI system disproved an important conjecture in combinatorial geometry, with leading mathematicians hailing it as a landmark demonstration of AI performing independent, original, and deep mathematical thinking.

Another major shift has come from combining LLMs with proof assistants — tools that have existed for over a decade, including specialized programming languages such as Isabelle, Lean, and Rocq, which can verify the logical correctness of mathematical proofs step by step. Previously, mathematicians had to manually translate theorems and proofs into machine-readable formats — a time-consuming process called "formalization." Now, LLMs are beginning to remove that bottleneck, automatically converting informal proofs into formal code that proof assistants can verify.

---

From Human Proof to Formal Proof

Euclid's famous proof that there are infinitely many primes looks very different once formalized in Lean. Human mathematicians habitually skip steps and rely on shared understanding; formalization makes every assumption and inference explicit so that a computer can verify them.

Human version: We want to show that for every natural number n, there exists a prime p such that p ≥ n. Consider the smallest prime factor of n! + 1, call it p; clearly it is prime. To show p ≥ n, suppose otherwise — then p divides n!, and therefore also divides (n! + 1) − n! = 1. But this is impossible: p is prime, and 1 has no prime factors. Hence p ≥ n.

Lean formalization: Every definition must be explicit; the formal proof builds on previously verified theorems; implicit logical steps must all be stated explicitly — one cannot simply say "obviously" it divides.

---

Such systems — sometimes called reasoning agents — are growing increasingly sophisticated. In February of this year, AI company Math, Inc. used its reasoning agent called Gauss to formalize the work of mathematician Maryna Viazovska (EPFL, Switzerland), who received the Fields Medal in 2022. Gauss first helped human mathematicians formalize the 8-dimensional sphere-packing problem within a few days, then autonomously completed the formalization of the far more complex 24-dimensional case within two weeks.

These achievements indicate that AI can already handle certain mathematical tasks long considered to be exclusively human. As the technology continues to advance, an ever-growing portion of human mathematicians' day-to-day work may well fall within AI's reach.

The Debate Among Mathematicians Over AI's Role

---

Human mathematicians could become "priests of the oracle." — Yang-Hui He, London Institute for Mathematical Sciences

---

In September 2025, I attended the 12th Heidelberg Laureate Forum — the annual gathering that brings together hundreds of young mathematicians and computer scientists with their academic heroes. AI dominated every discussion, and from the outset the air was charged with tension.

Speakers described a future of superhuman AI mathematicians: posing conjectures, searching solution spaces, proving conjectures, verifying proofs, and generalizing results — all without human intervention. Yang-Hui He of the London Institute for Mathematical Sciences made a striking declaration: if that future arrives, human mathematicians could be reduced to "priests of the oracle."

As those stunning predictions were delivered from the stage, my attention was drawn to the audience. Furrowed brows, restless shifting, uneasy glances exchanged — the disquiet was unmistakable. Trill White, a student from Deakin University in Australia, later recalled sitting in the hall thinking: "'This is so depressing. What can people still contribute to mathematics? Will mathematics become something no one understands?' I really felt this was going to change everything."

---

"We really are starting to realize that AI has the potential to replace us." — Jessica Randall, Google Developer Groups

---

Jessica Randall, a South African mathematician with Google Developer Groups, said she could feel a collective existential dread rippling through the younger mathematicians. "I could sense that everyone was very worried, because they hadn't thought that far before," she said. "It was like a big bomb suddenly going off — we really are starting to realize that AI has the potential to replace us."

Some senior mathematicians, including He, appeared sanguine about AI taking over tasks currently performed by humans. They simply want to know the answers to mathematics' greatest open problems — such as the six remaining Millennium Prize Problems — regardless of whether AI or humans solve them. "A lot of mathematicians are pragmatic and just want to figure things out. They'll sell their soul to a solution," Avigad jokes, "no matter the means, right?"

But the "just-want-the-answer" camp is far from the only voice. Most mathematicians neither want nor expect AI to replace them entirely. Two broad alternative visions are emerging: a human-centered ideal that treats AI as a tool (like a calculator), prioritizing human mathematical understanding; and a collaborative "teamwork" vision in which humans and AI work together to solve problems neither could tackle alone.

The Human Role in Mathematics

---

Numbers are "a way for us to reach agreement." — Akshay Venkatesh, Princeton University

---

Fields Medal laureate and Princeton University mathematician Akshay Venkatesh has been thinking about this question from a human-centered perspective for years. In 2022, at a Fields Medal symposium, he made a heartfelt appeal to the mathematical community to reflect on AI's implications for mathematical practice. The idea of AI replacing mathematicians still seemed remote at the time; today, he says, "We are gradually reaching a point — at least for some tasks involving abstract mathematical reasoning — where computers are beginning to rival humans."

For Venkatesh, the question is not only what computers can do, but why mathematics exists in the first place. "Sometimes I feel that when we use numbers, rather than describing phenomena that are inherently numerical, it is more that we can reach precise agreement on what numbers mean," he says. "It is a way for us to reach agreement."

Maia Fraser, a mathematician and machine learning expert at the University of Ottawa, agrees. She says the joy she draws from mathematics is a distinctly human experience that blends the subconscious and the conscious — from intuitively sensing that something ought to be true, to gradually distilling it into a rigorous proof. Communicating and sharing thoughts that emerge from deep within, she says, "is a collective intelligence, a beautiful part of the human spirit."

By this argument, even if AI produces a proof of a conjecture that has long resisted human efforts, its usefulness still depends on whether humans can understand it. "That AI can prove this proposition is already useful information in itself," Fraser acknowledges, "but afterwards, finding an elegant and beautiful human proof remains an open problem." Even if no such proof exists, she says, searching for one "remains a worthwhile endeavor."

The Future of AI–Mathematics Collaboration

A more collaborative vision for AI in mathematics comes from Terence Tao — who first competed in the Mathematical Olympiad at age 10 and won bronze, silver, and gold medals in 1986, 1987, and 1988 respectively, making him the youngest triple-medallist in Olympiad history. Now a Fields Medal laureate and professor at UCLA, he has built a reputation as one of the most distinguished mathematicians of his generation…

(Article truncated at source; the above represents the complete translatable portion of the original text.)

---

原文來源： 查看原文