--- title: AI in mathematics url: https://ftrlg.com/en/wiki/ai-mathematics/ lang: en published: 2026-10-11 version: 2 summary: AI systems that prove theorems and solve olympiad and research problems. In three years: from olympiad silver to hundreds of manuscripts. cite_as: "future.log, «AI in mathematics», https://ftrlg.com/en/wiki/ai-mathematics/" license: CC BY 4.0 https://creativecommons.org/licenses/by/4.0/ --- # AI in mathematics **AI in mathematics** refers to artificial intelligence systems that prove theorems, solve olympiad and research problems, and check proofs. The formal language Lean plays a key role: a proof written in it is checked by a computer, so an AI result can be verified without trusting the model itself. In three years the field went from olympiad silver-medal level (2024) to hundreds of manuscripts with new results (2026).[^2][^9] Mathematicians reacted with both excitement and alarm: Terence Tao says “we are now entering an era of proof abundance in mathematics”, while the International Mathematical Union endorsed a declaration that mathematics must remain a human endeavour.[^11][^12] ## History - **14.12.2023** [Google DeepMind](https://ftrlg.com/en/models/google-deepmind/) publishes the FunSearch system in Nature: a language model paired with automated evaluation found “new constructions of large cap sets going beyond the best-known ones”.[^1] - **25.07.2024** DeepMind's AlphaProof and AlphaGeometry 2 systems “solved four out of six problems” at the International Mathematical Olympiad, reaching “a final score of 28 points”, silver-medal level; the system “solved one problem within minutes and took up to three days to solve the others”. AlphaProof “couples a pre-trained language model with the AlphaZero reinforcement learning algorithm” and proves statements in Lean.[^2] - **14.05.2025** DeepMind's AlphaEvolve “found an algorithm to multiply 4x4 complex-valued matrices using 48 scalar multiplications, improving upon Strassen's 1969 algorithm”. On more than 50 open problems, the system matched the best known solutions in about 75% of cases and improved on them in 20%.[^4] - **19.07.2025** [OpenAI](https://ftrlg.com/en/models/openai/) announces that its experimental reasoning model achieved “gold medal-level performance” at the olympiad.[^5] - **21.07.2025** DeepMind's Gemini Deep Think officially wins olympiad gold: it “solved five out of the six IMO problems perfectly, earning 35 total points” out of 42, within the 4.5-hour competition time; the result was “officially graded and certified by IMO coordinators using the same criteria as for student solutions”.[^6] - **08.09.2026** OpenAI reports that its internal model proved that a singularity is possible in the Navier–Stokes equations (with external forcing), using about 10,000 agents over 88 hours; the proof is formalized in Lean.[^8] - **08.10.2026** Science publishes DeepMind’s paper on the AlphaProof Nexus agent: it autonomously resolved 9 of 353 open Erdős problems and proved 44 of 492 conjectures from the On-Line Encyclopedia of Integer Sequences (OEIS), with every proof checked in Lean. In the same issue mathematicians Jeremy Avigad and Matthew Ballard write the commentary “AI for research mathematics has arrived”.[^15] ## How it works There are two approaches. In the first, a model searches for solutions in the form of programs or constructions, and an automated evaluator checks whether they beat the known ones: this is how FunSearch and AlphaEvolve work. In the second, a model writes a proof in the formal language Lean, and a computer checks it: this is how AlphaProof works, and so does the Gauss project by Math Inc, which formalized the strong form of the prime number theorem, a challenge set by Tao and Alex Kontorovich in January 2024; Math Inc says “we have completed the project after three weeks of effort”, producing “~25,000 lines of Lean code”.[^13] ## Data | study | what was measured | result | |---|---|---| | Epoch AI, FrontierMath, 07.11.2024[^3] | new hard problems at the level of research mathematics | “Current state-of-the-art AI models solve under 2% of problems” (**under 2%**) | | [OpenAI](https://ftrlg.com/en/models/openai/), 06.10.2026[^9] | results of an internal model published on GitHub; the company's own estimate | **719** manuscripts in 372 groups, about 4,000 posed problems; “The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking.” Three manuscripts were soon withdrawn because of a sign error | > **[EDITORS' CONCLUSION]** In two years AI went from “under 2%” on research problems and olympiad silver to hundreds of manuscripts with new results. Verifiability is what sets mathematics apart from other fields: a proof in Lean is checked by a computer, so the limit on AI's pace here is not trust in the model but people's ability to understand and absorb the results. Caveats: some claims are the companies' own internal estimates, and OpenAI's most striking results come from a model that cannot be checked from outside. ## Criticism In October 2025 researchers announced that with GPT-5 they had found solutions to 10 Erdős problems listed as open. Thomas Bloom, who maintains the erdosproblems.com database, called the framing “a dramatic misrepresentation”: GPT-5 had found already published papers with solutions that he personally did not know about. “The 'open' status only means I personally am unaware of a paper which solves it.” In his words: “Its literature searching ability is already useful and impressive enough, no need to describe it as something it's not!”[^7] After OpenAI's release, The Verge spoke with more than three dozen mathematicians; Bartosz Naskręcki said: “It can cause a huge collapse in the academic culture”.[^10] On 13.10.2026 Scientific American reported that mathematicians who worked through OpenAI’s 166-page Navier–Stokes proof found it builds its external force in a totally distinct way from the program of the Spanish mathematicians Diego Córdoba and Luis Martínez-Zoroa — although at release company officials “clearly and repeatedly stated” that it followed that program.[^16] Timothy Gowers named his main fear about AI in mathematics as “the possible destruction of mathematical culture”: knowledge and experience that exist not only in the literature but also in mathematicians' heads.[^14] ## Evolution On 02.06.2026 the Leiden Declaration on Artificial Intelligence and Mathematics was published and endorsed by the International Mathematical Union: “Credit and responsibility continue to belong to humans within the mathematical community and should not be given to automated systems.”[^12] Tao proposes to stop blindly chasing problem-solving: in an era of proof abundance, he writes, “Further blind optimization of problem-solving alone is now actively harmful to the long-term health of mathematics.”[^11] ## Signals - 2026-10-12 — Jack Clark: «We've seen both a tremendous advancement in the ability for AI systems to make creative-seeming math breakthroughs … I now think it's more likely we'll see full RSI become possible in 2027, whereas before I thought it was more likely in 2028» — Anthropic co-founder, in his Import AI newsletter, on a benchmark of models’ research taste; in May he put at 60% the chance that by the end of 2028 a model could train its own successor on its own (https://ftrlg.com/en/signals/csfrbwmzs/) - 2026-10-09 — Terence Tao: «We are now entering an era of proof abundance in mathematics» — in his “Math 2.0” lecture at Caltech, on what AI has done to mathematics (https://ftrlg.com/en/signals/cacw8rarw/) - 2026-10-08 — Hugo Duminil-Copin: «OpenAI’s release of hundreds of AI proofs is a “monumental shock”: for mathematicians “it is the day after”; on one problem it felt like running a marathon with someone on his back who jumped off in the last 100 metres to cross the line first» — French mathematician and 2022 Fields medalist, on Swiss radio RTS after OpenAI published hundreds of manuscripts with AI proofs, 16 of them on problems in his field (https://ftrlg.com/en/signals/cngtgrwz8/) - 2026-05-08 — Timothy Gowers: «To prove something that LLMs can't prove» — a Fields medallist on ChatGPT producing PhD-level research in an hour (https://ftrlg.com/en/signals/c6efm7fk5/) ## See also Reasoning models · [Large language model](https://ftrlg.com/en/wiki/large-language-model/) · Reinforcement learning · [AI agent orchestration](https://ftrlg.com/en/wiki/ai-agent-orchestration/) ## References [^1]: B. Romera-Paredes et al. Mathematical discoveries from program search with large language models — Nature, 14.12.2023. [nature.com](https://www.nature.com/articles/s41586-023-06924-6) [^2]: AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind, 25.07.2024. [deepmind.google](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/) [^3]: E. Glazer et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI — arXiv, 07.11.2024. [arxiv.org](https://arxiv.org/abs/2411.04872) [^4]: AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms — Google DeepMind, 14.05.2025. [deepmind.google](https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms/) [^5]: Alexander Wei: “our latest @OpenAI experimental reasoning LLM has achieved … gold medal-level performance” — X, 19.07.2025. [x.com](https://x.com/alexwei_/status/1946477742855532918) [^6]: Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad — Google DeepMind, 21.07.2025. [deepmind.google](https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/) [^7]: Thomas Bloom: “this is a dramatic misrepresentation” — X, 17.10.2025. [x.com](https://x.com/thomasfbloom/status/1979254235075059732) [^8]: On the Navier–Stokes Millennium Prize Problem — OpenAI, 08.09.2026. [openai.com](https://openai.com/index/navier-stokes-solution/) [^9]: openai/math — OpenAI, GitHub, 06.10.2026. [github.com](https://github.com/openai/math) [^10]: ‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop — The Verge, 09.10.2026. [theverge.com](https://www.theverge.com/ai-artificial-intelligence/1008726/openai-mathematics-solutions-chaos) [^11]: Math 2.0 — Terence Tao, 10.10.2026. [terrytao.wordpress.com](https://terrytao.wordpress.com/2026/10/10/math-2-0/) [^12]: Leiden Declaration on Artificial Intelligence and Mathematics — 02.06.2026. [leidendeclaration.ai](https://leidendeclaration.ai/) [^13]: Introducing Gauss, an agent for autoformalization — Math, Inc. [math.inc](https://www.math.inc/gauss) [^14]: Thoughts about the Leiden Declaration — Timothy Gowers, 26.07.2026. [gowers.wordpress.com](https://gowers.wordpress.com/2026/07/26/thoughts-about-the-leiden-declaration/) [^15]: Tsoukalas et al. Advancing mathematics research with AI-driven formal proof search — Science, 08.10.2026. [doi.org](https://doi.org/10.1126/science.aej2213) [^16]: OpenAI’s blockbuster Navier-Stokes proof isn’t what we thought it was — Scientific American, 13.10.2026. [scientificamerican.com](https://www.scientificamerican.com/article/openais-blockbuster-navier-stokes-proof-isnt-what-we-thought-it-was/) — future.log, «AI in mathematics», https://ftrlg.com/en/wiki/ai-mathematics/ · CC BY 4.0