In July 2024, Google DeepMind announced that AlphaProof and AlphaGeometry 2 had solved four of six problems from that year's International Mathematical Olympiad, reaching silver-medal level for the first time. Impressive, but the system took days to compute each solution and required translating problems into a formal programming language before it could reason about them at all.
Twelve months later, in July 2025, Demis Hassabis announced on X that a more advanced version of Gemini with Deep Think had solved five of the six 2025 IMO problems, scoring 35 out of 42 points. The IMO President, Prof. Dr. Gregor Dolinar, confirmed: "We can confirm that Google DeepMind has reached the much-desired milestone, earning 35 out of a possible 42 points. A gold medal score." The system worked entirely in natural language, end-to-end, within the standard 4.5-hour contest window.
One year. Silver to gold. The technical gap between those two results is where things get interesting.
Why mathematics is the right proving ground for reinforcement learning
Reinforcement learning is a training approach where an agent learns by taking actions in an environment and receiving a reward signal. The model doesn't learn from labeled examples. It learns from trial, error, and iterative improvement against a feedback signal.
The hard part in most RL applications is defining a reliable reward. In game-playing, the reward is obvious: win or lose. In most real-world domains, it isn't. You need either a human evaluator (expensive and slow) or a verifier that can check correctness automatically (rare).
Mathematics is one of the few domains where that verifier exists naturally. A proof is either correct or it isn't. There's no partial credit ambiguity at the logical level, no need for human judgment on whether the reasoning "seems right." This is what makes formal proof assistants like Lean so valuable for RL research.
In Lean, proofs are composed of short, discrete steps called tactics. The system checks each step programmatically. If the proof compiles, it's correct. That verification step is essentially free. No human in the loop, no hallucination possible at the output. The reward signal is exact and automatic, which is what RL needs to function at scale.
AlphaProof: the AlphaZero approach applied to formal proofs
AlphaProof is Google DeepMind's RL-based system for formal mathematical reasoning. It couples a pre-trained language model (based on Gemini) with the AlphaZero reinforcement learning algorithm, the same one that previously mastered chess, shogi, and Go.
The analogy to board games is more than cosmetic. In chess, the agent explores a tree of possible moves and receives a win/loss signal at the end. In formal proof search, the agent explores a tree of possible tactic applications inside Lean and receives a verification signal when a proof closes. The structures are similar enough that AlphaZero's approach transfers.
The data problem was harder. Formal mathematical proofs written by humans are scarce. The mathematical community has been formalizing proofs in Lean for years, but the total corpus is small compared to what RL systems typically need. AlphaProof addressed this with a large-scale auto-formalization pipeline.
A fine-tuned Gemini model translated approximately 1 million natural language math problems into Lean statements. The translation didn't need to be perfect. Even an imperfect translation produces a syntactically valid, machine-checkable mathematical proposition. From those 1 million source problems, the pipeline generated roughly 80 million formalized problems. That's the training dataset. Nothing at that scale had existed before.
AlphaProof's 2024 IMO performance showed what this approach could do. It solved the algebra problem from IMO 2024 (P6), a problem that only 5 of 609 human contestants solved correctly. The catch: the solutions took far longer to compute than the contest's time limits would allow, and every problem required translating from the original natural language statement into Lean first.
The hallucination problem and why formal languages address it
Natural language models, even strong ones, can produce mathematical reasoning that looks correct but isn't. The model generates fluent prose that follows the surface conventions of a proof but contains logical gaps or outright errors that only become visible on careful inspection. In mathematics, a plausible-but-wrong proof is worse than no proof at all, because it can mislead.
Formal languages like Lean make that failure mode impossible at the proof level. Every tactic is checked. The proof either closes or it doesn't. There's no way to generate a formally verified but logically incorrect proof. The verification is the point.
The downside is that Lean is hard to write in, the corpus of human-written formal proofs is small, and translating natural language problems into formal statements introduces its own errors. AlphaProof's 80-million-problem auto-formalization pipeline was designed to work around that constraint by generating enough training signal from imperfect translations to make the RL training viable anyway.
The Nature paper, "Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning," published November 12, 2025, documents AlphaProof's full methodology and results.
What changed in 2025: Gemini Deep Think and natural language RL
The 2025 result is architecturally different from AlphaProof. Gemini Deep Think operates entirely in natural language. No Lean translation required. It produces full, rigorous solutions directly from the official IMO problem descriptions.
Deep Think incorporates what Google describes as "parallel thinking": the model simultaneously explores multiple solution paths rather than committing to a single chain of thought, then combines the results before producing a final answer. For the IMO, many problems have multiple valid approaches, and a system that can hold several partial attempts in parallel is less likely to get stuck on an unproductive path.
To train this version of Gemini for mathematical reasoning, Google used a curated corpus of high-quality solutions that included not just problems and final answers but also intermediate steps and general hints on how to approach IMO-style questions. The training incorporated reinforcement learning techniques designed to reward multi-step reasoning, problem-solving, and theorem-proving. The model supports a 1-million-token context window and can generate up to 192,000 tokens in a single session. That's enough room to work through the extended, layered reasoning that hard olympiad problems require.
Google also used Supervised Reinforcement Learning (SRL), which reformulates problem-solving as a sequence of logical actions and provides rich learning signals during training. This approach let smaller models learn complex problems that other common training techniques struggle with.
The 2025 approach reflects a broader shift in how labs think about RL for language models. In January 2025, DeepSeek released R1 using RLVR (Reinforcement Learning with Verifiable Rewards), where a simple rule-based verifier checks whether the model's answer matches a known solution. The math domain is particularly clean for RLVR because answers are verifiable without ambiguity. Google's approach to training Gemini Deep Think follows a similar philosophy but applied to the harder challenge of full proof generation, not just final-answer matching.
The practical result: where AlphaProof in 2024 required days of compute per problem and a translation pipeline, Gemini Deep Think in 2025 solved five IMO problems within the 4.5-hour contest window in natural language. That's not just a performance jump. It's a change in the operational character of the system.
What the IMO actually tests, and why the benchmark holds up
The International Mathematical Olympiad has run annually since 1959. Each country sends six pre-university mathematicians. The contest consists of six problems across algebra, combinatorics, geometry, and number theory. Roughly 8% of contestants receive a gold medal. The problems are not computation problems. They require original mathematical insight, sometimes involving proof strategies that professional mathematicians find non-trivial.
That combination is what makes the IMO a meaningful benchmark for AI mathematical reasoning. The problems don't reward pattern matching against a known solution format. They require constructing arguments that are novel within the context of the problem. Scoring 35 of 42 points, with IMO coordinators verifying the solutions, is not a narrow benchmark win. It's a meaningful result.
AlphaProof also produced a notable result on the 2024 algebra problem (P6), solving a question that only 5 of 609 student contestants solved. Solving a problem that almost no human at an elite competition could solve suggests the system is generating genuine mathematical reasoning rather than retrieving or recombining known solutions.
What comes next: the AI for Math Initiative and AlphaEvolve
Google DeepMind's ambitions extend past olympiad competition. Around October-November 2025, DeepMind launched the AI for Math Initiative, partnering with five research institutions including Imperial College London and the Institute for Advanced Study to work on open mathematical problems.
AlphaEvolve, Google's algorithm discovery agent, is already producing results at the research frontier. It tackled over 50 open problems across mathematical analysis, geometry, combinatorics, and number theory. It improved the best-known solutions in 20% of them and produced a new method for matrix multiplication. Matrix multiplication is a foundational operation in computing. Improvements there have downstream effects across nearly every numerical application. The fact that an RL-trained system is producing novel results at that level is significant.
The arc from AlphaProof's 2024 silver to Gemini Deep Think's 2025 gold is a one-year case study in how quickly math-grounded RL can improve when the reward signal is clean, the training data pipeline is well-designed, and the architecture is given room to explore. The IMO was always intended as a milestone on the way to something harder. Based on what DeepMind has built so far, the research agenda past the olympiad looks serious.