# Mathematical reasoning in AI

> Source: https://aiwiki.ai/wiki/mathematical_reasoning
> Updated: 2026-07-24
> Fact-checked: 2026-08-05
> Categories: AI Benchmarks, AI Research, Mathematics, Reasoning Models
> License: CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) - attribute to "AI Wiki (aiwiki.ai)"
> Cite as: AI Wiki. "Mathematical reasoning in AI." aiwiki.ai, 24 Jul 2026. https://aiwiki.ai/wiki/mathematical_reasoning
> From AI Wiki (https://aiwiki.ai), the free encyclopedia of artificial intelligence. Reuse freely with attribution.

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](https://aiwiki.ai/wiki/lean), Isabelle, and Rocq, represents mathematics in formal languages where every step is machine-checkable. The statistical tradition, dominant since [large language models](https://aiwiki.ai/wiki/large_language_model) (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](https://aiwiki.ai/wiki/alphaproof) brought the two lineages together [2]. Research-level mathematics remains largely open: on the hardest benchmarks, frontier models still fail most problems [3], and mathematicians continue to dispute how much of the measured progress reflects genuine reasoning [29].

## 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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/mathlib), had grown to more than 283,000 theorems and 134,000 definitions from over 770 contributors by mid-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.

## 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.

| Benchmark | Introduced | Contents | Status (mid-2026) |
|---|---|---|---|
| [MATH](https://aiwiki.ai/wiki/math) | March 2021 (Hendrycks et al.) | 12,500 competition problems with step-by-step solutions [9] | Largely saturated by frontier models |
| [GSM8K](https://aiwiki.ai/wiki/gsm8k) | October 2021 (OpenAI) | 8,500 grade-school word problems [10] | Saturated; robustness questioned [11] |
| [MATH-500](https://aiwiki.ai/wiki/math_500) | May 2023 (OpenAI) | 500-problem test subset of MATH [12] | Standard quick evaluation; top models above 97% [13] |
| [AIME](https://aiwiki.ai/wiki/aime) | Reused each year | 15 integer-answer problems from the annual American Invitational Mathematics Examination [14] | Top reasoning models above 80% by early 2025 [15][16] |
| [FrontierMath](https://aiwiki.ai/wiki/frontiermath) | November 2024 (Epoch AI) | Hundreds of unpublished expert-level problems in four tiers [3][17] | Hardest tiers mostly unsolved |
| [Humanity's Last Exam](https://aiwiki.ai/wiki/humanity_s_last_exam) | January 2025 (CAIS and Scale AI) | 2,500 expert questions across more than a hundred subjects including mathematics [18][19] | Top leaderboard score 38.3% (Gemini 3 Pro) [19] |

[GSM8K](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/math_500), survives as a standard quick benchmark [12].

The [AIME](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/frontiermath), commissioned by [Epoch AI](https://aiwiki.ai/wiki/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 corrected errors found in 42% of the original problems [17]. [Humanity's Last Exam](https://aiwiki.ai/wiki/humanity_s_last_exam) plays a similar role across disciplines, with mathematics among its subjects; the top score on its official leaderboard stood at 38.3% as of mid-2026 [18][19].

Because static benchmarks leak into training data, evaluators increasingly test on competitions published after a model's release. [MathArena](https://aiwiki.ai/wiki/matharena) evaluates models on each new olympiad and contest as it happens, including the AIME, HMMT, the Putnam, and the IMO [16].

## 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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/program_synthesis) for mathematics persists in modern systems as code-interpreter tooling, and specialized fine-tuned models such as [DeepSeekMath](https://aiwiki.ai/wiki/deepseek_math) and [Qwen2.5-Math](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/o1), previewed on September 12, 2024, was trained with [reinforcement learning](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/test_time_compute) as a scaling axis alongside model size, and [reasoning models](https://aiwiki.ai/wiki/reasoning_models) became a distinct product category.

[DeepSeek-R1](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/rlvr), is particularly natural in mathematics, where a final answer either matches or does not [13].

## Milestone results

| Date | System | Result |
|---|---|---|
| June 2022 | Minerva (Google) | 50.3% on MATH with majority voting, versus 6.9% prior state of the art [24] |
| January 2024 | AlphaGeometry (DeepMind) | 25 of 30 olympiad geometry problems, published in Nature [1][25] |
| July 2024 | AlphaProof + AlphaGeometry 2 | 28/42 points on IMO 2024 problems, silver-medal standard [2] |
| September 2024 | o1-preview (OpenAI) | 83% on AIME versus 13% for GPT-4o [15] |
| December 2024 | o3 (OpenAI) | Just over 25% on FrontierMath reported, in a high-compute configuration [26] |
| January 2025 | DeepSeek-R1 | 79.8% on AIME 2024 with open weights [23] |
| July 2025 | Gemini Deep Think (DeepMind) | 35/42 on IMO 2025, gold-medal standard, officially certified [4] |
| July 2025 | OpenAI experimental model | 35/42 on IMO 2025, self-reported [27] |

[Minerva](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/alphageometry), published in Nature on January 17, 2024 by Trieu Trinh, Thang Luong, and colleagues at [Google DeepMind](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/gemini_2_5_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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/ai_imo_gold_2025).

By 2026 the frontier had shifted from competitions to research problems. On August 1, 2026, OpenAI reported that an internal version of its next major model, [Astra](https://aiwiki.ai/wiki/openai_astra), had produced ten new results on long-standing open problems in mathematics and theoretical computer science, released a machine-checkable Lean certificate for each result, and said the tokens needed to find all ten solutions would cost roughly $2,000 at the API rates of its GPT-5.6 Sol tier [34]. The following day Levent Alpöge, a mathematician at Anthropic, reported on X that [Claude Fable 5](https://aiwiki.ai/wiki/claude_fable_5), a publicly available model, had reproduced five of the ten results in what he described as a totally autonomous setup with a generic prompt and no internet access, with only one of the five using essentially the same argument as OpenAI's model; the claim is his own report, posted on X rather than in a reviewed venue [35][36].

## 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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/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](https://aiwiki.ai/wiki/ai_co_mathematician). The attraction is that a formal proof, unlike a natural-language one, needs no expert grader: the kernel either accepts it or it does not, which is why many researchers consider formal mathematics the most reliable path to trustworthy machine reasoning at research level.

## 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]. 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].

The distance between contest mathematics and research mathematics is the larger open question. Competition problems are short, self-contained, and known to have solutions; research problems are none of these. FrontierMath's hardest tier and its open-problems track remain essentially unsolved [17], and skeptics note that gold-medal contest performance says little about the ability to produce new mathematics [29]. Even so, the direction of travel is visible: by May 2026, Nature reported mathematicians describing their profession as being reshaped, with AI systems contributing to actual mathematical work and Terence Tao observing that the job description of a mathematician is changing [33].

## See also

- [AI gold-medal results at IMO 2025](https://aiwiki.ai/wiki/ai_imo_gold_2025)
- [AlphaProof](https://aiwiki.ai/wiki/alphaproof)
- [FrontierMath](https://aiwiki.ai/wiki/frontiermath)
- [Chain-of-thought](https://aiwiki.ai/wiki/chain_of_thought)
- [Automated theorem proving](https://aiwiki.ai/wiki/automated_theorem_proving)
- [Reasoning models](https://aiwiki.ai/wiki/reasoning_models)

## References

1. Trinh, T. et al. "Solving olympiad geometry without human demonstrations." Nature 625, 476-482 (January 17, 2024). https://www.nature.com/articles/s41586-023-06747-5
2. Google DeepMind. "AI achieves silver-medal standard solving International Mathematical Olympiad problems." July 25, 2024. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
3. Glazer, E. et al. "FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI." arXiv, November 7, 2024. https://arxiv.org/abs/2411.04872
4. Google DeepMind. "Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad." July 21, 2025. https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/
5. Wikipedia. "Logic Theorist." https://en.wikipedia.org/wiki/Logic_Theorist
6. Wikipedia. "Computer-assisted proof." https://en.wikipedia.org/wiki/Computer-assisted_proof
7. The Rocq Prover. "About." https://rocq-prover.org/about
8. Lean Prover Community. "Mathlib statistics." https://leanprover-community.github.io/mathlib_stats.html
9. Hendrycks, D. et al. "Measuring Mathematical Problem Solving With the MATH Dataset." arXiv, March 5, 2021. https://arxiv.org/abs/2103.03874
10. Cobbe, K. et al. "Training Verifiers to Solve Math Word Problems." arXiv, October 27, 2021. https://arxiv.org/abs/2110.14168
11. Mirzadeh, I. et al. "GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models." arXiv, October 7, 2024. https://arxiv.org/abs/2410.05229
12. Lightman, H. et al. "Let's Verify Step by Step." arXiv, May 31, 2023. https://arxiv.org/abs/2305.20050
13. Guo, D. et al. "DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning." arXiv, January 22, 2025; Nature 645, 633-638 (2025). https://arxiv.org/abs/2501.12948
14. Wikipedia. "American Invitational Mathematics Examination." https://en.wikipedia.org/wiki/American_Invitational_Mathematics_Examination
15. Wikipedia. "OpenAI o1." https://en.wikipedia.org/wiki/OpenAI_o1
16. MathArena. "Evaluating LLMs on uncontaminated math competitions." https://matharena.ai
17. Epoch AI. "FrontierMath Tiers 1-4." https://epoch.ai/frontiermath/tiers-1-4
18. Phan, L. et al. "Humanity's Last Exam." arXiv, January 24, 2025. https://arxiv.org/abs/2501.14249
19. Center for AI Safety and Scale AI. "Humanity's Last Exam." https://lastexam.ai
20. Wei, J. et al. "Chain-of-Thought Prompting Elicits Reasoning in Large Language Models." arXiv, January 28, 2022. https://arxiv.org/abs/2201.11903
21. Wang, X. et al. "Self-Consistency Improves Chain of Thought Reasoning in Language Models." arXiv, March 21, 2022. https://arxiv.org/abs/2203.11171
22. Gao, L. et al. "PAL: Program-aided Language Models." arXiv, November 18, 2022. https://arxiv.org/abs/2211.10435
23. DeepSeek. "DeepSeek-R1." GitHub repository. https://github.com/deepseek-ai/DeepSeek-R1
24. Google Research. "Minerva: Solving Quantitative Reasoning Problems with Language Models." June 30, 2022. https://research.google/blog/minerva-solving-quantitative-reasoning-problems-with-language-models/
25. Google DeepMind. "AlphaGeometry: An Olympiad-level AI system for geometry." January 17, 2024. https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/
26. Zeff, M. "OpenAI's o3 AI model scores lower on a benchmark than the company initially implied." TechCrunch, April 20, 2025. https://techcrunch.com/2025/04/20/openais-o3-ai-model-scores-lower-on-a-benchmark-than-the-company-initially-implied/
27. Engadget. "OpenAI's experimental model achieved gold at the International Math Olympiad." July 19, 2025. https://www.engadget.com/ai/openais-experimental-model-achieved-gold-at-the-international-math-olympiad-182719801.html
28. Hubert, T., Mehta, R., Silver, D. et al. "Olympiad-level formal mathematical reasoning with reinforcement learning." Nature 651, 607-613 (November 12, 2025). https://www.nature.com/articles/s41586-025-09833-y
29. Wikipedia. "International Mathematical Olympiad." https://en.wikipedia.org/wiki/International_Mathematical_Olympiad
30. Tao, T. Mastodon post on evaluating AI competition performance. Mathstodon, July 2025. https://mathstodon.xyz/@tao/114881418225852441
31. Zheng, K., Han, J. M., Polu, S. "MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics." arXiv, August 31, 2021. https://arxiv.org/abs/2109.00110
32. Ren, Z. Z. et al. "DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition." arXiv, April 30, 2025. https://arxiv.org/abs/2504.21801
33. Castelvecchi, D. "'It is incredible': How AI is transforming mathematics." Nature, May 19, 2026. https://www.nature.com/articles/d41586-026-01553-1
34. OpenAI. "Ten advances in mathematics and theoretical computer science." August 1, 2026. https://openai.com/index/ten-advances-in-mathematics/
35. Alpöge, L. X post ("so after 24h i have half of them with fable"). August 2, 2026. https://x.com/__alpoge__/status/2083855298239078748
36. Mowshowitz, Z. "OpenAI's Unreleased Model Astra Solves Ten Major Open Mathematics Problems." Don't Worry About the Vase, August 3, 2026. https://thezvi.substack.com/p/openais-unreleased-model-astra-solves