I have always believed that advancing mathematics is about empowering mathematicians.
From our earliest days at @GoogleDeepMind, our focus has been on deep collaboration with the mathematical community, pioneering new tools alongside one another to push the boundaries of what’s possible.
From our earliest days at @GoogleDeepMind, our focus has been on deep collaboration with the mathematical community, pioneering new tools alongside one another to push the boundaries of what’s possible.
15
22
398
35,924
Our journey started with a remarkable collaboration with Professor Geordie Williamson from the University of Sydney, Professor Marc Lackenby and Professor András Juhász from the University of Oxford that demonstrated that AI systems can help mathematicians discover new conjectures. This work resulted in the paper Advancing mathematics by guiding human intuition with AI, published in Nature in 2021.
1
0
27
3,664
To further explore how DeepMind can help mathematicians, we organized the DeepMind AI for Maths workshops at the Institute of Advanced Studies at Princeton in 2022 and 2025. Working with mathematicians, we learnt that they would like tools to search over complex structures and prove open conjectures. These insights motivated the development of our optimization and proof agents like AlphaEvolve and AlphaProof.
1
0
24
2,953
The development of AlphaProof was also inspired by the efforts of the formal mathematics community - pioneers like Kevin Buzzard at Imperial College London, and the amazing mathematicians that built Lean's Mathlib (and later CSLib). Formal systems like Lean make AI proofs trustworthy, which is why the community's work matters so much today. To add to this community, we started Formal Conjectures, an open repository of precisely stated open problems in Lean built with the community.
1
1
19
2,286
These resources are at the heart of our proof agents - from the creation of AlphaProof and its silver medal performance at the International Mathematical Olympiad in 2024, to the use of LLM-powered agents like AlphaProof Nexus, which have been used by our collaborators like Gergely Bérczi of Aarhus University to prove research-level results. Our technical paper on AlphaProof Nexus appears in Science today, led by my colleagues @swarat, @gtsoukal, @SergeyShir994, @antonkovsharov and contributions from many other researchers.
Oct 8, 2026 · 6:37 PM UTC
2
1
20
2,696
To say that we are living through a transformational time for mathematics is not an overstatement. AI's growing ability to find proofs coupled with ability to check them quickly due to the pioneering work of the formal mathematics community is leading to remarkable answers. But mathematics will never be "solved": every answer opens up new questions.
In many ways, it is just the beginning - a time to work on asking new and even more important questions than before, and understanding the answers. We look forward to working with the mathematical community in this new era.
In many ways, it is just the beginning - a time to work on asking new and even more important questions than before, and understanding the answers. We look forward to working with the mathematical community in this new era.
1
2
38
2,221
Read about AlphaProof Nexus here: science.org/doi/10.1126/sc…
0
1
0
507