Alphaproof paper (IMO 2024 Silver) is finally published in Nature [pdf] (www.nature.com)

DeepMind’s AlphaProof, now published in Nature, introduces an AlphaZero‑style reinforcement‑learning agent that discovers formally verified proofs inside the Lean theorem prover. Trained on millions of auto‑formalized problems, the system couples a 3-billion‑parameter encoder–decoder transformer (producing policy and value estimates) with a specialized MCTS-like tree search over Lean tactics. The environment models proving as an RL task (states = Lean tactic states, actions = tactic strings, reward = −1 per tactic) and uses a novel return definition (minimum over subgoals) to handle parallel proof branches. For hard problems AlphaProof applies “Test‑Time RL,” generating and learning from millions of related variants at inference to adapt deeply to each instance. Significance: AlphaProof substantially improves state‑of‑the‑art results on elite competition math and—together with AlphaGeometry 2—solved three of five non‑geometry problems at the 2024 IMO (including the hardest), reaching a computation‑heavy performance comparable to an IMO silver medalist. Unlike LLMs, proofs produced are mechanically checked by Lean’s kernel, giving guaranteed correctness. The work demonstrates that large‑scale experiential RL in a verifiable formal environment can produce complex, reliable mathematical reasoning, but it remains compute‑intensive and dependent on auto‑formalization pipelines. This bridges provable verification and learned search, opening paths toward trustworthy AI assistants for formal mathematics.