AlphaProof Paper

Thu 13 November 2025

I'm very excited to finally be able to share more details about how AlphaProof works! AlphaProof is the system that we used to discover the Lean proofs for the International Mathematical Olympiad 2024, reaching silver medal performance. Our full paper Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning has now been published in Nature.

: The work described was done from the beginning of 2022 to July 2024, while I was still at Google DeepMind.

The International Mathematical Olympiad

The International Mathematical Olympiad, or IMO for short, is a yearly contest in mathematics amongst the 6 ...

Discovering Matrix Multiplication Algorithms with AlphaTensor

Wed 05 October 2022

Matrix multiplication is at the foundation of modern machine learning - whether transformers or convolutional networks, diffusion models or GANs, they all boil down to matrix multiplications, executed efficiently on GPUs and TPUs. So far the best known algorithms have been discovered manually by humans, often optimized for specific use cases.

The most famous is probably the Strassen algorithm to multiply two 2x2 matrices using only 7 instead of the naive 8 multiplications:

Through clever addition and subtraction of the individual elements of the a and b matrices this algorithm is ...