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).¹² 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.³⁴

History

• 14.12.2023Google 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”.⁵ ¶ cza2rk877
• 25.07.2024DeepMind’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.¹ ¶ cpmp95wjd
• 14.05.2025DeepMind’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%.⁶ ¶ cz2yux3ij
• 19.07.2025OpenAI announces that its experimental reasoning model achieved “gold medal-level performance” at the olympiad.⁷ ¶ ccp7fkcq7
• 21.07.2025DeepMind’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”.⁸ ¶ c4xkfkcjr
• 08.09.2026OpenAI 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.⁹ ¶ cfknhmsr6
• 08.10.2026Science 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”.¹⁰ ¶ ckdzaxmkz

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”.¹¹ ¶ c6575vwd8

Data

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!”¹³ ¶ cydu4nn57

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”.¹⁴ ¶ c6fm7zxay

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.¹⁵ ¶ cdpxcquac

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.¹⁶ ¶ czth2y863

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.”⁴ ¶ cxrzjmjxp

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.”³