Latest / Strachey Lectures / Will Computers prove theorems?

Transcript

Will Computers prove theorems? · Strachey Lectures

• 0:01
  [Auto-generated transcript. Edits may have been applied for clarity.] So if you haven't.
• 0:15
  Okay. Um, so now it's my great pleasure to introduce Kevin Hart.
• 0:20
  So Kevin did his PhD in Cambridge in 1995 and algebraic number theory, and he had, uh, positions at Princeton and Berkeley.
• 0:28
  Uh, but since 2004, he has been a professor of pure maths at Imperial.
• 0:33
  He's had some very distinguished prizes. Um, Kevin got the white House Prize, BLM Sydney 2002, for distinguished work in number theory.
• 0:42
  And in 2008 he got the senior price of the LMS, which is for a really outstanding piece of mathematical work.
• 0:50
  In 2017, he kind of turned his attention partly from number theory to formalisation at a midlife crisis.
• 1:00
  Um, for this work, actually, he's given a plenary lecture at the international, um, Congress of Mathematicians in, uh, 2022.
• 1:09
  And in 2024, he started this kind of super exciting project to formalise the proof of Fermat's Last Theorem, which, um, was anticipated here.
• 1:16
  And we're now going to hear about. So, um, he's going to be telling us about whether computers are going to prove theorems.
• 1:22
  Great to have you here. Thank you. So.
• 1:31
  So many thanks for the, uh, for the invitation.
• 1:35
  Uh, and, yeah, I'll do the same joke as Leo. Uh, it's an absolute honour to be giving these lectures, especially, uh, with this,
• 1:43
  this guy who basically has changed my life, uh, not least by writing, you know, forget Nintendo.
• 1:50
  Uh, uh, my my favourite computer game. This is, uh.
• 1:55
  This is summer. I've always loved computer games, but the fact that I can do, you know,
• 2:00
  sort of interesting algebraic number theory in this completely novel way, uh, is something that still blows me away.
• 2:08
  Uh, so I kind of want to think big.
• 2:12
  So, you know, the questions after I finished.
• 2:15
  You know the questions maybe you want to consider, uh, you know, what conformal methods do for me?
• 2:21
  Your your. Yeah. Many of you probably experts in something.
• 2:24
  Uh, well, what can formal methods do in that thing that you're an expert in?
• 2:30
  Uh, and then more generally, you know, what can formal methods do for mathematics?
• 2:34
  Because that's not really formal.
• 2:36
  Methods have existed for decades, but that is not something that mathematicians were asking themselves, uh, ten years ago.
• 2:44
  So these are, I think, two interesting questions. Uh, so that was the title I had to give a title.
• 2:50
  So I wrote Will Computers Prove Theorems? And I mentioned this on social media.
• 2:54
  And immediately some wag says that, you know, any any time you see a title with a question mark, the answer is always no.
• 3:00
  Because if if it wasn't no, you wouldn't put the question mark.
• 3:04
  Uh, so in fact, the answer isn't no. The answer is yes.
• 3:07
  Like, already computers are proving theorems. Uh, and so yes, you get this example, this thing that Leo already mentioned, uh,
• 3:17
  a computer program autonomously solved four out of the six problems on the 2024 International Maths Olympiad.
• 3:24
  Uh, and and of those four, uh, three of them, uh, it gave formal lane solutions.
• 3:30
  So, you know, uh, formally verified, uh, solutions to three of these questions.
• 3:35
  And the other one was the Euclidean geometry question, uh, where the system didn't use Lane,
• 3:40
  it just wrote down, uh, an easily human readable and human checkable proof.
• 3:45
  Um, and so of course, if you're a research mathematician, you would say, well, these aren't theorems, right?
• 3:50
  These are, you know, high school, you know, level problems.
• 3:54
  Uh, they're not really what a mathematician would call it. You know, maybe a push their lemmas, right?
• 4:00
  They're not really theorems. But of course, if you think that it's going to stop there, then I think you're very naive.
• 4:06
  Uh, and so really, what I'm talking about, uh, is how we can, you know,
• 4:11
  how mathematicians and computer scientists can collaborate to take these things further?
• 4:15
  Because this is one thing that really, really shocked me, uh, when I moved into this area, was that even though,
• 4:21
  you know, my background and Leo's background couldn't be more different, I can't write a line of computer code.
• 4:26
  Really. I know very little about, uh, programming languages, and I'm not expecting Leo to know anything about, uh, you know, advanced mathematics.
• 4:34
  And yet mathematicians and computer scientists are finding that they have a common language.
• 4:40
  You know, we we we stuck with the maths problem. We run into something.
• 4:43
  We can't get the system to do it, but we can ask questions which computer scientists can understand and they can give us answers.
• 4:51
  Well, I find this quite, quite striking, uh, and that we can actually communicate with each other,
• 4:57
  uh, and, and, uh, and make progress, even though our backgrounds are very different.
• 5:04
  Uh, this is something that, you know, constantly the fact that I can talk to computer scientists and they can solve my problems,
• 5:11
  uh, even though they don't understand the maths behind it, I understand.
• 5:15
  Yeah, it's a straight is, you know, it's a strange synergy and one that I was very surprised by.
• 5:22
  So yeah, we've got this. Will computers proof theory. It's a very valid question.
• 5:26
  Let's ask a more precise question.
• 5:28
  And you know, the kind of question I'm interested in is how can you technology, uh, your theorem prove as early as talked about.
• 5:35
  But language models you can't really ignore in 2025.
• 5:39
  Uh, can these things actually give mathematicians new general purpose tools?
• 5:44
  Mathematics is a very conservative area.
• 5:48
  Uh, it's really striking when you look at the kind of things that we're teaching the undergraduates in 2025,
• 5:55
  the courses which are offering final year undergraduates in 2025,
• 5:59
  they are essentially exactly the same as the courses that I was being offered, uh, when I was an undergraduate, you know, 30 plus years ago.
• 6:08
  Uh, so mathematicians are very slow to change and adapt, and yet there's all this stuff happening.
• 6:15
  Uh, and the question is, can we actually, you know, can we actually use it to make new tools to use to mathematicians?
• 6:23
  You know, can we accelerate mathematics for me?
• 6:26
  Yeah. For me. You know, I used to think that prove new theorems was the important thing.
• 6:30
  But I think that this some this question really dwarfs that, you know, that that traditional idea of let's accelerate maths by proving new theorems.
• 6:39
  I think there might be other ways of doing things. So what kind of tools am I thinking of?
• 6:45
  What kind of yeah, how are we going to change mathematics?
• 6:48
  How are we going to, uh, how are we going to disrupt mathematics?
• 6:51
  I like the idea of disrupting, uh, so yeah.
• 6:55
  Well, yeah, he's a tool.
• 6:57
  But wouldn't it be great if we had a tool where you just press a button and we can solve, you know, all the great unsolved problems in mathematics?
• 7:03
  That'd be good. That'd be a useful. That's accelerating mathematics.
• 7:07
  So the big problem with that tool is that tool is just, you know, doesn't exist.
• 7:12
  Uh, and it's not just that it doesn't exist. I can't see a path to that tool yet.
• 7:17
  Right. It's it's not just that it doesn't exist, but given what we know.
• 7:22
  So we don't really see how to make that tool exist. There's not really even a route to making that tool exist.
• 7:30
  That's a shame. Uh, so what about. What about another tool?
• 7:33
  Wouldn't it be great? Now? Is this. This is some mathematician's nightmare, right?
• 7:39
  Is this a dream, or is this a nightmare? Wouldn't it be great?
• 7:42
  Wouldn't it be great if we had a tool? You press a button and you got 10 million lines of incomprehensible code that you said.
• 7:47
  Let F1 be this function, F2 be this function.
• 7:50
  Let F3 be this. You know, theorem 398 is that this, this, you know, function 28 and function 374 are related in this way.
• 8:00
  And it just goes on and on and on and on and on. You have no idea what's going on.
• 8:03
  And then at the end, it's the Riemann hypothesis. And you run it through Lane.
• 8:06
  And Lane says, yes, this is correct. You know that.
• 8:10
  You know, that's terrifying for some. Because my what's nice about is it about proving all the theorems or is it about getting understanding,
• 8:18
  you know, different mathematicians have different opinions about that.
• 8:21
  You know, do we just want to get the job done or do we want to understand what's happening?
• 8:26
  So again, that's science fiction, right? There's no route to that yet.
• 8:31
  And so, you know, this that's this is you know, I can't see you know, there's lots of new tools and it's very exciting.
• 8:38
  But these lofty goals here are kind of out of reach at the minute, you know.
• 8:44
  But of course, five years ago getting a point on the IMO was also considered completely out, right?
• 8:50
  Five years ago there were no language models. Five years ago we had Lane.
• 8:55
  We could do Lane. Uh, yeah we could, we could start proving, you know, research level theorems,
• 9:02
  but we couldn't get a point on the IMO, on the International Maths Olympiad.
• 9:07
  So things do move and they're moving pretty fast. Uh, so we don't really know where we'll be in five years time.
• 9:14
  Uh, but, you know, I don't want to just speculate. Let's talk about what's not science fiction now.
• 9:21
  So where are we? What about here we go. What about a tool that can find interesting patterns?
• 9:25
  What about a tool that can spot patterns in data that humans can't spot?
• 9:29
  Uh, that would be. That would be an interesting tool. Uh, but actually we have that tool, right?
• 9:34
  That's exactly what the neural network does, right? We we learn a high school.
• 9:39
  We like given a 2D plot, given a, you know, given X and y variables, we can plot some dots, and then we learn how to draw the best fit line.
• 9:47
  Right. And I watched the neural network. Neural network.
• 9:50
  It can find best fit shapes. There are lines.
• 9:53
  It can find best fit shapes and extremely high dimensional data.
• 9:56
  That's what the neural network does. Uh, and so that's great.
• 10:00
  So we can give it, you know, mathematical tables that we have already.
• 10:04
  And we can say, you know, can you spot stuff that we can't see. So there's a theorem.
• 10:08
  Uh, I just thought I mentioned this theorem because, uh, you have some that can be these are low dimensional topologies here in Oxford.
• 10:16
  Uh, and they collaborated with computer scientists at Google DeepMind, and they proved a theorem about hyperbolic knots.
• 10:22
  Uh, and the way this theorem was discovered, uh, was that they generated a big table of, uh, you know, invariants of knots.
• 10:31
  Uh, and then they asked the neural network to see if it could find any patterns in this table.
• 10:36
  And, uh, the neural networks spotted that this Siggraph case, this is the signature of the knot.
• 10:42
  The neural network could accurately predict the signature of a not given other invariants.
• 10:47
  And this was surprising because the other invariants have a slope, the volume in the activity radius.
• 10:52
  These are. These are embeddings coming from the three manifolds. You know topology, the three manifolds associated to them.
• 10:57
  These are these if you like. These are continuous invariance. These are real numbers whereas the signature is an integer.
• 11:03
  So this is some some theorem relating the discrete and the continuous.
• 11:08
  So it must you know you know it must be profound.
• 11:11
  Uh, but the fact that these things were the fact that these things were related at all, this is what the neural network told them.
• 11:17
  And once the neural network said there is some pattern, then the mathematicians took over and found the pattern and proved the theorem.
• 11:23
  So the machine didn't prove the theorem, but the machine told them where to look for the theorem.
• 11:28
  So that's kind of a surprising application. Uh, but it's really old.
• 11:33
  It's from 2021, so this ain't nothing else.
• 11:36
  And all the other things I cite in this talk will all be from 2024 or 2025.
• 11:42
  Um, because the air is just moving very, very fast.
• 11:46
  Uh, so really, I want to. Jordan Ellenberg, uh, is thinking a lot about this, uh, this kind of thing.
• 11:55
  How do we use neural networks? These things can find patterns in data.
• 11:59
  How can we use neural networks, uh, to, you know, find new interesting structures, examples, counterexamples, this kind of thing.
• 12:08
  So again, uh, this pattern boost paper. Ellenberg is a mathematician, prestigious mathematician from Wisconsin.
• 12:14
  This is Jodie Williamson, another very, uh, FRS and a very famous mathematician.
• 12:20
  Adam Vargas, a young researcher. And uh, funds were shot on the works of meta.
• 12:25
  So again, very surprising collaboration. So, you know, five years ago, you might not have expected, uh, and they,
• 12:32
  they made a very simple architecture, uh, that can search for examples of counterexamples.
• 12:38
  Uh, so in sort of finite combinatorial objects, uh, and what they're doing, basically,
• 12:43
  they write a naive human algorithm to try and solve a problem, to try and find extreme examples.
• 12:49
  And then they write a and then they, you know, use neural networks to say, you know,
• 12:53
  they generate lots of extreme examples, uh, and then they encode them as strings.
• 12:57
  And then they say to a neural network, here's a list of strings that we really like.
• 13:01
  And now could you give us more examples of strings that we're going to like. And then the neural network say sure, I'll do that.
• 13:07
  You don't explain the question. You you encode your finite graph, which is extremely in some way, you encode your finite graph as a string.
• 13:16
  You give it the neural network. Say, I love these strings. Give me more strings is a show.
• 13:20
  I'll give you strings. And then you try and decode the strings back to graphs.
• 13:23
  And half of them just don't decode that, you know, they garbage. And then the other half do decode into graphs.
• 13:28
  And then you look at these graphs and they're not a great example, but they're not extreme.
• 13:32
  But you get a you can keep adding edge, you can do more.
• 13:35
  You know, the computer and the human are just thinking about the question in really different ways.
• 13:39
  And they find, you know, they they can find counterexamples to, uh, to theorems.
• 13:45
  This way is very weird. Some extremely simple to read paper.
• 13:50
  Uh, I quite like this work of Ellenberg. You should look at recent work of Jordan.
• 13:54
  He's also collaborated with the physicists, uh, from Oxford. Uh, getting getting machines to write Python programs, which are solving maths questions.
• 14:03
  It's a very surprising, very surprising and innovative new use of technology.
• 14:09
  Uh, but the big problem with using neural networks to do this kind of thing is that they have limited application.
• 14:14
  You know, you can't if you're if you're interested in an area of mathematics where there are lots of tables or where,
• 14:21
  you know, the fundamental objects can be described by finite amounts of data.
• 14:26
  And the interesting problems is finding, you know, finding new data, then that's great.
• 14:31
  But if you, you know, if you are doing research in Sobolev spaces or, you know, whatever Banach manifolds, so, you know, infinite,
• 14:38
  intrinsically infinite dimensional objects where there aren't any tables, um, then you just might not be able to use these tools at all.
• 14:47
  So we've got limited applicability. And that's just to say we've seen that happen before, right.
• 14:51
  And then the 1960s and the 1970s computers became available to mathematicians.
• 14:56
  And they were just very, very fast fancy new calculators.
• 14:59
  And all of a sudden we could do you can multiply two, 100 digit numbers together really quickly, right.
• 15:05
  And if you're doing research into, into Banach manifolds is no used to at all.
• 15:10
  But if you're doing research in sort of, you know, computational number theory, then suddenly you've got a great new tool.
• 15:18
  So we've seen, you know, computers come along and they might affect some bits of maths.
• 15:23
  They might make some, some, some areas that suddenly, you know, an exciting new thing.
• 15:29
  You know, I mean, I'm interested in, uh. I'm interested in general purpose tools.
• 15:35
  Yeah. This is this is this is the kind of question. Can we can we really give mathematic.
• 15:40
  You know, give mathematicians a general purpose tool.
• 15:44
  Uh, so now we have to talk about, you know, I'll talk about there in previous in a bit, but we've got to talk about language models, uh,
• 15:51
  because you know, that any, any mathematician who's use them will know that they right now they are not perfect by any means,
• 15:59
  uh, for doing mathematics. So I idea, uh, the mathematicians in there,
• 16:03
  are there any mathematicians in the room can actually use the language model and it's told them something useful.
• 16:08
  Are there any can anyone put their hand up to. Yeah.
• 16:11
  Go. So some you see. There you go. Great. There's like ten hands.
• 16:17
  You see. But you know, the AI people are really, really excited about language models, but that they're in their current form.
• 16:25
  Uh, they're not perfect. Uh, so actually, I, I, I used ChatGPT last week.
• 16:33
  Uh, uh, because I so I as it's been, as it's been, uh, mentioned several times.
• 16:42
  Uh, I'm currently involved in some strange project related to Fermat's Last Theorem.
• 16:46
  Uh, and I dare I, I if I click this, then all manner of things that happen.
• 16:52
  Right? I'm gonna try clicking this.
• 16:56
  Uh. Let me.
• 17:15
  Was. So anyway, as I was saying.
• 17:22
  There's some website on the internet that contains a whole bunch of maths, uh, involving some kind of, uh, that.
• 17:32
  It's a very beautiful website. Looks really nice, but rendered in rendered in beautiful latex on the web.
• 17:39
  Uh, but I'm just in the middle of writing, uh, a very long, you know, explanation of a lot of mathematics behind Fermat's Last Theorem.
• 17:48
  And I needed the fact that if a was a dedicated domain with field of fractions K, and if L was a finite separable extension of k,
• 17:56
  and B was the integral closure of A in L, uh, then I claim that for an arbitrary k module uh,
• 18:04
  string over k with L is the same as ten string over I would be. So there's some random statement in graduate level algebra.
• 18:12
  Uh, and that's the kind of thing that I thought that I should be able to prove.
• 18:15
  Uh, but the problem is, I just got a bit stuck because it ring advantages of a number filled ring of integers with finite extension.
• 18:24
  The new thing might not be free over. The whole thing is going to be projective, but it might not be free.
• 18:29
  Locally free, but maybe not free. So there was an at that.
• 18:31
  [INAUDIBLE], there was some technical issue, so I thought I should be able to do this right.
• 18:37
  And I spent like two minutes on it and I was just like, this is stupid.
• 18:40
  It's like, this is graduate level algebra, right? This, this, you know, okay, so I, uh, I.
• 18:47
  So well about 20 years ago. Uh, I would have just, like, knocked on another number.
• 18:52
  Theory stories that had you do this. Uh, ten years ago.
• 18:56
  There's a new option I could ask for. Math overflow. Right?
• 19:00
  Or math dot stack exchange.
• 19:01
  Two years ago, I could just kind of cheat and ask on the lean chat, uh, because there's a bunch of mathematicians hanging out there.
• 19:08
  Uh, uh, and it's likely that somebody will give me an answer quickly.
• 19:11
  But now, of course, you can actually ask ChatGPT for I don't pay for these things, right?
• 19:18
  Because I'm super sceptical that they're useful. But you just go to chatgpt.com and I type in my graduate level question.
• 19:25
  It gives you a list of algebra and the, uh, the answer is illuminating, right.
• 19:30
  Because I asked this explicit question about ten tearing up finite extensions of, uh, the rings of integers, of number fields.
• 19:38
  And the first thing it does is it says, oh, suffices to prove this simpler problem.
• 19:42
  And that was something I'd spotted when I was thinking about it for two minutes, and I thought, this looks like progress.
• 19:47
  And then I decided, actually, is it progress? It seemed the reduction seems just as difficult as the original question.
• 19:54
  So I tried that, and then I gave up on that. And then I asked ChatGPT, and the first thing ChatGPT does is finds the same reduction.
• 20:01
  Uh, and then actually, you know, it gives the idea which I'd missed.
• 20:05
  It gave the idea about, uh, how to, you know, how to prove the reduction.
• 20:11
  Uh, and then it justified its argument with rubbish.
• 20:14
  This is this, you know, is very, very wishy washy on exactly how this proof worked.
• 20:22
  But the thing is, it gave me enough clues, uh, that I could actually put everything together.
• 20:29
  And so. So there we go. So the language model was good in the sense that it pushed me in the right direction,
• 20:36
  but it wasn't perfect because when it actually when it came to the details, it was, it was, it was, um.
• 20:42
  Not at all. Yeah. As I say, this is not an inaccurate summary, right.
• 20:46
  The details were vague or meaningless. Uh.
• 20:51
  And why is that happening? It's because, of course, they know all the facts on the internet, right?
• 20:55
  That's, you know, that's how they're trained on the internet. But the thing is, they're not very good at logical reasoning, right?
• 21:01
  They're not very good at actually. They don't have understanding in the same way that we have understanding.
• 21:07
  Right. Can these things think it's just not even a meaningful question.
• 21:12
  It's like asking if a submarine can swim. You said humans think these things are not thinking they're doing something else right?
• 21:20
  As Ken, I know this is a quote from Ken Ono, right?
• 21:23
  That is not cognition. They're doing recognition, right.
• 21:26
  I they've seen lots and lots of things before. And so they kind of think, oh yeah, I've seen this thing before.
• 21:32
  That's to that's what humans do in this situation.
• 21:35
  I'll do that.
• 21:36
  Uh, and actually it's interesting, like what a mathematician actually doing this is a lot of what mathematicians are we just doing pattern matching.
• 21:44
  Occasionally we have ideas, but how often are we having ideas and how often are we just, you know, just going through the motions and.
• 21:53
  Yeah. Oh, I know, you know, just applying stuff that. Yeah, we just.
• 21:59
  It's not immediately clear how many times we're having brilliant new ideas,
• 22:03
  and how many times we're just applying facts and techniques that we just know work because we've seen them in other situations.
• 22:11
  So we're we're maybe doing similar things to the machines.
• 22:14
  But the thing is, we can back it up with this logical reason.
• 22:17
  We take an idea from a related area, but then we could rigorously prove that that idea works in our situation, right?
• 22:24
  The machine takes an idea from another area, attempts to apply it, and then and then,
• 22:27
  you know, it's really fluff when you ask them, does it actually work?
• 22:32
  Hey, this is the thing they never give. They never say, I don't know.
• 22:35
  The common failure mode if you ask a human a question.
• 22:39
  Yeah. A common failure mode is I don't know. Whereas you ask a machine a question, the common failure mode is [INAUDIBLE].
• 22:46
  This is the if they they would rather make something up and say they don't know.
• 22:53
  So this is the big question, right? If we want to use these things, how do we teach language models to reason accurately?
• 22:58
  And uh, and the way, the way that we're going to do that compared to scientists, they like, you know, they like challenges.
• 23:05
  They want they want a challenge, and then they want to be state of the art in that challenge.
• 23:09
  Right. And if you can get state of the art, you can get a paper.
• 23:13
  That's how computer science seems to work. You you you you make some challenge and then you say and compute.
• 23:21
  Yeah, I can try this challenge. And at the end they get a grade.
• 23:25
  Yeah, they get a grade. They, they try this challenge and they get 15%.
• 23:29
  And if that's better than any other AI then the then they've got state of the art.
• 23:34
  And if you get state of the art then what you win is a paper. That seems to be how computer science works as far as I'm concerned.
• 23:42
  Anyway. So how do we make challenges? The way you make a math challenge is a data set, right?
• 23:47
  So a quest, you know, a big collection of mathematical questions.
• 23:51
  That's what a challenge looks like. Uh, and the idea is you get the machine to answer the questions correctly, you get a point for each word you get.
• 23:59
  Right. And, uh, and so now the question is what a mathematical data sets look like is that when you're a mathematician,
• 24:06
  you, you know, these things are being generated by computer scientists.
• 24:09
  And as mathematicians, we tend not to look at them at all. So what a mathematical data sets look like.
• 24:14
  Uh, they come in several forms. Uh, they're mathematical questions.
• 24:18
  But what level? Right. They can be. They can be sort of GCSE level.
• 24:22
  Right. The way up to research level. That's what it.
• 24:26
  Yeah, that's the range of, uh, it's, uh, the range of the mathematics is really, really extreme.
• 24:33
  Uh, they might be a natural language, or they might be in a formal language, like languages.
• 24:39
  There are other formal languages as well. Uh, so.
• 24:43
  But of course, Leon seems to be winning.
• 24:46
  There's. And in many cases, uh, the formal language chosen is Latin for mathematics at least, uh, the problems might have shorter.
• 24:55
  This is a big difference. The answers to the questions my either be expressible in about eight characters.
• 25:04
  Yeah, they might be a multiple choice question. Uh, or they might be.
• 25:07
  What is this number? Uh, or they might have really long answers, you know, prove this theorem.
• 25:13
  And the answer is like two pages long. So you get different data sets.
• 25:17
  Uh, you know, ranging. Yeah. The kind of answers you get can be very different.
• 25:23
  And finally, they can be either public or private. Uh, that the private ones, the way it works is you have 100 secret questions,
• 25:30
  and they say we've got 100 secret questions, and here's here's five of them.
• 25:34
  Yeah, we'll make five of them public. And the other 95 is secret.
• 25:37
  Uh, so you get some kind of feeling as to what the data set looks like.
• 25:41
  Uh, but you can't see. Yeah, you can't see the question if you want to have a go.
• 25:46
  Uh, you have to send your I. Yeah. To the company or the organisation that's holding the secret questions.
• 25:52
  And they run, you know, they run it, and then they give you the reports about how many you got, right?
• 25:57
  So let me just give you a couple of examples of data sets. This is the artificial intelligence math Olympiad.
• 26:03
  Uh, this is again this is Jurco. Uh, he was mentioned in the last, uh, you know, he's a guy who's funding more and more mathematics.
• 26:11
  Uh, the, uh, you know, X markets.
• 26:14
  So there's a, uh, he's really pushing the idea of open source AI.
• 26:19
  He's very worried. The, you know, the the sort of closed source.
• 26:24
  Yeah. I was talking about wouldn't it be great if we had a general tool that help mathematicians?
• 26:28
  But one thing that perhaps would be a bit less great if that tool was owned by a private company.
• 26:33
  And I was like, just for $1,000 a month, you can have that.
• 26:36
  Your university can have that tool. Uh, yeah.
• 26:39
  He would like he wants to see open source tools. Uh, so that I should say I mentioned this first item on the advisory board.
• 26:48
  Uh, for this for this project. So right now we've had two progress prizes.
• 26:53
  So we've had two competitions. Uh, and both of the competitions have involved private data sets.
• 26:59
  So secret questions. Uh, and the questions are written in English.
• 27:04
  Um, and there are an error that so challenging high school type questions.
• 27:09
  Uh, not as hard as International Math Olympiad, but yeah. So there are other Olympiads.
• 27:14
  An easier level, right? Uh, and the key thing is the answers are short.
• 27:19
  Answers are always whole numbers between 0 and 9, nine, nine.
• 27:23
  And this is this is the kind of question that you see.
• 27:26
  So it's not the kind of thing you can do immediately.
• 27:29
  Uh, so each of the three digit numbers from 111 to 999, you colour it blue or yellow and there's some rule.
• 27:36
  And then the question is what's the maximum number of yellow. So it's so sufficiently big you can't solve it by brute force.
• 27:42
  You can't do all two to the 889 possibilities.
• 27:46
  You have to you know, those a sort of a combination. There's some calculation involved and some reasoning involved as well.
• 27:53
  Uh, and we're at the stage now where you can type that kind of question into a language model, and the language model can get it right.
• 28:02
  Uh. So, as I say, the questions are kept.
• 28:05
  Secrets. And if you want to play, then you have to give us your model.
• 28:09
  So you can't, uh. Yeah.
• 28:12
  We won't send the questions to, uh, to the to the private, to the private models.
• 28:18
  You have to upload your models of hugging. Yeah, it's a Kaggle and then Kaggle.
• 28:21
  Run it and tell you what you got out of 50. Uh, and there's prize money, right?
• 28:26
  The models compete to win six figure prizes. Uh, and there's been two competitions so far.
• 28:31
  And the second one just finished, uh, and top, top of the leaderboard, uh, was a, you know, a gang of 3 or 4 people.
• 28:38
  And they scored 34 out of 50.
• 28:40
  So, so for high school Olympia, there's state of the art for these kind of high school Olympiad questions as far as open source models are concerned.
• 28:50
  Uh, if you asked OpenAI AI to do this, they would probably get a much higher score because the closed source models are always ahead.
• 28:58
  Uh, so what advantage of, uh, of me being on this, uh, maybe on the organisation committee for this thing is that you get to see secret data.
• 29:08
  That's, uh. Uh, so this is a table.
• 29:11
  These are the 50 questions. Uh, is this is this competition's just finished.
• 29:15
  Uh, and then these orange bars indicate sort of the ten most popular answers that.
• 29:20
  So these are the top 500, uh, eyes that took part in this game.
• 29:26
  And, uh, the light orange is the most popular answer. And then the dark purple is the least popular answer.
• 29:31
  And, uh, so you grade it from, uh, light to dark orange, uh, and then the grey is all the other answers.
• 29:37
  And then you take the most popular colour in green so that, you know, of these 50 questions, the top questions there, the easiest question.
• 29:43
  You can see like 90% of the models, uh, were guessing the right answer first time.
• 29:49
  Uh, so and uh, then by the time it halfway down, you can see it's still the case that the most popular answer was equal to the, uh.
• 29:59
  I was equal, uh, to the correct answer. For the first 50% so that you see things are going wrong.
• 30:05
  Right? These things where there's very small green dots.
• 30:08
  So the, you know, like the green, the green stripes there indicate like the eighth most popular answer turned out to be the correct answer.
• 30:16
  So that, you know, there's some data. Uh, but basically 500 language models are getting, you know, getting half of these questions correct.
• 30:25
  So there's some kind of idea as to where open source AI is now.
• 30:31
  Uh, but we don't care about these stupid undergraduate questions, right?
• 30:35
  We care about hard questions. So what about this frontier math data set?
• 30:38
  Here's a here's a proper question. Uh, here's a question about moduli spaces of conics.
• 30:45
  So, you know, here's some intuitive geometry question. Well, it looks like an intuitive geometry question.
• 30:50
  It's actually a combinatorics question which is heavily in disguise.
• 30:54
  Uh, but you've got moduli space of conics tangent to a given set of five conics in the plane.
• 31:00
  Uh, and the question is and now you look at this, you look at these moduli space mod p and you ask how many how many connected components this got.
• 31:08
  Uh and as p varies this answer changes. This is not over FP bar over FP.
• 31:14
  So this is an arithmetic question not a geometric question.
• 31:17
  Uh, and then the answer is give the answer to two decimal places. So again the answer's very short.
• 31:22
  Uh, but now this is research level mathematics.
• 31:26
  Uh, and one of OpenAI's closed source models got 25%, uh, on this dataset.
• 31:32
  So we've got questions of that nature. You know, that looks.
• 31:35
  That's technical and complicated. But the AI is getting 25% of that, including a correct solution to the question.
• 31:44
  The. So that's where closed source is right now.
• 31:47
  And. And um, but when you actually ask, this is the problem.
• 31:51
  You know, it's great the you know, the model can solve that.
• 31:55
  The model get that number right. But then when you ask it to explain why that number's correct, it's wishy washy.
• 32:02
  Is it because it makes them get it has to like if you've got some Galois group and has to guess what the Galois group it is,
• 32:08
  it just guesses the gavel group is the full symmetric group. And it's right.
• 32:11
  And then you ask it why is it the full symmetric group. And it's vague.
• 32:15
  It doesn't actually know why. But it's just you know it's just this is the problem with these number questions is they don't correctly test reasoning.
• 32:24
  They test how good you are at guessing the answer. And these models have got very good at guessing the answer.
• 32:30
  Uh, so the close source, the close source models are around two years ahead,
• 32:35
  and the close source models are trying to pull ahead because the tech companies have stopped publishing.
• 32:40
  This is this is what's happened because they want to stay ahead and the open source models are trying to catch up.
• 32:47
  Say, why are these datasets private? That's kind of obvious, because if they weren't private, if you just put them all on the internet,
• 32:52
  that people would start asking them on Math Overflow and people would start answering them,
• 32:56
  and then the answers would be on the internet, and then the models would learn the answers,
• 32:59
  and then the models would just all get 100%, so it would break the system.
• 33:04
  And now what are the RSS numbers? That's a much more pertinent question.
• 33:08
  What are their numbers? Just because we want to be able to market really easily.
• 33:13
  Right. If you ask a question and if you ask the how do you prove this theorem?
• 33:19
  If the answer is a two page long proof. Who's going to mark that right.
• 33:23
  You can't have I marking its own homework.
• 33:27
  This is the problem right? If if you if you get if the question is prove this theorem and the questions in English and the answer is in English,
• 33:36
  you see where this is going, right. If the questions in English and the answers in English and the answer is two pages of LaTeX,
• 33:43
  and we have to decide how many points out of ten this answer, a human has to read it right.
• 33:48
  And that's really expensive. Right.
• 33:53
  So the computer scientists want to get state of the art.
• 33:57
  But the problem is marking a proof. Right.
• 34:00
  That's what we do. We don't. We don't ask, what is this number?
• 34:04
  We ask how to prove this theorem. But it it's too expensive to mark that in natural language.
• 34:11
  So the natural language data sets are all what is this number. Questions.
• 34:15
  Right. That's not what we do. Okay.
• 34:19
  So formal data sets right. And these are data sets now.
• 34:23
  Now it's different. Now the questions are not written in English. They're written in lead.
• 34:27
  Uh, all these other languages. But yeah, the vast majority of them are written in lean.
• 34:32
  And now, of course, you can ask the interesting question is I prove this theorem right?
• 34:38
  And now the idea is this time. Now the model writes a model writes a solution.
• 34:42
  And now we just throw it into lean and see if it compiles.
• 34:47
  Yeah, because now a machine can grade the answer, right?
• 34:51
  If it's wishy washy, it's just not going to compile, right.
• 34:54
  That's what we do. And now, of course, the big problem, uh, unfortunately, uh, is that right now the level is terrible.
• 35:04
  The level is terrible. The data sets are mathematically trivial, right?
• 35:09
  So we have these formal data sets where the questions are in line, but they're GCSE.
• 35:14
  They're really very, very easy stuff. So the hardest one I'm aware of currently for these formal data sets is Putnam Bench,
• 35:22
  uh, which is formalised statements of 640 uh Putnam's uh Putnam questions.
• 35:28
  So the Putnam is an undergraduate level, uh, undergraduate level problems.
• 35:34
  Uh, so hard undergraduate level problems and state of the art is abysmal, right?
• 35:39
  State of the art is ten out of 640.
• 35:43
  Uh, so that's good when you see state of the art like that, because it means there's plenty of room for improvement.
• 35:48
  Well, by the time that the by the time the state of the art is 60%, then you really you've lost interest like people like, oh, great, I've got 65%.
• 35:56
  But like if you're solving half the problems, then you know won't be.
• 36:00
  Give us a year and you'll have solved all the problems.
• 36:02
  But right now this is undergraduate level material formalise and lead and people can't do it right.
• 36:10
  Apparently OpenAI's most recent. Oh, no.
• 36:13
  No, this is this Chinese model, deep sea prover A claiming they've got they've got more than ten, but it's yet to be.
• 36:20
  And you know, the the Putnam people have to officially check this, but apparently, uh, there's been a big jump this week, so we'll wait and see.
• 36:28
  But what do we really want? Like, what am I trying to sell here?
• 36:32
  I want to. I want these systems to do the kind of mathematics that I want them to do.
• 36:37
  The periodic Langlands program. Right. That's what we want.
• 36:42
  And, uh, because, you know, that's what's happening in places like this.
• 36:47
  And so data sets are private. That's a bit rubbish. Like data sets are too easy.
• 36:52
  That's a bit rubbish. Uh, so there's a very good paper by, uh, by Simon Fraser again, uh, talking about, you know,
• 37:00
  the general problem of mathematical data sets and just flagging all the things which are somehow insufficient currently.
• 37:09
  Uh, but I do believe that when we get it right and we start making data sets that are
• 37:14
  actually correctly modelling the kind of mathematics that researchers are doing,
• 37:19
  you will get computer scientists, you know, trying to get state of the art on these data sets.
• 37:25
  Right. So where are we? Like, language models are rubbish.
• 37:28
  Language models make stuff up. Uh, current data sets aren't asking the right questions.
• 37:33
  Uh. And so now let me finish this talk with a vision.
• 37:39
  Uh, this isn't science fiction. Uh, and is maybe a route to some kind of tool that mathematicians can use.
• 37:49
  Uh, so let me go all the way back to 2023, uh, where language models that first appeared and they couldn't compute.
• 37:56
  Right. And it was really funny you asked them, you asked ChatGPT to multiply 210 digit numbers together.
• 38:03
  You give it two explicit two digit numbers together, and it confidently gives you a 20 digit answer.
• 38:07
  And it begins in the right number, and it ends in the right number.
• 38:11
  And in the middle, all the numbers are just made up. That was like that was what it looked like in 2023, right?
• 38:17
  But in 2024, when you ask it to multiply 210 digit numbers together, it just follows a python.
• 38:24
  You know, it fires up Python to ask Python what the answer is, and then it reports the answer because these systems learned how to write Python code.
• 38:34
  And how did they learn how to write Python code? Well, they just train them on Python.
• 38:38
  There's billions of lines of Python code on the internet.
• 38:42
  So the language models just train on that Python code. And then I got really good at writing Python.
• 38:46
  And now when you ask some computation questions the python's good at it.
• 38:51
  Just, you know, it just gets Python to do it. But right now, as I've said several times, they can't reason at a high level.
• 38:59
  Right. And the the harder the mathematics gets, the worst, I guess, at reasoning.
• 39:05
  Okay, so maybe we should just teach them to write lean code.
• 39:09
  That would be good because then, you know, that stops them [INAUDIBLE], right?
• 39:15
  It's you know, you ask them to write, you say prove this theorem.
• 39:19
  And then internally it proves it in lean and that it translates it back into human.
• 39:24
  You know, it's going to get it right. But the problem is we can't train it only in code because there's only millions of lines of leading code.
• 39:34
  And that's and a lot of that is undergraduate level, right?
• 39:37
  This is the problem we want to break through on. We want to get them to do research.
• 39:42
  We want to break through undergraduate level. And most of it is undergraduate level.
• 39:47
  So undergraduate level. That's great. Are you? DeepMind has shown us that you can train on what's already there and you can get heart.
• 39:55
  You know, you can solve half 50% of the 2024 IMO, given given only what we have.
• 40:04
  But as I say, that's lemmas, right? That's not theorems. So how are we going to get this further?
• 40:10
  And we just lied. This is a big problem.
• 40:14
  We need to think seriously about getting a lot more modern mathematics.
• 40:19
  Formalised. It seems to me this is this is the bottom.
• 40:22
  This is the problem. We need to get a lot more modern mathematics formalised.
• 40:27
  And because that does not this is not science fiction, right?
• 40:33
  Maybe, maybe we can get machines to do that.
• 40:36
  Maybe because it's one thing coming up with your own ideas,
• 40:41
  but actually translating from a human proof into a computer proof that really does not sound.
• 40:48
  Yeah, that's much easier than coming up with your own proof.
• 40:51
  Just doing that. Like we can translate between English and Chinese.
• 40:55
  So I Gobbi translate between English and lean. Right.
• 40:59
  That that doesn't sound crazy to me. And of course, you know, people are thinking about this.
• 41:05
  And so finally, whether this is one of the reasons why I'm currently teaching Lena proof of Fermat's Last Theorem.
• 41:12
  So this was proved in the 1990s by Andrew Wiles and, uh, ably assisted by my advisor, Richard Taylor.
• 41:20
  Uh, the proof is huge. Uh, I mean, the Wiles paper is album pages, but it's got 80 references.
• 41:27
  Uh, like I said, the proof is over 200 pages either if you want to write down the proof.
• 41:32
  Yeah. From the axioms of mathematics, it would be more like 2000 pages.
• 41:36
  I think it would be a more reasonable estimate of how long this proof is.
• 41:39
  Uh, and and the weird thing about the proof is that the Fermat's Last Theorem was a question about positive whole numbers.
• 41:47
  But the proof goes through all manner of really complex structures.
• 41:52
  Right. All these modern buzzwords. Uh, elliptic curves and modular forms and Galois representations of finite flat group schemes.
• 42:00
  And we've got them. All right. There's you know, there's an example.
• 42:04
  Yeah. Those are examples of things that over the last couple of years, we've now carefully formalised these things in lean.
• 42:11
  So that in I mean, you know, it's in my Fermat's Last Theorem repository and uh,
• 42:15
  it's slowly moves in, in my repository as a feed, a repository for math lib.
• 42:21
  Uh, so elliptic curves are modular forms are math lib, uh, and the other two things, Galois representations and group schemes.
• 42:27
  They're not in Matlab yet, but in a year's time they will be. That's, uh, that's how the project is going.
• 42:33
  You know, I'm I'm building stuff. But, you know, when we make a new definition, we make sure it works.
• 42:39
  You know, we make sure it's usable. And then when we're convinced we've got it right, uh, we push it.
• 42:45
  But but it's. No, it can't just be me. Right?
• 42:49
  It can't just be me doing that. There's more to mass than Fermat's Last theorem.
• 42:54
  It turns out. Uh, there's other there's other areas of mathematics.
• 42:58
  And here are just some dumb examples of stuff that are like undergraduate or beginning graduate level mathematics that are not formalised.
• 43:07
  Yeah, that are not formalised. And as far as I know, any theorem prover.
• 43:11
  And I just need someone to sit down. You know, it's not difficult to sit down and teach the machine.
• 43:17
  It's not just the definition. The definition and basic facts about the definition.
• 43:22
  Right. But the thing is, we can't get machines. We can get machines to prove theorems.
• 43:26
  But it's really difficult to get machines to write down definitions because formalising definitions is an art.
• 43:33
  Right. Is it system specific? Right.
• 43:36
  Well, the best way to to teach lean, uh, what are not is, isn't necessarily the best way to teach Isabel or to teach math and math.
• 43:44
  Right. It's system specific. Uh, and also, you've got the problem.
• 43:49
  The machine isn't holding your hand at this point, right?
• 43:53
  The machine will check that your definition is syntactically correct, but the machine won't check.
• 43:59
  It's semantically correct. The machine won't check that you've written down the right definition.
• 44:03
  The machine will just check. You've written down a definition that makes sense.
• 44:08
  So you've got to be super, super careful here. So this is something.
• 44:15
  This is something that human experts need to do.
• 44:18
  Right to theorems. We can let the software do it itself.
• 44:22
  Right. In two years time, maybe the systems will be translating from human maths.
• 44:28
  Translate a human proof into a living proof. That is absolutely not out of the question.
• 44:34
  But for me, formalising definitions you absolutely need to take anything in machine says with a very big pinch of salt, right?
• 44:43
  So who is going to do? Who is going to formalise all these definitions in all the graduate courses that are being run in Oxford?
• 44:51
  Right. It's not going to be computer scientists. Okay.
• 44:56
  Whose job is it? I mean, I claim. I claim that it's the mathematics research community's job, right?
• 45:03
  We've got we've got to do. We are the people who are qualified. But the problem is, we're not going to be rewarded for that, right?
• 45:10
  The reward system in maths is that you get points, you get money.
• 45:15
  If you get points in the research assessment exercise and you get points in the research assessment exercise by papers.
• 45:23
  Do you get papers by proving therapies? New theorems builds upon old theorems which builds upon old theorems, not all of which are correct.
• 45:31
  As I found out when I was trying to teach the computer proof of Fermat's Last Theorem.
• 45:35
  We're not as smart as we think we are. So we've got this idea that everything in the lecture is fine and we just need to build more.
• 45:42
  Right. But it's is is this really is this really how we're going to change mathematics?
• 45:48
  Right. I think that this whole, this AI and theorem prove is that together they are giving a completely new way of thinking about mathematics.
• 45:59
  But but the system isn't, you know, the system.
• 46:02
  There's something wrong. Right? That that's the problem.
• 46:07
  You know, and actually actually. Yeah.
• 46:10
  What can full moon message do for mathematics? Okay.
• 46:14
  Can they really turn it on its head? I mean, that's it.
• 46:19
  Thank you.