Mathematics
Olympiad gold, and first contributions to open problems.
Language models have moved from textbook exercises to competition-level proofs. Systems that pair a model with an automated evaluator have improved results on problems that stood for decades, and formal proof languages such as Lean make machine-generated proofs checkable.
Milestones
Jul 21, 2025
Two AI systems reach gold-medal standard at IMO 2025
Models from Google DeepMind and OpenAI each solved five of six olympiad problems, writing natural-language proofs within the competition time limits.
Google DeepMindMay 14, 2025
AlphaEvolve improves on a 1969 matrix multiplication result
An evolutionary coding agent found a way to multiply 4×4 complex matrices with 48 scalar multiplications, improving on Strassen's algorithm for this case.
Google DeepMindJul 25, 2024
AlphaProof and AlphaGeometry 2 reach IMO silver-medal standard
The systems solved four of six problems from the 2024 International Mathematical Olympiad, scoring 28 of 42 points.
Google DeepMindDec 14, 2023
FunSearch finds new constructions for the cap set problem
A language model paired with an automated evaluator found larger cap sets than any previously known, a new result on an open problem in combinatorics.
Nature