DeepMind coupled language models to Lean and synthetic geometry to solve olympiad problems with checkable proofs.
AlphaGeometry tackled geometry by generating auxiliary constructions; AlphaProof reinforced Lean proving via RL and autoformalization.
The combo showed an exportable template: conjecture in natural language, formalize, search, verify.
That template is the conceptual bridge to later efforts in analysis and PDEs with massive agent assistance.
LLM proof assistants accelerated Lean libraries; mathematicians adopted hybrid human–machine flows.
Science published Google DeepMind’s paper on AlphaProof Nexus on October 8, 2026, describing an agent framework that produces formal proofs verified in Lean and solved 9 of 353 attempted Erdős problems and 44 of 492 open OEIS conjectures.
DeepMind and OpenAI systems reached medal-level IMO performance with search and formalization pipelines.