For most of the past half century, mathematicians had a comfortable answer to the question of whether computers would ever do real mathematics. Machines could check cases, crunch numbers, and grind through searches, the thinking went, but the creative part, finding the idea that cracks a problem that has stumped people for decades, would stay human for a long time to come. That answer is now in trouble. In about two years, AI systems went from a silver-medal score at the International Mathematical Olympiad to gold, then to settling a string of problems left behind by the famously prolific Paul Erdős, in May 2026 to disproving one of Erdős’s favorite conjectures, a question he first asked in 1946, and in September 2026 to the biggest claim yet: a machine-checked solution, still under formal review, to the Navier–Stokes problem, one of mathematics’ $1 million Millennium Prize Problems. Many mathematicians are impressed. Many are also uneasy. And some of the most candid among them admit something harder to say out loud: they were too sure this could not happen yet.
This is a story about machines getting better at math, and about a field that assumed its deepest work was safely out of reach.
A field that had been here before
Mathematicians have argued about computer proofs for 50 years. In 1976, Kenneth Appel and Wolfgang Haken at the University of Illinois announced a proof of the four color theorem, the claim that any flat map can be colored with just four colors so that no two neighboring regions share one. Their argument reduced the problem to checking well over a thousand special configurations, a job that took more than a thousand hours of computer time. The department was proud enough to change its postage meter to stamp “Four Colors Suffice” on outgoing mail.
Many mathematicians were not celebrating. No human could check every case by hand, and to some that meant it was not really a proof at all. In 1979 the philosopher Thomas Tymoczko argued that the result changed what “proof” meant, because a proof was supposed to be something a person could survey and understand from start to finish. The debate eased only slowly, as later teams simplified the argument and, in 2005, Georges Gonthier checked the whole thing in the Coq proof assistant, a program that verifies every logical step.
Other milestones followed the same pattern. In 1996, a program called EQP, written by William McCune at Argonne National Laboratory, proved the Robbins conjecture, a question in abstract algebra that had been open since the 1930s. It was an early case of a machine finding a proof that had eluded people. In 1998, Thomas Hales announced a proof of the Kepler conjecture, the 400-year-old claim that the familiar grocer’s pyramid is the densest way to stack oranges. The proof leaned so heavily on computer calculations that the referees for the Annals of Mathematics reportedly said they were 99 percent certain it was correct, but could not be fully sure. Hales responded by leading a project called Flyspeck that formally verified the proof in the proof assistants HOL Light and Isabelle, finishing in 2014.
Each time, the lesson was reassuring: a human had the idea, and the machine did the bookkeeping. That is the lesson that has started to crack.
How fast the ground moved
The first serious sign came from Google DeepMind. In December 2023, its FunSearch system, which pairs a language model with an automated evaluator, found larger examples of “cap sets,” a puzzle in combinatorics, than mathematicians had found before. A month later, its AlphaGeometry system solved 25 of 30 olympiad geometry problems, close to the level of an average gold medalist. In July 2024, AlphaProof and AlphaGeometry 2 together scored 28 of 42 points on that year’s olympiad problems, one point short of gold.
The Fields Medalist Tim Gowers helped grade those answers. He called one construction the program found “well beyond what I thought was state of the art,” while noting that it took more than 60 hours on some problems and that humans had first translated the questions into formal language. Asked whether mathematicians were close to becoming redundant, he guessed “we’re still a breakthrough or two short of that.”
A breakthrough or two arrived quickly. In November 2024, the research group Epoch AI released FrontierMath, a set of hard, unpublished problems written by expert mathematicians. Terence Tao, the UCLA mathematician often called the best of his generation, predicted the hardest of them would “resist AIs for several years at least.” The best models at the time solved under 2 percent. Six weeks later, OpenAI announced that its o3 model had scored about 25 percent on the benchmark. (It later emerged that OpenAI had funded FrontierMath and had access to many of its problems, which drew criticism over transparency.)
Then came gold. In July 2025, an advanced version of Google’s Gemini Deep Think earned 35 of 42 points at the International Mathematical Olympiad, a score certified by the competition’s own coordinators, and wrote its proofs in plain English rather than formal code. OpenAI said an experimental model of its own reached the same score, graded by former medalists rather than by the IMO itself. Three years earlier, the AI researcher Paul Christiano had put the chance of an AI winning IMO gold by 2025 at under 8 percent in a public bet with Eliezer Yudkowsky, who put it at 16 percent or more. It happened anyway.
If you want to know why progress jumped so abruptly in this period, much of it came from letting models “think” far longer before answering, a shift we covered in our explainer on test-time compute.
The Erdős problems: what AI did, and what it didn’t
Paul Erdős, who died in 1996, left behind more than a thousand problems, many with small cash prizes attached. The mathematician Thomas Bloom keeps a catalog of them at erdosproblems.com, and in 2025 they became the proving ground for AI in mathematics. They also became a lesson in how easily AI results can be overstated, in both directions.
Found, not solved. In October 2025, an OpenAI vice president posted that GPT-5 had “found solutions to 10 (!) previously unsolved Erdős problems.” Bloom quickly called it “a dramatic misrepresentation.” The problems were listed as open only because he had not seen a solution. “GPT-5 found references, which solved these problems, that I personally was unaware of,” he wrote. Google DeepMind’s chief executive, Demis Hassabis, replied, “this is embarrassing.” The post was deleted. Finding forgotten papers is useful, but it is not new mathematics.
Solved, with an asterisk. In January 2026, a pairing of OpenAI’s GPT-5.2 Pro and Harmonic’s Aristotle, a system that writes proofs in the Lean proof assistant, produced a machine-checked solution to Erdős problem #728, a question about divisibility. Tao described it as solved “more or less autonomously by AI (after some feedback from an initial attempt).” Within days, though, mathematicians noticed that the method closely resembled a 2014 paper by Carl Pomerance, who then showed his own techniques also settled the problem. The AI’s proof was still the first to address the problem directly, partly because the original problem had been stated loosely. Tao and others now keep a public wiki that sorts each AI contribution by type, from full solutions to partial results to literature finds.
Solved, no asterisk. On May 20, 2026, OpenAI announced that an unreleased internal model had disproved Erdős’s unit distance conjecture. The question asks how many pairs of points among a set of points in the plane can be exactly one unit apart. Erdős believed a simple grid was essentially the best possible arrangement and offered a prize for settling the question. The model found a far better construction using deep tools from algebraic number theory. Nine outside mathematicians, including Gowers, Bloom, Noga Alon, and Daniel Litt, checked the argument and published a companion paper explaining it. Gowers wrote that if a human had submitted the paper to the Annals of Mathematics, he “would have recommended acceptance without any hesitation,” adding, “No previous AI-generated proof has come close to that.”
“I did not expect this”
What stands out in the unit distance paper is how openly the experts describe being caught off guard. A month before the result, Bloom had put the problem on a tongue-in-cheek “Top 10 Erdős Problems” list, partly to push back on the idea that the problems AI had been solving were trivial. He expected AI to make progress on some of them eventually. “I did not expect this to happen just one month later!” he wrote.
Gowers first heard about the result on a video call and misunderstood it, thinking the model had proved the conjecture rather than disproved it. “I spent the evening adjusting my world view: if AI could come up with a proof like that, then maybe it would be all over for mathematicians very soon,” he wrote. Learning it was a counterexample “came as a big relief.” He also admitted that he had never thought to try disproving the conjecture: “Somehow I was too convinced by a story that turned out to be incorrect.” That, in a sentence, is the hubris problem. The experts were not careless. They shared a belief, and it hid a whole line of attack from them.
Litt, a mathematician at the University of Toronto, had already said something similar in February 2026 about First Proof, an experiment in which eleven leading mathematicians posed ten unpublished research-level problems from their own work. He had expected current models to solve two or three. By most counts, combining every attempt, six to eight were solved, though some with human help and some by models not available to the public. “I think I was not correctly calibrated as to the capabilities of existing models,” he wrote. In the unit distance paper, he went further, suggesting the problem may have stayed open partly because experts anchored on the wrong belief or lacked ideas from neighboring fields. “These explanations, if correct, should cause us some discomfort,” he wrote.
Tao, to his credit, saw much of this coming. In a 2023 essay he predicted that “2026-level AI, when used properly, will be a trustworthy co-author in mathematical research.” In the same essay he warned that the profession was “largely unprepared” for what that would mean for journals, students, and credit. Both halves of that forecast now look right.
September 2026: AI takes on a Millennium Prize Problem
Four months after the unit distance result, the stakes jumped. On September 8, 2026, OpenAI announced that an internal AI system had resolved the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems the Clay Mathematics Institute named in 2000, each carrying a $1 million prize. Only one of the seven, the Poincaré conjecture, had been solved before. The Navier–Stokes equations describe how water, air, and other fluids move, and are used in weather forecasting and aircraft design. The open question, unresolved for roughly 90 years by OpenAI’s count, was whether a fluid that starts out smooth can ever “blow up,” with its speed racing to infinity in a finite time.
The answer, the system found, is yes. OpenAI ran an unreleased model it describes as significantly more capable than GPT-6 Astra as a swarm of roughly 10,000 coordinating AI agents. After about 88 hours, on September 5, they produced a proof that a fluid at rest, pushed by a smooth external force, can form a singularity: a vortex that spirals inward and stretches out “like spaghetti,” spinning faster and faster while its total energy stays finite. GPT-6 Astra then wrote a complete formal version in the Lean proof assistant in another 17 hours. The compute alone cost millions of dollars. Quanta Magazine judged that, if the result holds up, it is “by a significant margin, the most important mathematical proof to have been arrived at by an artificial-intelligence model to date.”
Experts were quick to call it a landmark. “It’s one of the guiding problems for the field. It is a huge deal to know the answer,” Dallas Albritton of the University of Wisconsin–Madison told Science News. “I was thrilled that the problem was solved,” said Charles Fefferman of Princeton, who wrote the Clay Institute’s official statement of the problem. Three days after the announcement, the Clay Institute itself said the problem “has apparently been settled.”
It also fits the pattern of experts being caught off guard, twice over. The first surprise was the math itself. “Ten years ago, nobody believed there was a singularity for Navier-Stokes,” the Madrid mathematician Diego Córdoba told Quanta. The second was who got there. Córdoba and his former student Luis Martínez-Zoroa had built the method both AI-assisted teams leaned on, and Fefferman called them the heroes of the story. Yet the finishing step came from machines, in a matter of days. The NYU mathematician Tristan Buckmaster, who with Levent Alpöge of Anthropic had used AI to reach a closely related result just hours earlier, said his team’s results marked a “Deep Blue-Kasparov moment.” The mathematician Gonzalo Cao-Labora told Scientific American, “We are really amazed with how [the technology] has evolved in the last year—so we don’t know how it will look in one year. It’s really a wake-up call to the community.”
The fine print. The result is a claim under review, not an awarded prize. Clay’s rules require a solution to be published and to survive at least two years of scrutiny, and OpenAI has said it does not intend to claim the money. Because the Lean code compiles, “the community seems to have the consensus that it is correct,” Brown University’s Javier Gómez-Serrano told NPR, but the 166-page write-up is hard going. “So far it’s been very difficult to really extract any human understanding from this new AI proof,” said Oxford’s James Maynard. Some experts also argue the proof wins on a technicality, since the official problem allows the kind of external force the AI used. “The Clay problem is settled, but the main problem for the Navier-Stokes equations is not,” said Luis Silvestre of the University of Chicago. And credit is contested: Buckmaster has suggested OpenAI may have benefited from his and Alpöge’s work, which OpenAI denies.
Navier–Stokes was not September’s only result. In the same month, a pre-release GPT-6 Astra proved the Erdős–Sós conjecture, a graph theory problem open since the early 1960s, with what the Oxford mathematicians Oliver Riordan and Alex Scott called “a very ingenious and surprising argument.” Taken together, the month made the old assumption, that the deepest problems were safely out of reach, look badly dated.
Why it stings: four kinds of unease
Credit. Who gets credit when a model writes the key idea? Mathematics runs on citation, and the unit distance argument rests on decades of human work in number theory that the AI’s write-up did not properly cite. Harvard’s Melanie Matchett Wood pointed out that a human who skipped those citations would be presumed unaware of them, while an AI is “in some sense ‘familiar’ with all the previous work.” She argued that “Mathematicians need to think about what best practices and proper citation is in these kind of situations.” Victor Wang, another co-author, asked whether mathematicians posting papers freely online “implicitly want it to be freely available to AI as well.”
Understanding. A proof is supposed to explain why something is true, not just certify that it is. Litt noted that many correct AI solutions in the First Proof experiment were “very poorly written,” and that “their correctness is exceedingly difficult to check because of this.” Human authors, he observed, often invent new terms and objects that clarify what is going on, while “the models usually just plow ahead.” If machines produce results that no one fully understands, mathematics risks becoming a list of verified facts rather than a body of insight.
What counts as a proof. This is the four color debate again, sharpened. A proof written in Lean or Isabelle can be checked mechanically down to the axioms, which is why formal verification has become central to the field. Kevin Buzzard of Imperial College London is leading a multi-year project to formalize Fermat’s Last Theorem in Lean, and Tao helped verify a major 2023 result he co-authored in Lean in about three weeks. But most AI output is ordinary prose, and prose can be confidently wrong. Wood warned that “it will be easier for AI to convince humans it has a proof than to come up with a correct mathematical argument,” adding, “we as mathematicians are not sufficiently prepared for this.” Litt described First Proof submissions that included “an enormous amount of garbage,” including incorrect solutions that claimed to be formalized in Lean.
Replacement. Then there is the fear Gowers named in 2024 and felt in 2026. For many mathematicians, the point of the job is the experience of understanding something new. If a machine can do the finding, what is left? The same question is rippling through other professions, as we described in our look at the quiet AI job shift, where tasks moved to machines faster than judgment did.
The case for a better calculator
There is another way to read all of this. Calculators did not end arithmetic, and computer algebra systems did not end calculus. On this view, AI is the next tool in that line: a tireless assistant that searches the literature, tests ideas, and checks routine steps, freeing humans for the parts that matter most.
There is evidence for that reading too. In First Proof, the computational mathematician Tamara Kolda reported that the best AI answer to her question was better than her own, with “an insight that was obvious in hindsight but that I had not seen yet myself,” and then found the key idea already existed in a 2016 paper. The First Proof organizers wrote that AI systems “are undoubtedly already at a level where they are useful tools,” and stressed that the hardest parts of research, choosing questions and building new theories, were outside what they tested. Even in the unit distance case, Bloom emphasized that the AI’s proof “was significantly improved” by people, and that “the human still plays a vital role in discussing, digesting, and improving this proof, and exploring its consequences.”
Gowers, too, offered a measured view. He suggested AI may have a particular edge on problems that reward encyclopedic knowledge and patience over deep new theory, while cautioning that he did not expect progress to plateau. So far, AI’s successes have come on well-posed problems. Inventing the definitions and frameworks that make new questions possible remains largely untested.
The bottom line
Mathematics has absorbed computer proofs before, and it will absorb this. What feels different this time is the timing. Many of the world’s best mathematicians believed that machine-made breakthroughs on hard open problems were years or decades off, and several of them now say plainly that they misjudged it. Then, in September 2026, an AI system produced a machine-checked answer to a $1 million Millennium Prize Problem, a result still under review but already hailed by experts as a landmark. That kind of honesty is the field at its best. The lesson of the last two years may be less about what AI can do than about how certain experts should be about what it cannot. Mathematicians still choose the questions, judge what matters, and turn raw results into understanding. Whether they stay in control of discovery will depend less on the machines than on how quickly the profession decides what it wants credit, proof, and understanding to mean.
Read more about machines and mathematical truth
The Proof in the Code: How a Truth Machine Is Transforming Math and AI — Quanta writer Kevin Hartnett’s 2026 history of the Lean proof assistant, the mathematicians who built it, and why machine-checked proofs now sit at the center of AI math.
The Creativity Code: Art and Innovation in the Age of AI — Oxford mathematician Marcus du Sautoy asks whether machines can be truly creative, in art and music and in his own field of mathematics.