수학을 대신하는 AI, '수학자의 존재 이유'를 묻다

AI Magazine Feature What it Means to Be a Mathematician When AI Does the Math Researchers debate motivation, purpose, and the field’s future Benjamin Skuse 25 Jun 2026 10 min read Terence Tao of the University of California, Los Angele s , believes AI could usher in an era of “Big Mathematics,” where humans and machines work together on complex problems. Peter Adams DarkBlue1 In the mid-noughties, when music by the Killers and Franz Ferdinand blared out of every pub and nightclub I passed, I spent my days and nights struggling through a Ph.D. in applied mathematics . My research focused on simulating how special light waves interact in liquid crystals and using simple equations to approximate and understand those interactions. When I look back at my thesis now, liquid crystal technology is old hat, and I imagine my work could be completed with AI assistance in a matter of days—maybe hours. But the same cannot be said for the work of the pure mathematics Ph.D. students with whom I shared a cramped office at the University of Edinburgh. At the time, I felt sorry for these colleagues, who day after day sat at their desks, seemingly tearing their hair out and making no progress. (Though I was struggling too, I was at least always making some headway.) When we finished and went our separate ways, some hadn’t even published a paper. Now, in hindsight, I finally understand why they toiled for years on abstract mathematical problems that only a handful of people in the world care about. It wasn’t arrogance, as I thought at the time; they weren’t trying to prove their superior intelligence by being the first to solve a seemingly intractable mathematical problem. It wasn’t even a form of masochism (which was my second guess)—penance for some imagined inadequacy. I realized they derived joy, satisfaction, and meaning from the long journey toward understanding. Gluekit “Sometimes, understanding just strikes you as being very beautiful.” —Jeremy Avigad, Carnegie Mellon University “Sometimes, understanding just strikes you as being very beautiful. Sometimes it’s a feeling of accomplishment, like completing a marathon,” muses Carnegie Mellon University mathematician Jeremy Avigad . “But it’s not quite either of those: It’s just a wonderful feeling when you’ve been thinking long and hard about something complex, difficult, and then—all of a sudden—it just comes together.” This feeling has driven mathematicians throughout history. Likewise, the way mathematicians pursue that feeling has changed little over the centuries. They notice or imagine links, patterns, or properties in numbers, shapes, or logical structures. From this, they write conjectures—unproven statements of their speculation. They or other mathematicians then use logical reasoning and the tools of mathematics in often creative ways to prove or disprove those conjectures. Finally, yet other mathematicians verify (or challenge) the proofs. Invariably, this process requires a whole heap of thinking time. “I went to a pure maths camp with classes where we would sit with hard maths problems for half an hour and no one would say anything—everyone was just thinking,” says Krystal Maughan , a mathematician and computer scientist about to get her Ph.D. at the University of Vermont. “But then we would work together and kind of tease out the problem.” This is the age-old joy of math in action. But today’s AI systems are starting to make inroads into bypassing this slow, deliberative process. Taking this trend to its logical conclusion, what happens if AI makes the mathematician’s struggle completely unnecessary? Might AI even sideline humanity completely? AI’s Growing Role in Mathematics For decades, computation has accelerated mathematical progress. This began 50 years ago, when mathematicians used a computer to prove the four-color theorem , which asks whether any map can be colored using no more than four colors, with no adjacent regions sharing the same color. The answer is yes, and the computer proved it, controversially, by checking 1,936 cases in a way no human could realistically verify. Yet throughout this computational era, even in proofs relying on massive computational resources, the role of the human mathematician has remained central. Humans propose conjectures, guided by intuition. They devise strategies to prove them, guided by creativity and experience. And humans verify whether those proofs are correct. Now AI is challenging the status quo . In just a few years, large language models (LLMs) have evolved from “ stochastic parrots ,” capable of little more than regurgitating basic mathematics scraped from the internet, into advanced mathematical reasoning machines. Last summer, systems from Google DeepMind and OpenAI reached a level equivalent to the world’s most mathematically gifted high school students, achieving gold-medal status at the International Mathematical Olympiad . In this annual competition, contestants must solve six notoriously difficult problems from various areas of mathematics. Earlier this year, Google DeepMind’s experimental AI system Aletheia achieved an even more significant milestone when it autonomously produced publishable Ph.D.-level research results. While the work itself is obscure mathematically—calculating structure constants in arithmetic geometry—the significance lies in the complex reasoning it displayed in tackling an unsolved mathematical problem. And more recently, a new general-purpose AI system from OpenAI disproved an important conjecture in combinatorial geometry . This result would have been worthy of publication in a major mathematics journal if humans had been the authors, and top mathematicians hailed the feat as a milestone for AI in mathematics, demonstrating independent, original, and sophisticated thinking. Another shift has come from combining LLMs with mathematical tools known as proof assistants, which have been around for more than a decade. These systems—such as Isabelle , Lean , and Rocq —are specialized programming languages that check mathematical proofs step-by-step, verifying their logical correctness. Traditionally, mathematicians have had to translate their theorems and proofs into this machine-readable format by hand, a laborious process known as formalization. Now, LLMs are starting to remove this bottleneck, automating the translation of 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 prime numbers appears very different when formalized in Lean, a proof assistant. Human mathematicians routinely skip steps and rely on shared understanding; formalization makes every assumption and inference explicit so a computer can verify the proof. HUMAN PROOF We want to show that for every natural number n , there’s a prime p that is at least n . Consider the smallest prime factor of n ! + 1. Call it p . It is obviously prime. To show p is at least n , assume, for contradiction, that it is not. p then clearly divides n !, so it also divides ( n ! + 1) − n ! = 1. But this is impossible: p is prime, and 1 has no prime divisors. So p is at least n . LEAN PROOF /- Euclid’s theorem on the **infinitude of primes**. Here given in the form: for every `n`, there exists a prime number `p ≥ n`. -/ theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p := 1 let p := minFac (n ! + 1 ) have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _ 2 have pp : Prime p := minFac_prime f1 have np : n ≤ p := le_of_not_ge fun h => have h 1 : p ∣ n ! := dvd_factorial (minFac_pos _) h 3 have h 2 : p ∣ 1 := (Nat.dvd_add_iff_right h 1 ). 2 (minFac_dvd _) pp.not_dvd_one h 2 ⟨p, np, pp⟩ ❶ Definitions must be explicit. The proof formally defines p as the smallest prime factor of n ! + 1 before it can use that quantity. ❷ Formal proofs build on earlier formal proofs. Here Lean invokes a previously verified theorem showing that p is prime. ❸ Hidden logical st