On January 17, 2024, DeepMind published AlphaGeometry, a neuro-symbolic system for olympiad-level geometry, in Nature. AlphaGeometry pairs a neural language model, which proposes useful geometric constructions, with a symbolic deduction engine that applies formal logic to find proofs. On a benchmark of 30 olympiad geometry problems it solved 25 within competition time limits, close to the average gold medalist’s score of 25.9 and far ahead of the prior best automated method, which solved 10.
In July 2024, DeepMind reported a larger result: AlphaProof, a reinforcement-learning system for formal mathematical reasoning built on Lean and AlphaZero-style search, together with an upgraded AlphaGeometry 2, solved 4 of the 6 problems at the 2024 International Mathematical Olympiad. The pair scored 28 out of 42 points, the same level as a silver medalist - the first time an AI reached that bar across a full IMO. AlphaProof handled three problems in algebra and number theory; AlphaGeometry 2 solved the geometry problem.
What makes these systems notable is that their solutions are machine-verifiable formal proofs, not plausible-looking text. The neural component supplies creative guesses, but every step is checked by a symbolic engine, so a correct answer is genuinely correct rather than merely convincing.
This work is the direct ancestor of the 2025 result in which AI systems reached gold-medal level at the IMO (see 2025-imo-gold-ai). It extends the AI-for-science pattern into formal mathematics, where the prize is not a prediction but a proof.