AI mathematical reasoning and theorem proving

Also known as AI theorem proving, Formal theorem proving with AI, AlphaProof

AI systems now solve some olympiad-level mathematics problems, including a score at gold-medal level at the 2025 International Mathematical Olympiad. Formal proof systems that check each step in the Lean language are the most rigorous of these approaches, but results on contest problems do not yet show that AI can solve open research problems.

Research and prototypesDemonstratedReviewed 21 Oct 2026
AI illustration · Illustrative scene, not a photograph of the specific device or experiment.

In plain language

Mathematics is built from proofs, where each step must follow logically from the one before. For a long time, computers could check proofs that people had written out in full, but they struggled to find new proofs for hard problems on their own.

Recent AI systems can now produce proofs for some competition problems. In 2024, a Google DeepMind system scored 28 of 42 points at the International Mathematical Olympiad, which the company described as silver-medal level. In 2025, an advanced version of Gemini Deep Think worked in plain language and scored 35 of 42, a gold-medal score that the competition's coordinators certified. These results show real progress, but contest problems are much easier to set up than open research questions.

Technical explanation

Two broad approaches are in use. Formal systems write proofs in a proof assistant such as Lean, which checks every step automatically. Informal systems use large language models to write proofs in natural language, which are harder to check. AlphaProof, described by Hubert, Silver and colleagues in Nature (2025), learns to find formal proofs through reinforcement learning on millions of auto-formalised problems. Its authors also describe test-time reinforcement learning, which generates and learns from related problem variants while the system is working on a hard problem.

At the 2024 International Mathematical Olympiad, the Nature paper reports that a system with AlphaProof as its core engine solved three of the five non-geometry problems, including the hardest problem in the competition. When combined with AlphaGeometry 2 it reached a score equivalent to a silver medallist. AlphaGeometry, described by Trinh, Luong and colleagues in Nature (2024), solved 25 of 30 recent olympiad-level geometry problems on a test set, compared with 10 for the previous best method. The 2024 formal results depended on problems being translated by hand into formal mathematical language first. The company's blog says the solutions were graded by two external mathematicians.

In 2025, Gemini Deep Think, which DeepMind says operated end to end in natural language, solved five of six problems and scored 35 of 42 points. According to DeepMind's blog, IMO coordinators graded the proofs under the same criteria used for students. The IMO review confirmed the answers but did not validate the underlying system. Separately, FunSearch (Romera-Paredes, Fawzi and colleagues, Nature, 2023) used large language models to search for computer programs that found new large cap set constructions, which shows AI can contribute to discovery in combinatorics, though this is different from proving theorems.

What the evidence says

Each statement is typed by the strength of its evidence and linked to the source that supports it.

Demonstrated Shown in a published experiment, test or shipping product.

At the 2024 International Mathematical Olympiad, a system with AlphaProof as its core engine solved three of the five non-geometry problems, including the competition's hardest problem.

Sources: [1] · Abstract

Combined with AlphaGeometry 2, the AlphaProof-based system reached a score equivalent to a silver medallist at IMO 2024.

Sources: [1] · Abstract

On a test set of 30 recent olympiad-level geometry problems, AlphaGeometry solved 25, against 10 for the previous best method.

Sources: [2] · Abstract

An advanced Gemini Deep Think model, working end to end in natural language, solved five of six IMO 2025 problems and scored 35 of 42 points, which the IMO coordinators graded under the same criteria as student solutions.

Sources: [4] · Announcement text

For the 2024 formal results, the competition problems were first manually translated into formal mathematical language before the system attempted them.

Sources: [3] · Results section

FunSearch, which uses large language models to search for programs, found new constructions of large cap sets that go beyond the best-known ones.

Sources: [5] · Abstract

Reported, unverified Stated by a company or team but not independently confirmed.

Google DeepMind reports that its IMO 2024 system scored 28 of 42 points, at silver-medal level, with solutions graded by two external mathematicians.

Sources: [3] · Results section · medium confidence

Limitations and open problems

  • Results so far are on olympiad-level contest problems, which are short and self-contained. They do not show that AI can prove open research conjectures.
  • The 2024 formal systems needed competition problems to be translated into formal mathematical language by hand before the system could attempt them (DeepMind, 2024).
  • AlphaProof's 2024 result used multi-day computation (Hubert and colleagues, 2025), far longer than the two 4.5-hour sessions that human contestants sit.
  • The 2024 results came from separate systems for geometry (AlphaGeometry) and non-geometry problems (AlphaProof). Only the combined system reached a silver-level score (Hubert and colleagues, 2025).

Possible future uses

Speculative

Ideas, not predictions. None of these has been demonstrated.

  • Automatic checking of long research proofs in Lean, so that human referees spend less time on routine verification.
  • Searching for counterexamples and extremal constructions in combinatorics, following the approach used for cap sets.
  • Step-checked proof tutors that give students immediate feedback on each line of a formal argument.

Timeline

  1. 14 Dec 2023Romera-Paredes, Fawzi and colleagues publish FunSearch in Nature, reporting new large cap set constructions found by program search with language models. Sources: [5]
  2. 17 Jan 2024Trinh, Luong and colleagues publish AlphaGeometry in Nature, solving 25 of 30 olympiad-level geometry problems in a test set. Sources: [2]
  3. 25 Jul 2024Google DeepMind announces that its AlphaProof and AlphaGeometry 2 systems reached a silver-medal score of 28 of 42 at the 2024 International Mathematical Olympiad. Sources: [3]
  4. 21 Jul 2025Google DeepMind announces that an advanced Gemini Deep Think model scored 35 of 42 at the 2025 International Mathematical Olympiad, certified by IMO coordinators. Sources: [4]
  5. 12 Nov 2025Hubert, Silver and colleagues publish the AlphaProof paper in Nature, describing formal olympiad-level proof search with reinforcement learning. Sources: [1]

Futures this could help bring about

AI illustration
How far away?

AI that makes its own scientific discoveries

Science demonstrated · 4 of 6 steps done

Related breakthroughs

Glossary

Formal proof
A proof written in a precise formal language so that a computer can check every logical step.
Lean
A proof assistant and programming language in which mathematicians write and automatically check formal proofs.
International Mathematical Olympiad (IMO)
The annual international competition for high school students, in which each contestant solves six problems over two 4.5-hour sessions.
Cap set
A set of points in a grid with no three on a common straight line, a combinatorics problem with open questions about how large such sets can be.

Sources

  1. peer reviewed paper
    Olympiad-level formal mathematical reasoning with reinforcement learning
    Thomas Hubert, David Silver. Nature, 12 Nov 2025. DOI: 10.1038/s41586-025-09833-y. Accessed 21 Oct 2026.
  2. peer reviewed paper
    Solving olympiad geometry without human demonstrations
    Trieu H. Trinh, Thang Luong. Nature, 17 Jan 2024. DOI: 10.1038/s41586-023-06747-5. Accessed 21 Oct 2026.
  3. company announcement
    AI achieves silver-medal standard solving International Mathematical Olympiad problems
    Google DeepMind, 25 Jul 2024. Accessed 21 Oct 2026.
  4. company announcement
    Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad
    Google DeepMind, 21 Jul 2025. Accessed 21 Oct 2026.
  5. peer reviewed paper
    Mathematical discoveries from program search with large language models
    Bernardino Romera-Paredes, Alhussein Fawzi. Nature, 14 Dec 2023. DOI: 10.1038/s41586-023-06924-6. Accessed 21 Oct 2026.

Revision history

3 changes since this profile was created.

Changes on 21 Oct 2026
Published on owner instruction; AI-researched, QA-checked and link-checked2817c93
Sources and claims re-checked against originalsfbb434c
Initial profile drafted from primary sources7e66249