DeepMind Details AlphaProof's Roots in Lean Math Community, Backs Formal Conjectures Repo
pushmeet · x · 2026-10-09
DeepMind's Pushmeet Kohli explains that AlphaProof was inspired by the formal mathematics community — Kevin Buzzard and the builders of Lean's Mathlib — since formal systems like Lean make AI proofs trustworthy.
- DeepMind ran AI for Maths workshops at Princeton's IAS in 2022 and 2025; mathematicians asked for tools to search complex structures and prove open conjectures, motivating optimization/proof agents like AlphaEvolve.
- The team also launched Formal Conjectures, an open repository of precisely stated open problems formalized in Lean, built with the community.
More from Research
- aimotive driving dataset: train labels come from a tracker that sees the future — RexDouglass · 2026-10-09
- Yale-led study finds symbolic structure inside LLM representations — tallinzen · 2026-10-09
- Discrete Diffusion Meetup at COLM: Oct 8, Grand Ballroom — yuntiandeng · 2026-10-09
- Astra 机器人控制实测:Johns Hopkins 深度评测其运动与控制理解 — jmin__cho · 2026-10-09
- Tavily's 93% live-retrieval agent study challenged: prompts were domain-anchored — edwin · 2026-10-09
- Independent researcher's phase-transition AI acceleration model hits all 6 pre-registered prediction windows — sadeyeprophet · 2026-10-09