{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiedltklpfwi6u3sbn4v5sucjllrq77v6opklvp3siyjlbug3bp3ry",
    "uri": "at://did:plc:k5pd62odhosxknrvmwrqfjn6/app.bsky.feed.post/3mp4s5vcljem2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreibgwvphi3luy7eyswubgqvtuy6agrdiowtht2uflt3u7ahbdsq3su"
    },
    "mimeType": "image/jpeg",
    "size": 129984
  },
  "path": "/ai-in-mathematics",
  "publishedAt": "2026-06-25T13:00:01.000Z",
  "site": "https://spectrum.ieee.org",
  "tags": [
    "Mathematics",
    "Large-language-models",
    "Llms",
    "Stem-education",
    "Google-deepmind",
    "Openai",
    "Jeremy Avigad",
    "Krystal Maughan",
    "prove the four-color theorem",
    "challenging the status quo",
    "stochastic parrots",
    "Google DeepMind and OpenAI",
    "International Mathematical Olympiad",
    "autonomously produced publishable Ph.D.-level research",
    "disproved an important conjecture",
    "in combinatorial geometry",
    "Isabelle",
    "Lean",
    "Rocq",
    "Math, Inc.",
    "Gauss",
    "Maryna Viazovska",
    "Fields Medal",
    "human mathematicians",
    "8-dimensional sphere-packing problem",
    "autonomously formalized",
    "24-dimensional case",
    "12th Heidelberg Laureate Forum",
    "Yang-Hui He",
    "Trill White",
    "Jessica Randall",
    "Millennium Prize Problems",
    "Fields Medalist",
    "Akshay Venkatesh",
    "Fields Medal Symposium",
    "Maia Fraser",
    "Terence Tao",
    "youngest winner",
    "working on problems",
    "writing essays",
    "organizing workshops",
    "debating in journals",
    "community groups",
    "guidelines"
  ],
  "textContent": "\n\n\n\n**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.\n\nBut 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.\n\nNow, 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.\n\n###\n\n\n\n\n“Sometimes, understanding just strikes you as being very beautiful.” **—Jeremy Avigad, Carnegie Mellon University**\n\n###\n\n\n\n\n“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.”\n\nThis 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.\n\nInvariably, 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.”\n\nThis 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?\n\n## AI’s Growing Role in Mathematics\n\n\nFor 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.\n\nYet 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.\n\nNow 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.\n\nLast 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.\n\nEarlier 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.\n\nAnother 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.\n\n### From Human Proof to Formal Proof\n\n\n\n\nEuclid’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.\n\n###\n\n\n\n\n#### **HUMAN PROOF**\n\nWe want to show that for every natural number _n_ , there’s a prime _p_ that is at least _n_.\nConsider the smallest prime factor of _n_! + 1. Call it _p_. It is obviously prime.\nTo show _p_ is at least _n_ , assume, for contradiction, that it is not.\n_p_ then clearly divides _n_!, so it also divides (_n_! + 1) − _n_! = 1.\nBut this is impossible: _p_ is prime, and 1 has no prime divisors.\nSo _p_ is at least _n_.\n\n#### **LEAN PROOF**\n\n/- Euclid’s theorem on the **infinitude of primes**.\nHere given in the form: for every `n`, there exists a prime number `p ≥ n`. -/\ntheorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=\n**1** let p := minFac (n ! + 1)\nhave f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _\n**2** have pp : Prime p := minFac_prime f1\nhave np : n ≤ p :=\nle_of_not_ge fun h =>\nhave h1 : p ∣ n ! := dvd_factorial (minFac_pos _) h\n**3** have h2 : p ∣ 1 := (Nat.dvd_add_iff_right h1).2 (minFac_dvd _)\npp.not_dvd_one h2\n⟨p, np, pp⟩\n\n###\n\n\n\n\n❶ Definitions must be explicit. The proof formally defines _p_ as the smallest prime factor of _n_! + 1 before it can use that quantity.\n\n❷ Formal proofs build on earlier formal proofs. Here Lean invokes a previously verified theorem showing that _p_ is prime.\n\n❸ Hidden logical steps become explicit. A human mathematician can write that _p_ “clearly” divides 1. Lean requires the proof to invoke a formal theorem about divisibility and show exactly why that conclusion follows.\n\n###\n\n\n\n\nVersions of such systems, sometimes called reasoning agents, are becoming highly sophisticated. In February, for example, the AI company Math, Inc. used its aspirationally named reasoning agent Gauss to formalize a proof that had earned the mathematician Maryna Viazovska, of EPFL, in Switzerland, a Fields Medal in 2022. Gauss first helped human mathematicians complete the formalization of Viazovska’s solution to the 8-dimensional sphere-packing problem in a matter of days, and then autonomously formalized the more complicated 24-dimensional case in just two weeks.\n\nSuch achievements suggest that AI is already capable of handling some mathematical tasks long considered uniquely human. As the technology advances, more of the day-to-day work of human mathematicians is likely to become fair game for AI.\n\n## Mathematicians Debate AI’s Role in Discovery\n\n###\n\n\n\n\nHuman mathematicians could become “priests to oracles.” **—Yang-Hui He, London Institute for Mathematical Sciences**\n\n###\n\n\n\n\nIn September 2025, I attended the 12th Heidelberg Laureate Forum—an annual conference that brings hundreds of young mathematicians and computer scientists together with their intellectual idols. AI dominated the conversation and, from the get-go, tension was in the air.\n\nSpeakers described a future in which superhuman AI mathematicians transcend human knowledge and capabilities: forming conjectures, searching solution spaces, proving conjectures, and finally verifying the proofs and generalizing the results, all without human involvement. If this future comes to pass, Yang-Hui He of the London Institute for Mathematical Sciences memorably declared, human mathematicians could become “priests to oracles.”\n\nWhile such startling predictions were being voiced on stage, my gaze was drawn to the audience. Frowning, fidgeting, and exchanging furtive glances—the crowd’s unease was palpable. Trill White, a student at Australia’s Deakin University, later recalled sitting in that hall and thinking: “ ‘That’s devastating. What will people have to contribute to mathematics? Will it become something that no one understands?’ I did get a sense that this is going to change everything.”\n\n###\n\n\n\n\n“We certainly started realizing AI has the potential to replace us.” **—Jessica Randall, Google Developer Groups**\n\n###\n\n\n\n\nJessica Randall, a South African mathematician for Google Developer Groups, says she sensed a collective existential dread rising among the young mathematicians. “I could feel everyone was worried, because they hadn’t thought that far ahead,” she says. “It was like a big bombshell that hit us, and we certainly started realizing AI has the potential to replace us.”\n\nSome established mathematicians, including He, seem comfortable with AI taking on tasks that are currently the preserve of human mathematicians. That’s because they just want to know the answers to the biggest questions in mathematics—such as the six remaining Millennium Prize Problems—even if AI does it all. “A lot of mathematicians are pragmatic and just want to understand. They would sell their soul for the solution to a problem,” jokes Avigad. “Whatever it takes, right?”\n\nBut this “just want to know” camp is by no means the only faction: Most mathematicians do not hope or expect AI to replace them entirely. Instead, two broad alternatives are emerging. The first is a human-centric aspiration that prioritizes human understanding of mathematics and treats AI as a tool, much like a calculator. The second is a collaborative “teamwork makes the dream work” vision, where humans and AI work together to tackle problems neither could solve alone.\n\n## The Human Role in Mathematics\n\n###\n\n\n\n\nNumbers are “a way of bringing us to agreement.” **—Akshay Venkatesh, Princeton University**\n\n###\n\n\n\n\nFields Medalist and Princeton mathematician Akshay Venkatesh has been thinking about this topic from the human-centric viewpoint for years. In 2022, he used his Fields Medal Symposium to implore the mathematics community to deeply consider what AI might mean for the practice of mathematics. At the time, the idea that AI could replace mathematicians seemed far-fetched. Now, he says, “we’re reaching the point where, for at least some tasks with abstract mathematical reasoning, computers are becoming competitive with humans.”\n\nFor Venkatesh, the question is not just what computers can do, but what mathematics is for. “Sometimes I think when we use numbers, it’s not so much that we are describing phenomena that are intrinsically numerical, but that we can all agree exactly what the numbers mean,” he says. “It’s a way of bringing us to agreement.”\n\n###\n\n\n\n\n###\n\n\n\n\nMathematician and machine learning expert Maia Fraser, of the University of Ottawa, shares this sentiment. She says the joy she derives from mathematics is something distinctly human that integrates the subconscious and conscious mind. She describes starting with an intuitive sense that a certain thing should be true and gradually bringing out something that she can express in a rigorous proof. Communicating and sharing these deep-born thoughts is “a form of collective intelligence that is something beautiful about the human spirit,” she says.\n\nBy these arguments, an AI proof of a mathematical conjecture that has stubbornly resisted human efforts would be useful only if comprehensible to humans. “That the statement can be proved by AI is already useful information,” concedes Fraser. “But then it’s still an open problem to come up with an elegant, beautiful human proof.” Even if no such proof exists, she says, searching for it “is still a valuable endeavor.”\n\n## AI and the Future of Mathematical Collaboration\n\nA more collaborative approach to AI in mathematics comes from Terence Tao, who first competed in the math Olympiad at the age of 10. In 1986, 1987, and 1988, he won bronze, silver, and gold medals, respectively, making him the youngest winner of each of the three medals in Olympiad history. Now a Fields Medalist and professor at the University of California, Los Angeles, he has earned a reputation as one of the most gifted mathematicians alive.\n\nUnlike some of his peers, Tao is neither dismissive of AI nor fearful. Instead, he sees it as the catalyst for a fundamental shift in the discipline—a transition toward what he calls “big mathematics.” He envisions a future of large-scale, decentralized collaborations between humans and machines, where complex mathematical tasks can be diced and sliced, with humans claiming the creative parts and AI doing the lion’s share of the technical grunt work.\n\n###\n\n\n\n\n### Three Futures for AI in Mathematics\n\n\n\n| AI as a tool| AI as a partner| AI as an oracle\n---|---|---|---\nRole of AI| Assistant| Collaborator| Autonomous researcher\nWhat matters most?| Human understanding| Shared discovery| Answers\n\nAlready, Tao is experimenting with this concept, working on problems alongside scores of online collaborators, some using AI tools. “A hundred years ago, almost every mathematics paper was single author,” he says. “But now I collaborate with people I’ve never met—and maybe in the future, I won’t even know if they are AI or real people.”\n\nThe key to Tao’s vision is uniquely mathematical: formalization. When a proof is translated into code and checked step-by-step by proof assistants, it removes any chance of human error or dishonesty. This approach changes how collaboration works, because trust is established through verification rather than reputation or rapport. An idea from an unknown researcher or even an amateur can be taken seriously if it has a formal proof.\n\n“If it wasn’t for this formal verification layer, opening projects up without any safeguards would just be a disaster,” adds Tao. “But in math, we can completely check and verify outputs, and this really filters out a lot of the rubbish.”\n\n## The Risks of AI in Mathematics\n\nFrom the young researchers at the Heidelberg Laureate Forum to some of the biggest names in the field, mathematicians all seem to agree on one point: AI has the potential to transform their discipline. But there’s far less consensus on what that transformation will mean in practice.\n\nSome worry about the accessibility of AI tools. Traditionally, mathematicians have required little more than intuition, training, and a pen and paper to advance their field. If this slow, deliberative process is no longer valued by society, and particularly by research funders, then mathematics could become an elitist activity, only practiced by select organizations that can afford to work with proprietary AI models.\n\nAnother concern is motivation. As AI systems take on more of the work, the incentive to engage deeply with difficult problems may weaken. Princeton’s Venkatesh says that the long human process of formulating and understanding a proof may be hard to justify, not just to funders, but even to mathematicians themselves. “There have been times where I’ve spent years thinking about something, and I’ve slowly struggled to understand it,” he says. “If your computer can do large chunks of that for you, will you have the motivation to spend that time?”\n\nThat concern extends to the next generation. If students can use AI to jump straight to answers, they most likely will. But every time they skip the struggle, they miss an opportunity to build the foundations of their own unique intuition. Over time, some worry, the next generation of mathematicians may suffer from a form of intellectual atrophy, unable to think outside the AI box that trained them.\n\nIn response to such fears, the mathematics community is taking action. Individuals are writing essays, organizing workshops, and debating in journals, while institutions and community groups are developing guidelines for how AI should be used in research and publication. Indeed, mathematicians are applying the same rigor and curiosity that they use every day to reckon with the challenges of AI. Taken together, these efforts reflect a broad effort to try to retain control over the direction of mathematics in the era of AI.\n\nSo, is AI sucking the soul out of math? In one way, it is doing the opposite. It is forcing mathematicians to confront deep questions about what mathematics is, why they have devoted their lives to it, and the purpose math serves in society. At the same time, though, it is reshaping the practice of mathematics in a way that may be difficult to reverse.\n\n“Mathematics makes me a better problem solver at normal problems, because it frames my mind to think in a very logical, rational way,” says Randall, who noted the existential dread at the Heidelberg Forum. “It helps with every aspect of my life.” As AI transforms mathematics, many researchers wonder whether future mathematicians will be able to say the same.",
  "title": "What it Means to Be a Mathematician When AI Does the Math"
}