Formal Math Reasoning: From Silver to Gold at the IMO
A year after AlphaProof reached silver-medal performance at the International Mathematical Olympiad, Gemini Deep Think hit gold — and produced rigorous proofs in natural language, end to end.
In 2024, DeepMind's AlphaProof and AlphaGeometry 2 solved four of six International Mathematical Olympiad problems — silver-medal level. By 2025, an advanced Gemini model with Deep Think solved five of six and earned a gold medal score of 35 points. The headline number gets attention. The methodological shift is what actually matters.
The architectural change that mattered
AlphaProof in 2024 worked in a formal language (Lean) and used reinforcement learning grounded in AlphaZero. The system was rigorous but operated in a specialized environment that humans had to translate problems into and out of.
The 2025 Gemini Deep Think result was different in two ways that compound: the model worked end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions, all within the 4.5-hour competition window. There was no formalization step. The proofs read like a human mathematician's solution.
That shift — from "AI that proves things in formal logic" to "AI that produces proofs you can read" — is the difference between a research demo and a tool a working scientist might actually use.
Why this isn't about math contests
The reason this matters is not that AI now wins math olympiads. It's that the problems IMO tests for are good proxies for one of the hardest things in cognitive work: chains of reasoning that are long, where every step has to be exactly right, where there's no shortcut, and where wrong answers don't get partial credit.
Most enterprise reasoning work fails on one of those four. Plans that have to hold up over weeks. Audits where every step is checked. Legal arguments where one wrong inference invalidates the conclusion. Models that can do silver-to-gold at the IMO are models that can hold a long, brittle chain of inference and not break it.
What the field is doing with this
Three lines of work matter most heading into late 2026:
-
Formal verification of agent plans. If an agent generates a multi-step plan, can a separate reasoner verify it formally before the agent acts? Early systems are appearing in finance and supply chain — domains where the cost of a wrong action is high.
-
Automated theorem-proving for engineering. Lean is reaching the point where it's a viable assistant for software-correctness proofs in critical systems. This is decades old as a research goal; it's newly tractable as a product.
-
Reasoning trace evaluation. Most LLM evaluation is end-to-end — was the answer right? — which masks reasoning errors that happen to land on the right number. Trace-level eval (was every step correct?) is becoming a standard quality gate, in part because Gemini's Deep Think made trace quality a benchmark category.
The honest limits
Two things still don't scale the way the IMO results suggest they might:
Domain transfer is uneven. A model that excels at olympiad math is not automatically excellent at applied math. Formal proof and applied modeling reward different skills, and the dataset asymmetries are hard to close.
Cost is real. Deep Think uses substantially more compute than standard inference. For most enterprise workloads, the unit economics still don't work — yet. The question for 2027 is whether the cost curve bends fast enough to make rigorous reasoning a default rather than an opt-in.
What it means for builders
If you're building anything that depends on a chain of reasoning longer than three or four steps — agentic plans, due diligence, regulatory analysis — the bet has shifted. A year ago the right answer was "use the model and verify with a human." The 2026 answer is closer to "use the model, verify with a separate reasoner, escalate to a human only on disagreement." That's not a small difference.