The Exchanges

Q Maybe this is a good time to, 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. Like, you know, how, how does Alphaproof work overall architecturally?

A Uh, yes, sure. So, um, AlphaProof is based on this thing called AlphaZero. So maybe let me start there. AlphaZero has this program we developed to, you know, like be basically kind of solve kind of perfect information board games. Um, and, um, and the way it works is, is, is also based on a reinforcement learning algorithm. So you can think of AlphaZero as maybe three components, like, uh, one, a neural network, uh, two, kind of, uh, large scale reinforcement learning, uh, basically learning from trial and, uh, trial and errors. And, and three, it also has like this planning and kind of search component to it, to try to, given the current situation, trying to search for kind of the best answer. Um, and, uh, it turned out that, you know, like maybe we weren't very imagining that when we were doing chess, but if you can handle kind of infinite action spaces, uh, then, you know, instead of kind of looking for a chess move, you can look for, for instance, a line of a proof. Um, and so that's what we, we tried to do when we, we, we started off a proof. It's basically, can we look, can we, our action space is to generate lines of proofs, uh, and, and maybe very importantly, we used a formal language to do that. So basically, uh, another way to say that is we use kind of code to write maths, uh, and it's become quite popular recently. Um, and, and the, the advantage of that is that on…

AI assessment note: “AlphaProof is based on this thing called AlphaZero... our action space is to generate lines of proofs”

Q the, um, sort of oldest and most prestigious math competition for young people. Uh, there's a set of six problems. They feel impossibly hard and Alphaproof had this, um, really amazing results of solving four of the six problems this year. Uh, can you talk a little bit about, um, Uh, math and the IMO in particular as a problem relative to game playing and other search problems like chess?

A I think, you know, like first there is a, there is a big difference is that in board games you, you play against someone, uh, and that's a lot of fun, uh, in, in the board games. And, and for instance, when we did this AlphaGo or AlphaZero algorithms, uh, we could really have this thing, uh, this, this, this thing about self-play. You could always play against, uh, someone who is exactly just your strengths. Uh, and that, that proved to be a powerful idea. Uh, when you're kind of trying to learn to do math, in some sense, you know, you, you don't really have an opponent. Uh, you just have to, to think about it. And, and math is a bit special in the sense that it's like, it's almost like a purely cognitive kind of thing where you, you can just, you know, the only thing you can do is to think more. Uh, you know, you're, maybe you can't really go into the real world and run an experiment. Um, I guess mathematicians says that, you know, sometimes it's a good thing to take a nap and that your unconscious self kind of think about the problem and, That's a good way to come up with new ideas. It's a lot about thinking. And so, you know, like when you're confronted with a really hard problem, there's a whole question about how do you go and try to solve it.

AI assessment note: “in board games you, you play against someone... when you're kind of trying to learn to do math... you don't really have an opponent”

Q mathematician forward in their own research. Um, you know, often when somebody proves something now, if they're in a more side field, there aren't that many people who can actually verify or check the proof that they've done. How many mathematicians have access right now to alpha proof, or how do you think about engaging with the mathematics community about day-to-day usage of this pretty amazing, um, set of advancements?

A So at the moment, you know, like mathematicians don't have access to alpha proof. And, and to be honest with you, you know, like kind of we, at the moment we can't rival at all with, with someone like Terry Tao. Um, we, I think we, we demonstrated that what we've demonstrated is that we can learn general mathematics almost from scratch and, and arrive at kind of an impressive high school level. Uh, and then we, we need to grow our knowledge base so that we become useful. Um, but I don't know if you've seen kind of, um, Terry Tao's kind of recent kind of interviews over the last year. And he's been saying that, you know, one, one thing that, uh, that is interesting in math is that collaborations has been relatively small. A lot of papers are one, two author paper and max five authors. And it's been because it's been very hard to collaborate with more mathematicians because you need to check what they are doing. And so it's very time consuming. But if you instead relied on a formal system to check everyone else's work, then You could do a little bit like in astronomy where you could have, um, an amateur kind of living in the middle of maybe nowhere and you, you've never met. And then you wouldn't have to trust him. Like you could trust in some sense the, the, the, the machine to check the work. And if he's, the machine says it's, it's a correct proof, then it's a correct proof. A…

AI assessment note: “So at the moment, you know, like mathematicians don't have access to alpha proof.”

Q different ways in cryptocurrencies, you know, um, Group theory and algebra propped up in quantum mechanics over time and was sort of developed beforehand and then applied and developed further there. Um, are there specific areas that you're most excited about from an applications area for some of the work that you're doing, or is it mainly, um, doing it for the, the love of the theoretical part of it?

A It's a good question. I think we can maybe, you know, maybe the answer depends on, on each one of us. I think one thing that I have been motivated about is to learn from mathematicians, you know, what they are interested in and what they find interesting in the current, you know, uh, world of mathematics. And so for instance, you know, I've been reading about this thing called the Lang Langs program that is trying to connect, uh, different areas of math. And it was described to me a little bit as kind of, You know, just, just like in physics, where you're trying to look for this unified theory of physics, it's like trying this unified theory of mathematics, where maybe, you know, we have number theory here and we have like geometry there and, and, but maybe there is kind of something behind that, you know, that is more unifying. Um, so I, I personally like those abstract ideas, uh, even though maybe I don't understand them very well. Um, but yeah, I'd be, I'd be very motivated to just see, you know, like kind of what mathematicians Care about and, uh, and they might disagree between themselves as well.

AI assessment note: “I personally like those abstract ideas, uh, even though maybe I don't understand”

Q So I guess, I think it was 1900 when David Hilbert posed his famous 23 problems that kind of defined a lot of the, the big areas that at the time he felt were important to mathematics and the sort of unsolved things that were important or topical. Or is there some Turing test equivalent, I guess, as a general, generic question?

A It's an excellent question, um, that, that totally defined kind of, you know, like the mathematics in, in the, in the 20th century, and maybe, you know, the millennium problems, uh, you know, the seven millennium problems of which, you know, one has been solved so far, uh, is, is another attempt at defining kind of what, you know, what could be one trajectory of, of mathematics for the, for the 21st century. What are our chances of solving that, that's like, kind of, That's like a really hard question because we know, you know, our brain kind of thinks linearly and, but we know from our experience in working on the AI that we should actually try to think exponentially. Uh, things might, might change pretty quickly. Um, at the same time, you know, like, I think we have no idea how hard maybe something like the Riemann hypothesis is. Is it, you know, is it, is it two orders of magnitude, three orders, maybe it is like 10 orders of magnitude away from what we can do, right? Uh, because we don't have an existence kind of proof, it's, it's much harder to kind of, uh, have an estimate of, of how hard this actually is. But I imagine that, you know, solving that problem will involve, like, kind of creating brand new maths, brand new theories, and things like this. So if we want to take our proof all the way there, I think that's a capability we, we need to, um, either it emerges, it's …

AI assessment note: “the seven millennium problems... is another attempt at defining kind of what”

Q be curious if any of you have, um, problems you want to work on. Another is the premise that, like, this sort of advancement in reasoning will allow us, it will transfer to other domains, um, be they, you know, science or what we think of as more, like, language-based, like, less verifiable non-code Non-rules based domains as well. Um, where do, where do you all want to take this?

A I'm not really a mathematician, so I didn't have like a problem I absolutely wanted to solve, but it's been my favorite subject when I was, when I was a student. Um, and I think, yeah, you're absolutely right. There are like, you know, at least two kind of main reasons why you would want to potentially spend a lot of time on math. One is that I guess it's been described as the language, the language of the universe. And, you know, it's been extremely powerful to both, you know, describe and predict the natural world and of course to shape it. And you see that, you know, basically we, we see mass being at the core of all the technology we are using now. So kind of having a good understanding of mass is probably kind of, uh, very important to understand our current world. And then of course you could, as you, as you alluded to, make an argument that, you know, kind of Solving math or, you know, like, which requires, you know, reasoning, generalization, abstraction, all these things that we, we think about when we're talking about something like a cognitive HGI, um, would be, would be, is, is a path to, you know, go towards HGI and that could really help in kind of the development of HGI. So I think at least for me, you know, um, these are maybe the two main reasons as to, you know, why math, uh, is a particularly interesting, you know, topic to try to solve it. In a general way, …

AI assessment note: “I'm not really a mathematician, so I didn't have like a problem I absolutely wanted to solve”