Pushmeet Kohli shares Google DeepMind's AlphaProof Nexus results: agentic proof search in Lean
VP of Research Pushmeet Kohli points to a GitHub trove of Lean-formalized proofs and prose by AlphaProof Nexus, signaling progress while holding back the framework code.
By Ryan Merket · Published
Why it matters
Agentic proof search that produces machine-checkable Lean proofs points to a path for trustworthy AI in math-heavy domains. Even without code, verified artifacts let builders gauge real capability and integration potential. For operators, it is a signal that formal systems may become core infrastructure for reliable AI reasoning.
Pushmeet Kohli revealed AlphaProof Nexus results from Google DeepMind in a thread on X, pointing to a public repository of formal Lean proofs the system discovered alongside prose explanations. The artifacts live in google-deepmind/alphaproof-nexus-results.
Kohli, Vice President of Research at Google DeepMind and head of its Science and Strategic Initiatives Unit, has been one of the lab's public-facing voices on AI-for-science. Google DeepMind itself is the post-2023 merger of DeepMind and Google Brain inside Alphabet, a consolidation aimed at pushing large-model research and scientific applications under one roof, as chronicled on Wikipedia.
"See the formal proofs (in lean) discovered by the AlphaProof Nexus agent," Kohli wrote in a thread on X, linking to the results repo.
The repository description is clear about what is on offer today: generated Lean proofs with accompanying natural language prose proofs. As of May 20, 2026, the repo shows light early interest (33 stars, 4 forks, 1 branch, 4 commits) and a latest update titled "Add attempted Erdos problem list."
What is not in the repo is just as notable: there is no AlphaProof Nexus framework code or method paper linked in the materials provided, and no quantitative benchmarks are reported. For now, Google DeepMind is letting the Lean artifacts speak for themselves, which invites the formal methods and Lean communities to validate or critique specific proofs on their merits.
If you are building or investing around AI agents for scientific and technical domains, the release hints at a direction that matters: agentic search wrapped around a formal system with machine-checkable guarantees. Lean has become a focal point for mechanized mathematics; proofs expressed in Lean are either accepted or rejected by the compiler, which makes the results auditable and reproducible in a way that informal math assistance is not.
For founders, the practical read is twofold. First, formal systems are surfacing in the agent stack as a way to bound reasoning, not just generate text. Second, results-first drops like this can seed collaboration: even without code, verified artifacts and prose explanations are enough for domain experts to assess scope, difficulty, and potential integration points. Whether Google DeepMind eventually shares the AlphaProof Nexus framework or publishes formal evaluations remains an open question; the materials shared so far stop short of either.
Google DeepMind has a long track record of putting heavyweight AI against hard scientific problems, and Kohli's unit has been explicit about AI as a tool for discovery. With AlphaProof Nexus, the lab is signaling that research-level math is on that roadmap, and it is starting by letting the community inspect what the agent actually proved, line by line, in Lean.