AlphaProof

What it is

AlphaProof is a reinforcement-learning system for formal mathematical reasoning, announced by Google DeepMind on 25 July 2024.^[1] It proves mathematical statements in Lean, a formal language in which a proof is written as a sequence of steps precise enough for a computer to check. The practical consequence is that a proof produced by the system can be verified mechanically: the checker either accepts the argument or rejects it, without anyone having to decide whether the reasoning is convincing. That is why formal proof has long been an attractive target for automated reasoning — success or failure is unambiguous.

How it works

AlphaProof pairs a pre-trained language model with the AlphaZero reinforcement-learning algorithm.^[1] The two parts do different jobs. A fine-tuned Gemini model translates natural-language problem statements into formal statements, and running that translation across many problems creates a library of formal problems of varying difficulty.^[1] That library is the material the prover practises on. Reinforcement learning, broadly speaking, trains a system by trial and error, strengthening the choices that lead to a desired result; here the desired result is a proof the Lean checker accepts, and the system improves by finding such proofs and reusing the lines of attack that produced them.

For the Olympiad, AlphaProof was trained by proving or disproving millions of problems over several weeks before the contest.^[1]

At the 2024 Olympiad

The International Mathematical Olympiad sets six problems, each worth seven points, for a maximum of 42.^[1] Before the system attempted them, human experts translated the problems into formal language.^[1] AlphaProof solved two algebra problems and one number-theory problem, including the hardest problem in the competition.^[1] Together with AlphaGeometry 2, a second system reported alongside it, it reached the same level as a silver medallist, scoring 28 of 42 points.^[1]

Scoring

The solutions were scored under IMO point rules by Prof Sir Timothy Gowers and Dr Joseph Myers.^[1] The marks therefore followed the convention used for human contestants, with mathematicians assessing whether an argument holds up, rather than a score being read off directly from the formal checker.

Where it sits

AlphaProof belongs to a line of work that treats proof search as a learning problem inside a formal language, rather than as the generation of ordinary mathematical prose. The division of labour is visible in the design: a language model reads the problem and restates it in Lean, and a reinforcement-learning prover then searches for a proof.^[1] What the 2024 result did not remove is the translation step, which was carried out by human experts before the system started work.^[1] The problems were also translated one by one, ahead of the attempt, rather than handed over in their original wording.

The result is best read as a measurement of where formal automated reasoning stood on a set of problems written for young mathematicians under exam conditions: three solved problems out of six, scored by hand under the same rules as the human competitors.^[1] A Nature article describing AlphaProof's methodology was published on 12 November 2025.^[1]