AlphaProof
Overview
Reinforcement learning–based AI for formal theorem proving. DeepMind's AlphaProof solves IMO problems at silver-medal level; integrates neural theorem proving, retrieval-augmented models, and expert iteration. Generates and verifies proofs in Lean. Trained on millions of auto-formalized problems; uses Test-Time RL for deep adaptation.
Era: 2024–
Proposed at: London, UK (DeepMind)
Formal structure
Domain: Formal proof (Lean); reinforcement learning; expert iteration
Problem → neural search → formal proof → verification
Constraints: Grounded in formal systems; no hallucinated steps
Objective: Autonomous formal theorem proving; AI as mathematical tool