AI scores a silver medal at the International Mathematical Olympiad

Top-tier high school math has long been the ultimate graveyard for artificial intelligence. While chatbots can effortlessly write essays or debug code, the International Mathematical Olympiad (IMO) requires hours of rigorous, mistake-free reasoning. Current large language models usually hallucinate a convincing lie by step three.

Now, Google DeepMind has cracked the podium. Combining a new reinforcement learning model called AlphaProof with an upgraded AlphaGeometry 2, the lab solved four out of six problems from the 2024 IMO. The system scored 28 out of 42 points, landing right at the top of the silver-medal tier and missing gold by a single point.

How AlphaZero learned Lean

The IMO problems were first manually translated into Lean, a formal programming language for mathematics. Official solutions were then graded by two heavyweights: Fields Medalist Sir Timothy Gowers and Joseph Myers, chair of the IMO 2024 Problem Selection Committee. Both scored the AI solutions with a perfect 7 out of 7 on all four solved problems.

AlphaProof took center stage by tackling two algebra problems and one number theory problem. In fact, it cracked problem six—the hardest challenge on the paper, which only five of the 609 elite human contestants managed to solve. AlphaGeometry 2 handled the geometry question, solving it in a ridiculous 19 seconds flat. Neither system could crack the two combinatorics problems.

Time was another major factor. Human contestants get two sessions of 4.5 hours to wrap up all six problems. DeepMind's systems took anywhere from seconds to up to three straight days of compute to search out a verified proof.

Killing hallucinations with formal code

The secret sauce here isn't just feeding more math textbooks into Gemini. Large language models trained on natural text constantly invent plausible-sounding math that falls apart upon scrutiny.

Instead, DeepMind built a bridge between natural language and formal verification. A fine-tuned Gemini model translated natural-language math problems into Lean code. Once in Lean, AlphaProof searched for logical proof steps using reinforcement learning algorithms derived from AlphaZero. Because the Lean compiler acts as an infallible referee, the model instantly knew if a proof step held up, completely wiping out hallucinations through self-play.

Why it matters

This is a massive milestone for AI reasoning. Proving that AlphaZero-style self-play works in pure mathematics means AI is moving past fuzzy pattern matching into verifiable, airtight logic.

For mathematicians, this shifts AI from an unpredictable toy into a legit research partner. Instead of checking a model's work for hidden math errors, researchers can lean on formally verified assistants to power through grueling, time-consuming intermediate proofs.

That said, don't pack up the chalkboards yet. Humans still had to manually translate the raw contest prompts into Lean before the systems could even boot up. Plus, taking three days on a single problem and completely whiffing on combinatorics shows that combinatoric intuition is still uniquely human. But bridging raw LLMs with hard-coded logic engines looks like the most viable roadmap we have to AGI.