A proof the computer can verify
A fluent explanation can hide a logical gap. AlphaProof works inside Lean, a formal system that checks every allowed proof step. The model proposes tactics, Lean updates the remaining goals, and an invalid step cannot be accepted as a proof. [1]
The system learned through reinforcement learning on millions of automatically formalized problems. For especially difficult questions, it generated related variants and continued learning during the search for a proof. [1]
Four problems across two systems
At the 2024 International Mathematical Olympiad, AlphaProof solved three of the five non-geometry problems, including the hardest problem in the competition. AlphaGeometry 2 solved the geometry problem. Together they received a score equivalent to a silver medal. [1]
This was not the same task faced by a contestant. People first translated the problems into formal language, and the systems used multiple days of computation rather than the competition's four-and-a-half-hour sessions. [1]
Formal correctness is powerful and narrow
Lean can verify the final proof once the statement and required mathematical library are formalized. It does not verify that the formal statement perfectly captures the original natural-language question. [1]
Olympiad problems are difficult but deliberately self-contained. The result does not show that the system can choose important open questions, build a new theory or explain a proof well to a mathematician. It does show progress in searching a large space while receiving exact feedback about correctness. [1]
Sources & context
One system paper reporting formal proof results from the 2024 competition.
Olympiad-level formal mathematical reasoning with reinforcement learning
Hubert and colleagues · Nature · November 12, 2025