AlphaProof: when Lean became the training signal
The competition milestone that helps explain the later research wave.
Google DeepMind · AlphaProof · AlphaGeometry 2
Start with the question
The problem
Can a system find rigorous proofs of difficult olympiad problems? The challenge combines creative search with exact verification: a plausible argument is insufficient if one logical step is wrong.
01
Learning from formal feedback
AlphaProof combined a language model with reinforcement learning to search for proofs in Lean. Training on formal statements provided an automatic correctness signal. This made theorem proving an environment in which the system could improve through many checked attempts. [1]
02
Read the competition conditions
DeepMind reported that AlphaProof and AlphaGeometry 2 together solved four of the six IMO 2024 problems, reaching silver-medal standard. Experts translated the statements into formal languages, and some runs took much longer than the human contest allows. The two systems’ methods were different; the geometry result should not be described as an AlphaProof Lean proof. [1]
03
What changed the following year
DeepMind’s 2025 gold-standard result used an advanced Gemini Deep Think system operating in natural language. Its announcement explicitly contrasts that setup with the formal-language pipeline of 2024. The newer medal headline is therefore not evidence that the same Lean-based workflow earned gold. [2]
Inspect the evidence
The Lean formalization
Published Lean proofs with an interactive proof-state viewer
DeepMind’s solution gallery displays the AlphaProof Lean code, lets readers inspect tactic states, and offers the Lean files for download. Its notes distinguish human-written statement translations and explanatory comments from agent-generated answers and proofs. The geometry solution uses AlphaGeometry’s separate system.
Open the Lean project ↗Sources & further reading
Reviewed 9 Sept 2026. X permalinks were recovered from indexed posts and linked discussions; direct X pages were not consistently accessible. They document the conversation, not proof correctness.
- 1.
- 2.
- 3.
- 4.