AlphaProof Paper

Thu 13 November 2025

I'm very excited to finally be able to share more details about how AlphaProof works! AlphaProof is the system that we used to discover the Lean proofs for the International Mathematical Olympiad 2024, reaching silver medal performance. Our full paper Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning has now been published in Nature.

: The work described was done from the beginning of 2022 to July 2024, while I was still at Google DeepMind.

The International Mathematical Olympiad

The International Mathematical Olympiad, or IMO for short, is a yearly contest in mathematics amongst the 6 ...

The Strong Turing Test

Thu 08 February 2024

In the conventional Turing test (aka imitation game), an investigator tries to distinguish between a human and a computer solely by interacting with them.

This is an interesting setup and has inspired much research, but it doesn't immediately translate into practical usefulness - a computer system may pass as human, but may still not be able to help me accomplish any task.

Instead, I find I'm mostly interested in a stricter variety: in each interaction the investigator chooses a preferred response; the goal of the computer system is to be chosen as the preferred side as many times ...