For most of computing history, mathematics has been the thing machines were good at in a narrow, mechanical sense. They could crunch numbers, solve differential equations, run simulations. But actually proving things, constructing logical arguments that establish mathematical truth from first principles, that was supposed to stay in human hands. The recent behavior of several AI systems is making that assumption look shaky.
We're not talking about calculators getting faster. A handful of AI tools are now producing formal proofs of theorems that are genuinely nontrivial, statements that professional mathematicians find interesting and difficult. The conversation inside research departments has shifted from cautious curiosity to something closer to urgency.
What "Proving a Theorem" Actually Means
It helps to be precise here, because the word "proof" gets used loosely. When a high school student writes out a geometric proof, they're following a template. When a research mathematician proves something new, they're constructing a logical chain from axioms to conclusion that has never existed before, often after years of failed attempts. The difficulty isn't arithmetic. It's insight, the ability to see which path through an infinite space of possible logical steps actually leads somewhere.
Formal proofs are a stricter version still. In formal mathematics, every single inference step must be mechanically checkable by a computer program. Tools like Lean, Coq, and Isabelle implement this. Writing a formal proof is painstaking work; translating even a moderately complex result into Lean can take weeks. But once done, the proof is essentially guaranteed correct. No peer reviewer missed a subtle error. The machine checked everything.
This is the arena where AI is starting to show up in surprising ways.
AlphaProof and the IMO Moment
In July 2024, DeepMind announced that a system called AlphaProof, combined with a geometry-focused model called AlphaGeometry 2, had solved four out of six problems from the International Mathematical Olympiad. Two of those problems were rated as the hardest on the exam. The system scored 28 out of 42 points, which would have placed it at a silver medal level among human competitors.
The IMO is not trivial. It selects the best young mathematical minds from over 100 countries, and the problems are specifically designed to require genuine creative insight, not just computation. Getting four of them right is not a trick. It reflects something real about the system's ability to construct valid logical arguments under constraint.
AlphaProof works by translating problems into Lean 4, then using a reinforcement learning loop to search for proofs. The system essentially teaches itself by attempting millions of proof strategies and learning which approaches tend to succeed. It's a different paradigm from just training on text. The feedback signal is unambiguous: either the proof checker accepts the argument or it doesn't.
Terence Tao's Reaction and the Formalization Question
One of the more telling indicators of how seriously mathematicians are taking this comes from Terence Tao, the UCLA mathematician who is widely considered one of the best in the world. Tao has been publicly experimenting with Lean and AI-assisted proof tools, and his commentary on the field has been characteristically precise.
His take is not dismissive, but it's not uncritical either. Tao has pointed out that current AI systems tend to be brittle in ways that differ from human mathematicians. A human who understands a proof can usually explain it, adapt it, apply pieces of it to new situations. AI systems producing Lean proofs sometimes find arguments that are technically valid but essentially unreadable, chains of steps that verify correctly but give no intuition for why the result is true.
That distinction matters enormously to working mathematicians. A proof that no one understands is less useful than it sounds. Mathematics isn't just about establishing that something is true; it's about building a body of knowledge where ideas connect to each other. A proof that's a black box contributes less to that project.
Still, Tao has expressed optimism that AI tools could dramatically accelerate the formalization of existing mathematics. Vast amounts of published mathematical knowledge exist only in informal prose, not in any machine-checkable form. If AI can help translate that body of work into formal systems, it creates an infrastructure that future researchers, human or machine, can build on more reliably.
Beyond Olympiad Problems: Research-Level Mathematics
The IMO results got attention partly because they're legible to a general audience. But some researchers are more interested in what's happening at the actual research frontier.
In 2023, a team at Google DeepMind used an AI system to discover new solutions to the cap set problem, a combinatorics question that has attracted serious mathematical attention. The system found constructions that beat the best known human results. This wasn't a proof in the formal sense, but it was a genuine mathematical discovery.
More recently, work on AI systems interacting with proof assistants has shown that large language models can serve as useful collaborators even when they can't produce complete proofs on their own. A mathematician working in Lean can use an LLM to suggest next steps, fill in routine lemmas, or identify which existing theorems in a library are relevant to the current goal. The human still directs the overall argument, but the drudge work gets automated.
This workflow is already happening in practice. The Mathlib library for Lean 4, a community-maintained repository of formalized mathematics, has seen increased contributions from researchers using AI assistance. The pace of formalization is accelerating, even if no single AI is autonomously proving major open conjectures.
The Credit Problem
Mathematics has a strong culture around attribution. Who proved what, and when, matters deeply. Careers are built on theorems. The Fields Medal, the closest thing math has to a Nobel Prize, goes to individuals for specific contributions. When an AI system plays a significant role in finding a proof, the question of credit becomes genuinely uncomfortable.
If a mathematician uses an AI tool to handle 60 percent of the inferential steps in a proof, who proved it? The question isn't entirely new; mathematicians have always used computers for computation, and some major results like the four color theorem rely on computer-checked case analysis. But the scale and nature of AI involvement is different. An AI that suggests entire proof strategies, not just crunches cases, is closer to a collaborator than a calculator.
No consensus exists yet. Some researchers argue that the human who poses the right question, interprets the AI's output, and takes responsibility for the result deserves full credit. Others think journals need to develop disclosure standards, similar to what's emerging in other scientific fields around AI use. The mathematical community moves slowly on institutional questions, but this one is going to force a resolution.
What This Means for the Future of Mathematical Discovery
There's a reasonable version of the future where AI tools do for mathematics what search engines did for research generally. They lower the cost of certain operations dramatically, making some things routine that used to be hard, while pushing human effort toward the genuinely novel parts of the problem.
Formal verification in particular could become standard. Right now, submitting a formal Lean proof alongside a paper is unusual. In ten years, for certain subfields, it might be expected. If AI makes formalization cheap enough, the incentive structure shifts. Peer review becomes faster and more reliable. Errors that currently survive in the literature for years get caught immediately.
The deeper question is whether AI will eventually produce truly original mathematical insight, not just verify or formalize what humans have sketched, but actually identify new structures, new connections, new conjectures worth pursuing. The IMO results suggest the systems can construct creative arguments under constraints. Whether that generalizes to the open-ended, unstructured work of research mathematics is genuinely unknown.
What's clear is that the tools are good enough now to change daily mathematical practice, and they're improving fast. Mathematicians who engage with them seriously are finding real productivity gains. Those who ignore them entirely may find themselves at a disadvantage as the field's infrastructure shifts around them. That's a situation that should feel familiar to anyone who watched what happened to other knowledge-intensive fields when powerful software tools arrived. The math is harder, but the dynamic is recognizable.
