AI mathematical proving at Olympiad level
Demostración matemática por inteligencia artificial a nivel de Olimpiada (AlphaProof, FunSearch)
- Date
- 2024-2025 · confidence high
- Place
- London (Google DeepMind), United Kingdom
- Credited to
- Google DeepMind (AlphaProof and AlphaGeometry 2, 2024; FunSearch, 2023); OpenAI and DeepMind systems reaching gold-medal level at the 2025 IMO
- Field
- Knowledge & symbols
⚠️ Disputed: the sources disagree.
What was discovered
AI systems that solve International Mathematical Olympiad problems with proofs verified in Lean (silver in 2024, gold in 2025) and that discover new constructions, such as a better lower bound in the cap set problem (FunSearch). The start of AI-assisted mathematical discovery.
It is debated how much of the mathematical credit belongs to the systems; the 2025 results are recent, and their scope for real research is still being assessed.
What it led to
- human-AI collaboration in mathematical research
- automated formalisation
- new combinatorial results
Built on
- Lean formalization: Liquid Tensor Experiment2022
- Lean and mathlib
- AlphaGo and reinforcement learning
- automated theorem proving
Made possible
- mathematical research assistants