Capability benchmark · Mathematics · Computer science

AlphaProof uses reinforcement learning for formal mathematical proofs

Lean-verified formal proofs found for hard competition mathematics problems.

Summary

The Nature paper presents AlphaProof, an AlphaZero-inspired system that learns to find Lean-verified formal proofs through reinforcement learning on millions of auto-formalized problems. At the 2024 International Mathematical Olympiad, AlphaProof solved three of five non-geometry problems; combined with AlphaGeometry 2, the system reached a silver-medal-equivalent score.

AI role

Used reinforcement learning over auto-formalized problems to search for formal proofs.

Narrative role

AlphaProof is a bridge between AI math benchmarks and verifiable mathematical output, making it important for the proof-search timeline.

Caveat

Competition problems are not equivalent to open research, and auto-formalization itself is a constraint.