AlphaProof
An AlphaZero-style agent learns to prove competition problems in Lean by reinforcement learning and trains on variants of hard problems.
The loop
- Proposes
Lean proofs, built step by step, for millions of auto-formalized problems
- Judged by
The Lean proof assistant, which verifies every proof
- Steers
Verified outcomes train the model; for hard problems, test-time RL learns from millions of related variants
Headline result
At IMO 2024 the system with AlphaProof as its core engine solved three of the five non-geometry problems, including the hardest one; combined with AlphaGeometry 2 this reached a score equivalent to a silver medallist, with multi-day computation.
What this does not prove
Problems were formalized into Lean before the system worked on them, and the paper reports multi-day computation, so this is far from a competition-time-limit result. The Nature paper's claim is the RL method; the medal-level score is the combined system.
How it generalizes the harness
Lean's verdicts train the model by reinforcement learning, including at test time on problem variants, and the output is a machine-checked proof.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | AlphaZero-inspired agent trained on millions of auto-formalized problems |
| Algorithmic authority | Lean proof assistant |
| Feedback | Reward signal |
| What gets updated | Model weights and search tree |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |