# AlphaProof AlphaProof is the [[Google DeepMind]] system for formal mathematical reasoning. Announced in July 2024, it uses a [[Gemini]]-family model to translate natural-language math problems into the Lean theorem prover, then searches for formal proofs using AlphaZero-style reinforcement learning. ## IMO 2024 result AlphaProof, working together with [[AlphaGeometry]] 2, solved 4 of the 6 problems from the 2024 International Mathematical Olympiad, reaching the score threshold for a **silver medal** (28 points out of 42). Problems included two algebra, one number theory, and one geometry. The system was a demonstration run, not a competition entry; it also took substantially longer than the human time limit on some problems. ## How it works - **Autoformalization**: a fine-tuned Gemini model translates informal math problem statements into Lean - **Proof search via RL**: the system explores candidate proof steps in the Lean environment, trained via AlphaZero-style self-play on ~1 million problems autoformalized from corpora - **Verification by Lean**: every output is a Lean-checked proof, so correctness is provable, not merely plausible ## Why it matters - First AI system to approach elite human performance on formal mathematics - Demonstrates the "LLM proposes, formal system disposes" pattern at high stakes: the LLM generates candidates, Lean verifies - Pairs naturally with [[AlphaGeometry]] (for synthetic geometry) to cover the full IMO problem distribution - Reinforces the [[AlphaFold]] thesis: pair general deep learning with domain-specific verification and you unlock previously out-of-reach scientific problems ## Caveats - Solved 4/6 problems, not 6/6; the unsolved problems include the hardest combinatorics - Per-problem compute time was well beyond human contest limits - Requires autoformalization, which remains imperfect for harder natural-language prompts ## References - Official announcement: https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ - International Mathematical Olympiad 2024: https://www.imo-official.org/year_info.aspx?year=2024 ## Related - [[Google DeepMind]] - [[AlphaGeometry]] - [[AlphaZero]] - [[Gemini]] - [[Artificial Intelligence (AI)]]