Mathematical reasoning in AI

Mathematical reasoning in AI is the ability of computer systems to solve mathematical problems: carrying out multi-step calculations, proving theorems, and answering competition or research questions that require chains of logical inference. It is one of the oldest goals in artificial intelligence and one of its most closely watched proving grounds, because mathematics offers something most domains do not: answers that can be checked exactly, either against a known result or by a formal proof verifier.

The field runs on two lineages that are now converging. The symbolic tradition, which began with theorem-proving programs in the 1950s and continues in proof assistants such as Lean, Isabelle, and Rocq, represents mathematics in formal languages where every step is machine-checkable. The statistical tradition, dominant since large language models (LLMs) began solving word problems, treats mathematics as text and learns to produce solutions from data. Between 2022 and 2025 the second tradition advanced from roughly half marks on high-school competition problems ^[24] to gold-medal-standard performance at the International Mathematical Olympiad (IMO) ^[4], while hybrid systems such as AlphaProof brought the two lineages together ^[2].

2026 changed the shape of the subject. Between May and September, AI companies announced results in research mathematics rather than competition mathematics: a disproof of a conjecture of Paul Erdős on unit distances ^[43], a counterexample to the Jacobian conjecture ^[44][45], ten results in mathematics and theoretical computer science shipped with Lean certificates ^[34], a machine-checked formalization of Fermat's Last Theorem ^[60], and a contested claim on one of the Clay Millennium Prize Problems ^[57]. Machine-checkable certificates became the line that separates the claims a kernel can settle from the ones it cannot, and the mathematical community organized a formal response: the Leiden Declaration on Artificial Intelligence and Mathematics on 2 June 2026, endorsed by the International Mathematical Union ^[48], and a declaration signed by 25 Fields Medallists on 11 September 2026 ^[50][51]. The objection in both documents is not that the results are wrong. It concerns attribution, the absence of writeups, the transmission of ideas, and the training of students.

From the Logic Theorist to proof assistants

The first program deliberately built for automated reasoning was the Logic Theorist, completed in 1956 by Allen Newell, Herbert Simon, and Cliff Shaw at RAND. It proved 38 of the first 52 theorems in chapter two of Whitehead and Russell's Principia Mathematica, and for theorem 2.85 it found a proof more elegant than the original; Bertrand Russell is said to have responded with delight when shown it. The program introduced ideas that became foundations of symbolic AI: reasoning as search through a tree of possibilities, heuristics for pruning that search, and list processing that influenced Lisp ^[5].

Automated theorem proving developed from there into a mature subfield, and computers gradually entered mainstream mathematics. The 1976 proof of the four color theorem was the first major theorem verified with essential help from a computer program, and Georges Gonthier later produced a fully formal, machine-checked proof, described in his 2008 paper "Formal Proof: The Four-Color Theorem" ^[6]. Gonthier's work used Coq, an interactive proof assistant developed since 1984 and later renamed the Rocq Prover ^[7]. Alongside Rocq and Isabelle, the Lean proof assistant became the main gathering point for mathematicians interested in formalization. Its community library, mathlib, listed 288,065 theorems, 136,941 definitions and 772 contributors when its statistics page was read on September 13, 2026 ^[8].

These systems matter for AI because they turn proof checking into computation. A model can propose millions of candidate proof steps, and the kernel of a proof assistant will accept only the valid ones, providing exactly the kind of clean training and evaluation signal that machine learning thrives on.

Competition mathematics and research mathematics

Most public measurement of AI mathematics has used competition problems, and most of the 2026 claims are not competition problems. The distinction matters enough to state plainly.

A competition problem is short, self-contained, posed by a problem committee, known in advance to have a solution, and graded against a rubric inside a fixed time limit. The AIME gives 15 problems whose answers are integers from 0 to 999 ^[14]; the IMO gives six proof problems over two 4.5-hour sessions ^[29]. A research problem has none of those properties. Nobody knows whether it is true, nobody knows whether the tools to settle it exist, there is no rubric, and the work of deciding whether a claimed solution is correct falls on volunteer experts. The gold-medal results at IMO 2025, covered at AI gold-medal results at IMO 2025, are competition mathematics. The 2026 announcements described below are not the same kind of object, and a score on one does not transfer to the other.

In an essay based on his public lecture at the 2026 International Congress of Mathematicians, Terence Tao argued that most of the publicly available evidence about AI capability in research mathematics "has not been gathered under controlled scientific conditions" and is subject to reporting bias, "successes are announced and failures are not", with the number of attempts, the amount of human scaffolding, the compute expended, and the degree of contamination with prior literature frequently undisclosed ^[47]. Epoch AI later restated his four shortcomings and added a fifth: different models are not systematically compared on the same problems, so it is unclear when AI first became capable of a given result or which current models are strongest ^[42].

The shift shows up in the benchmarks themselves. MathArena, run by the SRI Lab at ETH Zurich and INSAIT, spent 2025 and early 2026 scoring models on each new contest as it happened. As of September 13, 2026 its site marks the entire competition program as deprecated, including the AIME, HMMT, BRUMO, SMT, CMIMC, Project Euler, USAMO, IMO, IMC, the Miklós Schweitzer competition, and the Putnam, while its active tracks are all built from recent arXiv papers ^[55].

The benchmark ladder

Progress in LLM mathematics has been measured against a ladder of benchmarks of increasing difficulty, each introduced roughly when the previous rung stopped discriminating between models.

GSM8K, introduced with OpenAI's paper on training verifiers, showed that 2021-era models struggled even with grade-school arithmetic word problems ^[10]. The MATH dataset collected 12,500 competition problems with full step-by-step solutions; its authors observed that accuracy remained low even for enormous models and that scaling alone looked insufficient ^[9]. Both were effectively solved within four years. The 500-problem MATH subset that OpenAI selected for its 2023 process-supervision work, now known as MATH-500, survives as a standard quick benchmark ^[12].

The AIME, a 15-question, three-hour invitational exam whose answers are integers from 0 to 999, became the de facto successor because each year's edition supplies fresh, contamination-free problems ^[14]. FrontierMath, commissioned by Epoch AI with support from OpenAI, went much further: its problems are unpublished, span number theory to algebraic geometry, and typically demand hours or days of effort from a research mathematician. When it launched in November 2024, leading models solved under 2% ^[3]. Its tiers 1-3 cover undergraduate through advanced graduate material, tier 4 is research-level, and a v2 release on June 12, 2026 addressed errors in 42% of the original problems, leaving 338 problems in total: 295 in tiers 1-3 and 43 in tier 4, of which twelve are public ^[17][61]. Scores on the corrected v2 tiers are not comparable with the v1 figures, so any FrontierMath number needs both a version and a date attached; the model-by-model results are tabulated at FrontierMath. Humanity's Last Exam plays a similar role across disciplines, with mathematics among its subjects ^[18][19].

Because static benchmarks leak into training data, evaluators increasingly test on material published after a model's release. MathArena now draws its live tracks from recent arXiv mathematics papers, which lets each monthly edition be refreshed and limits data contamination: ArXivMath draws research-level problems from recent papers, ArXivLean formalizes statements in Lean and asks for proofs, and BrokenArXiv deliberately plants plausible but false statements and rewards a model for refusing to prove them and for saying why they are false ^[55]. The ArXivLean authors reported in April 2026 that on the first, 41-problem March edition every system they ran, including Harmonic's Lean agent Aristotle, scored below 20% ^[56]. On the 46-problem June 2026 edition the leaderboard as of September 13, 2026 put Mistral Prover (Leanstral 1.5 paired with Moonshot AI's Kimi K3) at 82.61% plus or minus 10.95, GPT-6 Astra at 65.22%, GPT-5.6 Sol at 39.13%, and Claude Opus 5 at 32.61%, with rows flagged where a model was released after the problem set, so contamination cannot be ruled out ^[16]. Those two editions are separate problem sets, and the jump between them is not a measured improvement on a fixed benchmark.

FrontierMath Erdős

The most carefully budgeted public measurement of AI on research problems is Epoch AI's FrontierMath Erdős, announced on September 1, 2026 by Tom Adamczewski and Greg Burnham ^[40]. Thomas Bloom, the mathematician who maintains the erdosproblems.com catalogue, selected 68 problems from among the 652 that were unsolved on his site, chosen to be both significant and difficult; a necessary condition was that a solution either way would, from a human, be worthy of a paper in a high-level journal. All 68 were open as of August 2026. Bloom estimated that only three to five Erdős problems of that caliber had been solved by AI up to that point ^[40][42].

Each conjecture is stated in Lean 4 using mathlib, and a model resolves it by submitting a machine-checkable proof of the conjecture or of its negation. Epoch AI reports that the 68 conjectures cover 65 distinct problems (the Hadwiger-Nelson problem contributes three, one per candidate chromatic number), that statements for 50 of them come from Google DeepMind's open Formal Conjectures library, and that Epoch AI autoformalized the remainder itself with Bloom reviewing each statement. Submissions are checked by Comparator, a proof checker maintained by the Lean FRO, inside a container with no network access; the agent works in a separate container with a Lean toolchain, SageMath, Python, and an offline snapshot of the LaTeX source of 476,000 pure-mathematics arXiv papers dated up to 2022 ^[41].

Each problem gets one attempt, capped at $300 of spend and 72 hours of working time. In the initial run, a pre-release version of GPT-6 Astra was the only one of five models to solve anything: 2 of 68, or 3%. It disproved problem 74 by counterexample for $218 and 15 hours and proved problem 126 for $247 and 16 hours. GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1, and Claude Fable 5 all scored 0% ^[40]. In separate, less systematic attempts with larger budgets and varied scaffolds, which Epoch AI states are "not a FrontierMath Erdős score", the same pre-release Astra solved five of the 68 at least once, adding problems 1, 548, and 571 at a total cost of more than $220,000 across all attempts against roughly $20,000 for the benchmark run itself ^[40]. Epoch AI's own summary of the exercise was that AI-driven mathematical breakthroughs are "real but still fairly uncommon" ^[40].

First Proof

A separate independent evaluation, the First Proof project, takes the opposite approach to verification: human referees rather than a kernel. Its second batch, released in June 2026 by Mohammed Abouzaid, Nikhil Srivastava, Rachel Ward, and Lauren Williams, consists of ten research-level problems contributed by working mathematicians, each arising from the contributor's own research and with a solution known to the contributor but never posted online. Four systems were tested between May 28 and June 1, 2026 under a rule that the underlying model had to be publicly accessible as of May 28: ChatGPT 5.5 Pro plus three academic harnesses from IMProofBench, UCLA, and Princeton. Thirty-nine solutions were produced, each graded by at least two subject experts, with the assistance of 30 expert mathematicians in total, and rated essentially flawless, requiring minor revisions, requiring major revisions, or rejected. Seven of the ten problems received at least one passing grade, meaning essentially flawless or needing only minor revisions, and two more drew a "major revisions" rating where referees judged the approach potentially viable ^[54].

Getting more out of language models

A series of inference-time techniques, most of them introduced between 2021 and 2023, turned LLMs from unreliable calculators into competent problem solvers.

Chain-of-thought prompting, described by Jason Wei and colleagues at Google in January 2022, simply asks the model to generate intermediate reasoning steps before its final answer. With eight worked examples in the prompt, the 540-billion-parameter PaLM model achieved then state-of-the-art accuracy on GSM8K, surpassing a fine-tuned GPT-3 paired with a trained verifier ^[20]. Self-consistency, proposed by Xuezhi Wang and colleagues two months later, samples many independent reasoning paths and takes a majority vote over the final answers; it added 17.9 percentage points on GSM8K over greedy chain-of-thought decoding ^[21].

A complementary line of work uses a second model to judge the first. OpenAI's GSM8K paper trained outcome verifiers to rank candidate solutions ^[10]. The 2023 follow-up, "Let's Verify Step by Step," compared rewarding only correct final answers against rewarding each correct reasoning step, and found that process supervision worked significantly better: a process reward model trained on the released PRM800K dataset of 800,000 step-level human labels let the system solve 78% of a representative MATH subset ^[12]. Process reward models subsequently became a standard ingredient in mathematical reasoning pipelines.

Tool use attacks the arithmetic weakness directly. Program-aided language models (PAL), from Luyu Gao and colleagues in November 2022, have the LLM write a Python program as its reasoning trace and delegate execution to an interpreter; with Codex, PAL beat PaLM's chain-of-thought accuracy on GSM8K by 15 absolute percentage points ^[22]. This style of program synthesis for mathematics persists in modern systems as code-interpreter tooling, and specialized fine-tuned models such as DeepSeekMath and Qwen2.5-Math combine it with large mathematical pretraining corpora.

Reasoning models trained with reinforcement learning

The next jump came from training, not prompting. OpenAI's o1, previewed on September 12, 2024, was trained with reinforcement learning to produce a long private chain of thought before answering, spending more compute at inference in exchange for better answers. OpenAI reported that it solved 83% of AIME problems, against 13% for GPT-4o ^[15]. The approach established test-time compute as a scaling axis alongside model size, and reasoning models became a distinct product category.

DeepSeek-R1, released with open weights under an MIT license in January 2025, demonstrated that the recipe needed no proprietary ingredients. Its precursor R1-Zero was trained with pure reinforcement learning against automatically checkable answers, with no human-labeled reasoning trajectories, and spontaneously developed behaviors such as self-verification and re-checking its own steps ^[13]. R1 scored 79.8% pass@1 on AIME 2024 and 97.3% on MATH-500 ^[23], and the work was later published in Nature ^[13]. Training against machine-checkable answers, often called reinforcement learning with verifiable rewards, is particularly natural in mathematics, where a final answer either matches or does not ^[13].

Milestone results

Minerva, built on PaLM and further trained on 118 GB of arXiv papers and mathematical web pages, was the first demonstration that scale plus domain data could move competition mathematics: in June 2022 it reached 50.3% on MATH with chain-of-thought prompting and majority voting, when the previous state of the art was 6.9%, and 78.5% on GSM8K ^[24].

AlphaGeometry, published in Nature on January 17, 2024 by Trieu Trinh, Thang Luong, and colleagues at Google DeepMind, paired a neural language model with a symbolic deduction engine and trained on 100 million synthetic proofs. It solved 25 of 30 IMO geometry problems under competition time limits, against 10 for the previous best method and 25.9 for the average human gold medallist ^[1][25].

At the IMO itself, DeepMind entered July 2024 with two systems. AlphaProof, which combines a pre-trained language model with the AlphaZero reinforcement learning algorithm and works inside Lean, solved two algebra problems and one number theory problem; AlphaGeometry 2 solved the geometry problem. Together they scored 28 of 42 points, one point below that year's gold threshold of 29, a standard reached by 58 of 609 human contestants. Problems were manually translated into Lean, one solution came within minutes but others took up to three days, and the proofs were graded by Fields Medalist Timothy Gowers and IMO problem selection chair Joseph Myers ^[2]. AlphaProof's methods were published in Nature in November 2025 ^[28].

A year later the formal-translation scaffolding was gone. An advanced version of Gemini Deep Think operated end-to-end in natural language at IMO 2025, solved five of six problems for 35 of 42 points within the 4.5-hour limit, and became the first AI system whose solutions were officially graded and certified as gold-medal standard by IMO coordinators; IMO president Gregor Dolinar called the solutions "astonishing in many respects" ^[4]. OpenAI announced two days earlier, on July 19, 2025, that an unreleased experimental reasoning model had also scored 35/42 on the same problems, solving five of six; researcher Alexander Wei posted the result, which, unlike DeepMind's, was not officially graded or certified by the IMO, and OpenAI said it did not expect to release anything with that level of capability for several months ^[4][27]. Only 67 of 630 human contestants earned gold that year ^[27]. Mathematicians including Terence Tao and Kevin Buzzard cautioned that the announcements rested on conditions that were not reproducible and did not amount to a fair comparison with human contestants, and Tao argued that scores obtained under undisclosed, differing methodologies cannot be directly compared ^[29][30]. The episode is covered in detail at AI gold-medal results at IMO 2025.

2026: claims in research mathematics

Six announcements between May and September 2026 moved the argument from contest scores to research results. Each is listed below with what was claimed, who has checked it, and what remains in dispute. In every case the result reached the public through a company blog post, a preprint, a repository, or a post on X rather than through a journal, and in every case except the Jacobian counterexample the model that produced it was an internal or unreleased version rather than a product a reader can run.

May 2026: the unit distance conjecture

On May 20, 2026, OpenAI announced that an internal model had disproved a conjecture that Erdős posed in 1946 about the planar unit distance problem: how many pairs among n points in the plane can be exactly distance 1 apart. Writing u(n) for the maximum, the best known constructions since 1946 came from a rescaled square grid and gave about n^(1+C/loglog n), and Erdős conjectured an upper bound of n^(1+o(1)). The model's proof constructs, for infinitely many n, configurations with at least n^(1+delta) unit distance pairs for a fixed delta greater than 0, which contradicts that conjectured bound. OpenAI says the construction replaces the Gaussian integers used in Erdős's original argument with algebraic number fields of richer symmetry, and that establishing the existence of the necessary fields uses infinite class field towers and Golod-Shafarevich theory. The company noted that the original proof gives no explicit delta and credited a forthcoming refinement by Princeton's Will Sawin with delta = 0.014. OpenAI also stressed how the proof was found: by a new general-purpose reasoning model rather than a system trained specifically for mathematics, scaffolded for proof search, or aimed at this problem, which the company had evaluated on a collection of Erdős problems ^[43].

The known upper bound of O(n^(4/3)), from Spencer, Szemerédi, and Trotter in 1984, is unaffected, so the problem itself remains open; what fell was the conjectured answer. OpenAI published the proof, a companion paper by external mathematicians, and an abridged chain of thought, and described the result in its own voice as "the first time that a prominent open problem, central to a subfield of mathematics, has been solved autonomously by AI" ^[43]. The external commentary it published was positive but bounded. Tim Gowers wrote that "there is no doubt that the solution to the unit-distance problem is a milestone in AI mathematics" and that he would have recommended acceptance at the Annals of Mathematics without hesitation. Noga Alon called it "an outstanding achievement" and singled out the surprise that the answer is not n^(1+o(1)). Arul Shankar wrote that the paper "demonstrates that current AI models go beyond just helpers to human mathematicians". Thomas Bloom's contribution was more measured: asked whether the proof teaches us something new about the problem, he answered "a moderated yes" ^[43]. A caution from Melanie Matchett Wood in the same companion material, that the release does not show the cases where AI claimed a proof and was wrong, is quoted on the GPT-6 Astra page.

Formalizing the result turned out to be a far larger job than proving it. Epoch AI records that the natural-language proof runs 18 pages while a subsequent Lean formalization came to 1.2 million lines, mostly because a deep result the paper could simply cite had not been formalized in mathlib and had to be derived from first principles ^[40].

July 2026: the Jacobian conjecture

The Jacobian conjecture, stated for two variables by Ludwig Kraus in 1884 and generalized to n variables by Ott-Heinrich Keller in 1939, says that a polynomial map whose Jacobian determinant is a non-zero constant must have a polynomial inverse. Stephen Smale included it in his 1998 list of problems for the next century ^[46].

On July 19, 2026 US time (July 20 UTC), Levent Alpöge, a mathematician at Anthropic, posted a counterexample on X in a single message, crediting Akhil Mathew with asking about the problem and Claude Fable 5 with finding it. The map sends complex triples to complex triples, has Jacobian determinant -2, and sends three distinct points to the same image, so it cannot be inverted ^[44]. Terence Tao wrote it up two days later, noting that the counterexample has degree seven, that presented bare it "appears like a massive miracle" because the vanishing of all non-constant Jacobian coefficients looks like a cancellation in far more equations than there are degrees of freedom, and that "finding such a polynomial looks highly unlikely to be located by brute force"; his post gives a geometric reconstruction of why such a map exists ^[45]. The conjecture remains open in two dimensions and is false in three and above ^[45][46].

Melissa Lee, writing in The Conversation, drew the contrast with the unit distance result: the Jacobian counterexample is short enough to verify by hand, so the difficulty lay not in a long argument but in navigating an enormous search space, which suggests AI may be as useful for finding unexpected mathematical objects as for constructing proofs. She also noted that at the time of writing no details had been published about how Alpöge prompted the model or what its output looked like ^[46].

August 2026: ten results attributed to Astra

On August 1, 2026, OpenAI reported that an internal version of its next major model, GPT-6 Astra, had produced ten new results on open problems in mathematics and theoretical computer science, released a Lean 4 certificate for each, and said the tokens needed to find all ten would cost roughly $2,000 at the API rates of its GPT-5.6 Sol tier ^[34]. The following day Levent Alpöge reported on X that Claude Fable 5, a publicly available model, had reproduced five of the ten in a setup he described as totally autonomous, with only one of the five using essentially the same argument as OpenAI's model ^[35][36]. The results, the reactions, and the disclosure complaints are covered in depth at GPT-6 Astra.

That announcement landed in the shadow of an earlier embarrassment. In October 2025 OpenAI vice president Kevin Weil posted, in a message later deleted, that "GPT-5 found solutions to 10 (!) previously unsolved Erdős problems and made progress on 11 others". Bloom's catalogue records a problem as open only in the sense that, as he put it, "I personally am unaware of a paper which solves it", and he called Weil's post "a dramatic misrepresentation": "GPT-5 found references, which solved these problems, that I personally was unaware of." Demis Hassabis of Google DeepMind commented "This is embarrassing", and OpenAI researcher Sebastien Bubeck acknowledged that "only solutions in the literature were found" while arguing that literature search is itself hard ^[62].

August 2026: zeros of the zeta function

On August 10, 2026, Anthropic reported that an unreleased research version of Claude, prompted by a non-mathematician staff member to "take a real stab" at the Riemann hypothesis, had instead raised the unconditional lower bound for the proportion of nontrivial zeros of the Riemann zeta function on the critical line from 5/12 (about 41.6%, a record set by Pratt, Robles, Zaharescu, and Zeindler in 2020) to 67.2% ^[37]. Claude's first attempt generated 650 ideas, none of which worked; the second, spread over two Claude Code sessions that used 31 million output tokens in total, coordinated about 60 subagents, which between them ran 2,400 shell commands, made thousands of numerical checks against known zeta zeros, and downloaded 54 arXiv papers to confirm the finding was new ^[37]. The paper, credited to Claude as sole author, does not refine the Levinson mollifier method behind every previous record; it instead makes Montgomery's 1973 pair-correlation argument unconditional, building on recent papers by Baluyot, Goldston, Suriajaya, and Turnage-Butterbaugh and a 2000 paper of Bombieri, and it further proves that at least two thirds of the zeros are simple and on the line, that at least five sixths of all zeros are distinct, and that the same bounds hold for primitive Dirichlet L-functions ^[38]. Anthropic mathematicians Levent Alpöge and Ralph Furman validated the proof, number theorists Brian Conrey and Dan Goldston examined it on short notice, and a complete, sorry-free Lean formalization of the main theorems was released on GitHub ^[37][39]. Anthropic said it does not expect the techniques to lead to a proof of the Riemann hypothesis itself, and the paper has not been peer reviewed ^[37].

September 2026: Fermat's Last Theorem, formalized

On September 4, 2026, Anthropic published a complete Lean 4 formalization of Fermat's Last Theorem, which it says a team of Claude agents running an internal research model wrote largely autonomously over 11 days in August 2026, producing roughly 13 million lines of Lean ^[60]. This is a different kind of claim from the others in this section: the mathematics was settled by Andrew Wiles and by Richard Taylor and Wiles in 1995, and what was new was the machine-checked translation. Kevin Buzzard, who leads the human formalization effort at Imperial College London and reviewed the result, wrote that "mathematically this work of anthropic tells us essentially nothing", since the number theory community already accepted the proof and the formalization "just faithfully follows the early literature". What it does tell us, he added, is "what is possible in the field of autoformalization" ^[63]. The project is covered at Formalization of Fermat's Last Theorem.

September 2026: the Navier-Stokes claim

On September 8, 2026, OpenAI announced a proposed resolution of the Navier-Stokes existence and smoothness Millennium Prize Problem, with a manuscript credited to "OpenAI" rather than to named authors and a public Lean repository ^[57]. The claim is contested on both mathematical and priority grounds, and the Clay Mathematics Institute has not accepted it: its page for the problem carried the status "Active" as of September 13, 2026, and its rules require publication in a qualifying outlet, a wait of at least two years after publication, and general acceptance in the global mathematics community before a proposed solution is considered at all ^[58][59]. The claim, the concurrent work by Tristan Buckmaster and Levent Alpöge, and the authorship dispute are treated at OpenAI Navier-Stokes Proposed Solution.

Formal mathematics and autoformalization

Formal, machine-checked mathematics remains the wing of the field where correctness is guaranteed rather than sampled. The standard benchmark is miniF2F, a 2021 suite of 488 olympiad-style problem statements rendered in multiple formal systems ^[31]. Neural provers have advanced quickly against it: DeepSeek-Prover-V2, a 671-billion-parameter open model released in April 2025 that trains with reinforcement learning on subgoal decomposition, reached 88.9% on the miniF2F test set and solved 49 of 658 problems on PutnamBench ^[32]. Its authors noted that the gap between formal and informal mathematical reasoning in LLMs is narrowing substantially ^[32]. Other open provers, such as Goedel-Prover, follow the same Lean-centric pattern.

The bottleneck is autoformalization: translating informal mathematics into formal statements. AlphaProof used a fine-tuned Gemini model for this during training ^[2], and startups and labs are building the pipeline into tools mathematicians can use directly, an agenda covered at AI co-mathematician. Collaborative platforms have appeared for the same purpose, including Prove2Me, which maintains a shared dependency graph of theorem statements so that many agents can work in parallel and which Anthropic used for the Fermat formalization ^[60].

What a certificate settles, and what it does not

By 2026 the presence or absence of a machine-checkable certificate had become the practical dividing line in disputes about AI mathematics, and most of the announcements above shipped one. The checking pipeline is now fairly standard: a proof in Lean 4 against mathlib, a build that fails if the final theorem depends on anything beyond Lean's three standard axioms or contains a sorry placeholder, and an independent check by Comparator, the adversarially minded proof checker maintained by the Lean FRO, which compiles a trusted statement and an untrusted submission in isolated sandboxes and accepts only if the submission proves the identical statement and replays through the kernel ^[41][60].

What that settles is narrow and valuable: the encoded conclusion follows from the encoded definitions and hypotheses, and it does so without any appeal to the reputation of the author or the diligence of a referee. As Tao puts it, a formally verified proof "is precisely a proof whose correctness no longer depends on the reputation or the diligence of its author" ^[47].

Three things it does not settle:

Statement fidelity. A kernel checks the formal statement, not whether that statement means what the informal problem meant. Epoch AI says so explicitly about its own benchmark: for the statements that Formal Conjectures did not already cover it directed AI to do the formalization, had Bloom review each one, and still wrote that its team are "not Lean experts, and so errors may exist", adding that it was seeking additional expert review ^[40][41]. The Leiden Declaration makes the same point in general terms, noting that plausible but incorrect arguments are hard to distinguish from correct ones not only in informal mathematics but also in formalizations, "where the difficulty lies in the translation between computer-encoded and human presentations of concepts" ^[48].

Cost and effort. Formalization is a separate project bolted on to the mathematics, and one that can dwarf it. The unit distance result went from an 18-page paper to 1.2 million lines of Lean, and Epoch AI treats this as a structural limitation of any Lean-based benchmark of open problems rather than an incident ^[40].

Whether it is good mathematics. This is the axis on which the 2026 disputes turn. Tao's ICM essay decomposes "solve unsolved problems" into a five-stage pipeline, of which only the first stage was ever an explicit community goal: proof generation, proof verification, proof exposition, proof publication and digestion, and canonicalization into the definitive form in which a result is taught. Formal verification accelerates the first two stages and does nothing for the last three ^[47]. He argues that current AI exposition "very often dwells at length on trivialities" while passing briefly through or actively obscuring the most interesting and novel parts of an argument, and that over-polished writing sands away the natural friction in a human proof that tells a reader where to slow down. His proposed rule of thumb is blunt: "A proof that no human can properly explain should be viewed as incomplete, even if it has been formally verified" ^[47].

The community response

Two documents from 2026 set out how the mathematical community proposes to handle this.

The Leiden Declaration on Artificial Intelligence and Mathematics, published on 2 June 2026 and endorsed by the International Mathematical Union, grew out of a 2025 workshop at the Lorentz Center in Leiden and sets out recommendations for individual mathematicians, for mathematical organizations and not-for-profit funders, for policymakers, and for commercial AI developers. Among the recommendations to individuals are to disclose tool use in a dedicated section of a paper, to retain human responsibility for the correctness of arguments produced with automated help, to "affirm the humanity of authorship" because credit and responsibility "should not be given to automated systems", and to put proactive effort into attribution because automated tools are known to be poor at it. The declaration also objects specifically to results "communicated through informal channels such as press releases or blog posts" without the information needed for scientific evaluation, a practice it says "seeks publicity for new results on market timelines before the accepted processes of community evaluation in mathematics can take place" ^[48]. It had more than 4,000 signatories as of September 13, 2026 ^[49]. The document is covered at Leiden Declaration.

A Severe Misalignment of AI in Mathematics, published on 11 September 2026 with 25 initial signatories, all Fields Medallists, states that LLM mathematical capability has improved to the point where models "can solve major outstanding problems in many fields of mathematics" and argues that "the push by AI companies to solve mathematical problems as a benchmark is detrimental to the science of mathematics, and to the mathematical community". Its case is that solving problems is a proxy for the real goal of conceptual understanding, that rushed announcements leave no time for a proper writeup or for citing prior work, which raises attribution and plagiarism questions, and that without mathematicians willing to develop and integrate them, AI-conceived ideas never enter the canon and "the crucial human transmission chain between mathematicians would be lost". It names students and ideas as "the most precious resources of our profession" ^[50]. Tao, one of the signatories, wrote that the declaration grew out of discussions among the signatories over the preceding week and that the group had deliberately traded a consultative process for speed ^[51]. More than 5,800 people had endorsed it as of September 13, 2026 ^[52]. It is covered at A Severe Misalignment of AI in Mathematics.

Neither document argues that the 2026 results are incorrect. Both are about what happens after a result is correct.

Limitations and open questions

Benchmark scores overstate how humanlike the underlying competence is. Apple researchers showed with GSM-Symbolic in October 2024 that model accuracy on GSM8K-style problems drops when names and numbers are changed, and falls by up to 65% when a single plausible-sounding but irrelevant clause is added, behavior consistent with pattern matching rather than reasoning from first principles ^[11]. Answer-only grading hides a related failure: a model can produce the right final answer through a wrong argument, and a model that will prove anything it is asked to prove will also prove false statements. MathArena's BrokenArXiv track exists to measure exactly that, scoring models on whether they refuse a plausible but false statement and recognize why it is false ^[55].

Benchmark governance has its own problems. OpenAI reported just over 25% on FrontierMath for o3 in December 2024, but when Epoch AI independently evaluated the released o3 in April 2025 it scored around 10%, a discrepancy attributed to different compute settings and a different production model ^[26]. Epoch's own v2 revision of FrontierMath corrected errors in 42% of the original problems ^[17], and scores on the two versions are not comparable.

Where referees rather than kernels do the grading, the reported failure modes are about argument quality rather than arithmetic. First Proof's referees found that AI solutions "tended to handle routine parts of an argument in meticulous detail while glossing over the most difficult steps, sometimes asserting that a key claim follows from 'standard arguments' without justification, or citing papers that do not actually contain the claimed results". On one problem, several solutions borrowed phrasing from the contributor's own earlier paper line by line, reusing its terminology and even its labels, without citing it anywhere; the report observes that a human submission of that kind would have been flagged for plagiarism ^[54].

Gary Marcus has pressed a different objection, aimed not at the results but at what is inferred from them. Writing on August 2, 2026 about the Astra announcement, which he called "amazing" and did not dispute, he argued that treating success on formal mathematics as evidence of imminent general capability is a fallacy of composition. His reason for thinking the fallacy applies here is specific to the domain. "Math lends itself to two things: verification (using symbolic tools), and massive amounts of cheaply produced synthetic data where you can guarantee that the answers are correct," he wrote, adding that the same holds for coding but not in general: "You can generate as many math facts as you want; you can't simulate the open-ended world. You can verify math; you can't verify a military strategy in the same way." ^[53] The Leiden Declaration identifies the same property of mathematics as what makes it attractive to general-purpose AI developers, and flags the assumption that theorem-proving capability will extend to broader reasoning as an assumption rather than a finding ^[48].

The distance between contest mathematics and research mathematics remains the larger open question, and 2026 narrowed it without closing it. On Epoch AI's budgeted measurement of significant open problems, the best score was 3% ^[40]. Tao argues that the more pressing problem is now downstream: if AI tools keep improving, the community will move from an era of "proof scarcity" to one of "proof abundance", in which proofs accumulate faster than they can be verified, written up, refereed, or worked into definitive form, while the institutions of the profession were all designed for scarcity. He notes that the Erdős problems database already holds dozens of AI-generated proof submissions, many of them probably correct, for which no human expert has volunteered to verify and vouch, and in several cases the human submitters have said they are not qualified to do so ^[47]. By May 2026, Nature reported mathematicians describing their profession as being reshaped, with AI systems contributing to actual mathematical work and Tao observing that the job description of a mathematician is changing ^[33].

See also

• AI gold-medal results at IMO 2025
• GPT-6 Astra
• OpenAI Navier-Stokes Proposed Solution
• Formalization of Fermat's Last Theorem
• AlphaProof
• FrontierMath
• Chain-of-thought
• Automated theorem proving
• Reasoning models

References

1. ^1 ^2Trinh, T. et al. "Solving olympiad geometry without human demonstrations." Nature 625, 476-482 (January 17, 2024). nature.com/...s41586-023-06747-5
2. ^1 ^2 ^3 ^4Google DeepMind. "AI achieves silver-medal standard solving International Mathematical Olympiad problems." July 25, 2024. deepmind.google/...-problems-at-silver-medal-level
3. ^1 ^2Glazer, E. et al. "FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI." arXiv, November 7, 2024. arxiv.org/...2411.04872
4. ^1 ^2 ^3 ^4Google DeepMind. "Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad." July 21, 2025. deepmind.google/...rnational-mathematical-olympiad
5. ^Wikipedia. "Logic Theorist." en.wikipedia.org/...Logic_Theorist
6. ^Wikipedia. "Computer-assisted proof." en.wikipedia.org/...Computer-assisted_proof
7. ^The Rocq Prover. "About." rocq-prover.org/about
8. ^Lean Prover Community. "Mathlib statistics." leanprover-community.github.io/mathlib_stats
9. ^1 ^2Hendrycks, D. et al. "Measuring Mathematical Problem Solving With the MATH Dataset." arXiv, March 5, 2021. arxiv.org/...2103.03874
10. ^1 ^2 ^3Cobbe, K. et al. "Training Verifiers to Solve Math Word Problems." arXiv, October 27, 2021. arxiv.org/...2110.14168
11. ^1 ^2Mirzadeh, I. et al. "GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models." arXiv, October 7, 2024. arxiv.org/...2410.05229
12. ^1 ^2 ^3Lightman, H. et al. "Let's Verify Step by Step." arXiv, May 31, 2023. arxiv.org/...2305.20050
13. ^1 ^2 ^3 ^4Guo, D. et al. "DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning." arXiv, January 22, 2025; Nature 645, 633-638 (2025). arxiv.org/...2501.12948
14. ^1 ^2 ^3Wikipedia. "American Invitational Mathematics Examination." en.wikipedia.org/...tional_Mathematics_Examination
15. ^1 ^2 ^3Wikipedia. "OpenAI o1." en.wikipedia.org/...OpenAI_o1
16. ^1 ^2 ^3MathArena. "Evaluating LLMs on uncontaminated math competitions." Leaderboard accessed September 13, 2026. matharena.ai
17. ^1 ^2 ^3Epoch AI. "FrontierMath Tiers 1-4." epoch.ai/...tiers-1-4
18. ^1 ^2Phan, L. et al. "Humanity's Last Exam." arXiv, January 24, 2025. arxiv.org/...2501.14249
19. ^1 ^2 ^3Center for AI Safety and Scale AI. "Humanity's Last Exam." Accessed September 13, 2026. lastexam.ai
20. ^Wei, J. et al. "Chain-of-Thought Prompting Elicits Reasoning in Large Language Models." arXiv, January 28, 2022. arxiv.org/...2201.11903
21. ^Wang, X. et al. "Self-Consistency Improves Chain of Thought Reasoning in Language Models." arXiv, March 21, 2022. arxiv.org/...2203.11171
22. ^Gao, L. et al. "PAL: Program-aided Language Models." arXiv, November 18, 2022. arxiv.org/...2211.10435
23. ^1 ^2DeepSeek. "DeepSeek-R1." GitHub repository. github.com/...DeepSeek-R1
24. ^1 ^2 ^3Google Research. "Minerva: Solving Quantitative Reasoning Problems with Language Models." June 30, 2022. research.google/...g-problems-with-language-models
25. ^1 ^2Google DeepMind. "AlphaGeometry: An Olympiad-level AI system for geometry." January 17, 2024. deepmind.google/...ad-level-ai-system-for-geometry
26. ^1 ^2Zeff, M. "OpenAI's o3 AI model scores lower on a benchmark than the company initially implied." TechCrunch, April 20, 2025. techcrunch.com/...an-the-company-initially-implied
27. ^1 ^2 ^3Engadget. "OpenAI's experimental model achieved gold at the International Math Olympiad." July 19, 2025. engadget.com/...ernational-math-olympiad-182719801
28. ^Hubert, T., Mehta, R., Silver, D. et al. "Olympiad-level formal mathematical reasoning with reinforcement learning." Nature 651, 607-613 (November 12, 2025). nature.com/...s41586-025-09833-y
29. ^1 ^2Wikipedia. "International Mathematical Olympiad." en.wikipedia.org/...national_Mathematical_Olympiad
30. ^Tao, T. Mastodon post on evaluating AI competition performance. Mathstodon, July 2025. mathstodon.xyz/...114881418225852441
31. ^Zheng, K., Han, J. M., Polu, S. "MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics." arXiv, August 31, 2021. arxiv.org/...2109.00110
32. ^1 ^2Ren, Z. Z. et al. "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition." arXiv, April 30, 2025. arxiv.org/...2504.21801
33. ^Castelvecchi, D. "'It is incredible': How AI is transforming mathematics." Nature, May 19, 2026. nature.com/...d41586-026-01553-1
34. ^1 ^2 ^3OpenAI. "Ten advances in mathematics and theoretical computer science." August 1, 2026. openai.com/...ten-advances-in-mathematics
35. ^Alpöge, L. X post ("so after 24h i have half of them with fable"). August 2, 2026. x.com/...2083855298239078748
36. ^Mowshowitz, Z. "OpenAI's Unreleased Model Astra Solves Ten Major Open Mathematics Problems." Don't Worry About the Vase, August 3, 2026. thezvi.substack.com/...released-model-astra-solves
37. ^1 ^2 ^3 ^4 ^5Anthropic. "Learning more about Claude's mathematical capabilities." August 10, 2026. anthropic.com/...riemann-zeta
38. ^Claude. "More than two thirds of the zeros of the Riemann zeta function lie on the critical line." Anthropic, August 10, 2026. www-cdn.anthropic.com/...cb4a17c9dbc8f608f1c37.pdf
39. ^Anthropic. "zeta-23-lean: Lean 4 formalization of Claude's zeta paper." GitHub, August 2026. github.com/...zeta-23-lean
40. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11Adamczewski, T. and Burnham, G. "Announcing FrontierMath Erdős." Epoch AI, September 1, 2026. epoch.ai/...announcing-frontiermath-erdos
41. ^1 ^2 ^3 ^4Epoch AI. "FrontierMath Erdős." Benchmark page, accessed September 13, 2026. epoch.ai/...frontiermath-erdos
42. ^1 ^2Adamczewski, T. and Bloom, T. F. "FrontierMath Erdős." Epoch AI, 2026. epoch.ai/...frontiermath-erdos.pdf
43. ^1 ^2 ^3 ^4 ^5OpenAI. "An OpenAI model has disproved a central conjecture in discrete geometry." May 20, 2026. openai.com/...sproves-discrete-geometry-conjecture
44. ^1 ^2 ^3Alpöge, L. X post ("hello there the jacobian conjecture is false thanx"). July 20, 2026 UTC. x.com/...2079028340955197566
45. ^1 ^2 ^3 ^4Tao, T. "A digestion of the Jacobian conjecture counterexample." What's new, July 21, 2026. terrytao.wordpress.com/...onjecture-counterexample
46. ^1 ^2 ^3 ^4Lee, M. "'hello there the jacobian conjecture is false thanx': why a tiny social media post has mathematicians rethinking AI." The Conversation, July 22, 2026. theconversation.com/...icians-rethinking-ai-283883
47. ^1 ^2 ^3 ^4 ^5Tao, T. "Mathematics in the age of AI." arXiv:2608.16753, August 17, 2026. arxiv.org/...2608.16753
48. ^1 ^2 ^3 ^4Leiden Declaration on Artificial Intelligence and Mathematics. June 2, 2026. DOI 10.5281/zenodo.20302944. leidendeclaration.ai
49. ^Leiden Declaration on Artificial Intelligence and Mathematics. "Signatories." Accessed September 13, 2026. leidendeclaration.ai/signatories
50. ^1 ^2"A Severe Misalignment of AI in Mathematics." Math and AI, accessed September 13, 2026. mathandai.org
51. ^1 ^2Tao, T. "A Severe Misalignment of AI in Mathematics." What's new, September 11, 2026. terrytao.wordpress.com/...ent-of-ai-in-mathematics
52. ^Math and AI. "Endorsers." Accessed September 13, 2026. mathandai.org/endorsers
53. ^Marcus, G. "OpenAI's amazing, but vastly oversold, new model Astra." Marcus on AI, August 2, 2026. garymarcus.substack.com/...ing-but-vastly-oversold
54. ^1 ^2Abouzaid, M., Srivastava, N., Ward, R., Williams, L. "First Proof Second Batch." arXiv:2606.18119, June 16, 2026. arxiv.org/...2606.18119
55. ^1 ^2 ^3 ^4MathArena. "MathArena Benchmarks and Links." Accessed September 13, 2026. matharena.ai/competitions
56. ^1 ^2Gehrunger, T., Dekoninck, J., Vechev, M. "ArXivLean: How Well Can LLMs Formally Prove Research Math?" MathArena, April 21, 2026. matharena.ai/arxivlean
57. ^1 ^2 ^3OpenAI. "On the Navier-Stokes Millennium Prize Problem." September 8, 2026. openai.com/...navier-stokes-solution
58. ^1 ^2Clay Mathematics Institute. "Navier-Stokes Equation." Accessed September 13, 2026. claymath.org/...navier-stokes-equation
59. ^Clay Mathematics Institute. "Rules for the Millennium Prize Problems." Accessed September 13, 2026. claymath.org/...rules
60. ^1 ^2 ^3 ^4 ^5Anthropic. "Formalizing Fermat's Last Theorem." September 4, 2026. anthropic.com/...formalizing-fermats-last-theorem
61. ^Epoch AI. "FrontierMath Tier 4 (v2)." Benchmark page, accessed September 13, 2026. epoch.ai/...frontiermath-tier-4
62. ^Ha, A. "OpenAI's 'embarrassing' math." TechCrunch, October 19, 2025. techcrunch.com/...openais-embarrassing-math
63. ^Buzzard, K. "FLT: Anthropic has beaten me to it." Xena Project, September 4, 2026. xenaproject.wordpress.com/...c-has-beaten-me-to-it