2025

Thomas Hubert, Rishi Mehta, Laurent Sartran & the AlphaProof team

AlphaProof: formal maths proofs by reinforcement learning

Built AlphaProof, an AlphaZero-inspired agent that learns to find formal proofs in the Lean language through reinforcement learning. With AlphaGeometry 2, it reached a silver-medal score at the 2024 International Mathematical Olympiad. The paper was published in Nature in 2025.

The people

• Thomas Hubert
• Rishi Mehta
• Laurent Sartran

Filed under

• Reinforcement learning
• Science & maths

Key work

Olympiad-level formal mathematical reasoning with reinforcement learning ↗ (opens in new tab)

Nature (Google DeepMind), 2025

Sources

• Olympiad-level formal mathematical reasoning with reinforcement learning ↗ (opens in new tab)
• Paper page, Google Research ↗ (opens in new tab)