AI and the Future of Math, with DeepMind’s AlphaProof Team

**Sarah** (0:06)
Hi, listeners, and welcome to No Priors. Today, we have Thomas Hubert, Rishi Mehta, and Lawrence Sartrand from DeepMind's AlphaProof Team. AlphaProof is a new AI system that can find and verify mathematical proofs, building on DeepMind's earlier successes in chess and Go to tackle one of AI's greatest challenges, mathematical reasoning. In today's episode, we'll explore how AlphaProof works, its implications for math and AI, more about test time RL, and what this reveals about machine learning's capability to reason rigorously. Really happy to have you guys. Welcome.

**Laurent Sartran** (0:38)
Thank you for having us.

**Sarah** (0:40)
Maybe you can start by just talking a little bit about your backgrounds and how you came to be working on AlphaProof together.

**Rishi Mehta** (0:45)
I'm Rishi. I was one of the tech leads on AlphaProof. I've been working in computer science and machine learning for a while. I'm a chess player and I came across the AlphaZero paper and saw some of the chess games that that agent produced and I found it really inspiring. I thought this is the kind of thing I need to work on. Coming up with something beautiful and superhuman, and almost alien, felt magical. I came over to DeepMind and the AlphaZero team, which Thomas was leading, was working on math, and that's how I got into math.

**Thomas Hubert** (1:14)
My background, I started working in industry in my early career. I worked on the minute detection of computer networks. I worked on ad targeting and switched to AI research. And there, a constant interest of mine has been systems that can span more computes to either tackle harder problems or to think more, and math seems to be a perfect domain for that.

**Laurent Sartran** (1:42)
Yeah, on my side, I was actually a Go player. So instead of doing programming since the age of 10, I was actually playing golf. And I played a lot of go during my youth. And then at some point, it was also my dad's dream to build a computer go program. And so I was kind of figuring out what do I need to know to be able to build a computer go program, and then I realized that maybe it was being built at that time. And so that's how I discovered DeepMind and how I discovered AGI. And that's how I joined the company and have been kind of involved with AlphaGo and AlphaZero, MuZero, this line of work. And recently we had worked on AlphaCode and AlphaTensor. So that's way before Challenge GPT, but we already knew that Transformers were kind of changing a little bit how things were done. And so we found that in math, yes, you could get this perfect verifiability. And with AlphaCode, we realized we can generate a lot of good code. And so it was very natural at that time to think about what the potential there was for mathematics.

**Sarah** (2:49)
Can you contrast, so maybe just as context, like for any listener who wasn't a super cool mathlete like me, IMO is the sort of oldest, most prestigious math competition for young people. There's a set of six problems. They feel impossibly hard and AlphaProof had this really amazing results of solving four of the six problems this year. Can you talk a little bit about math and the IMO in particular as a problem relative to game playing and other search problems like chess?

**Laurent Sartran** (3:23)
I think first there is a big difference is that in board games, you play against someone and that's a lot of fun in the board games. For instance, when we did this AlphaGo or AlphaZero algorithms, we could really have this thing about self-play. You could always play against someone who is exactly just your strength and that proved to be a powerful idea. When you're trying to learn to do maths, in some sense, you don't really have an opponent, you just have to think about it. Mass is a bit special in the sense that it's almost like a purely cognitive thing where you can just, the only thing you can do is to think more. Maybe you can't really go into the real world and run an experiment. I guess mathematicians says that sometimes it's a good thing to take a nap and that your unconscious self can think about the problem and there's a good way to come up with new ideas. But it's a lot about thinking. When you're confronted with a really hard problem, there's a whole question about how do you go and try to solve it.

**Sarah** (4:23)
Maybe this is a good time to ask you to describe for our listeners, most of whom are technical or somewhere in the tech field, but also a broader business audience. How does AlphaProof work overall architecturally?