Transcript: Chief Scientist: Timothy Gowers, GOSIM 2026 Paris

Hello everybody. I'm Alexa Proball, the head of commutate Lake sale and here we are at the Go Sim Paris and with us we have Sir Timothy Gowers who is a professor at College de France and University of Cambridge and he can order this conference and he's a field medal winner in mathematics and in combinatorics and it's really exciting. I went to math school in Moscow. One of my classmates Igor Park is a well-known combinatorics scientist. So I you know, I'm not you know, I love mathematics but never you know, work at this amazing levels. It's really exciting and all all the eyes math, right? It's all matrices all the way down. So it's really exciting to have Timothy with us and can you tell us a little bit about how you came here and what you talked about in your keynote? Yes, I mean I came here because uh I've got an invitation and uh I'm although I'm a mathematician, I'm also very interested in automatic theorem proving and I have a group in Cambridge >> Mhm. devoted to automatic theorem proving. That's to say um just trying to get computers to do mathematics. But uh our focus is a little bit different from um a lot of what's going on in that uh domain. So a lot of what's happening is what you might just call prompt engineering. You're just you're giving problems to uh language models to solve and if you get the prompts right, they're getting better and better at solving them. But we are interested in really understanding in a more fundamental way how human beings solve problems. It's a very mysterious uh question because um we know that uh it shouldn't in some sense it shouldn't be possible. If you have a general mathematical statement Mhm. and uh you ask does this statement have a proof? That's actually uh halting complete. There's no algorithm that can tell whether a in a sense there's no algorithm that can do mathematics in general. Mhm. But, uh we can do mathematics, and that's because we don't do general mathematics, we do sort of interesting mathematics. >> Right. So, we're trying to understand what it is that about the interesting mathematics that makes it possible for human mathematicians with their rather limited resources to be able to come up with complicated proofs. Right. And we hope that by understanding that, we'll be able to teach AI to do it better. Right. And so, as a result of that, I have an interest in what's going on in AI, and so coming to somewhere like Ghost Server is a good way to meet people and find out what other people are thinking about in the more AI domain, so. Thank you. I I mean, it really struck me. One thing in your keynote, right? So, I went to this best math school in Soviet Union because and I should have studied history. I like history. I really like humanities. I'm not very good at math. I'm okay at math, but now I'm a better programmer. So, but there was no other path for people to do something real because, you know, all the humanities were Marxist-Leninist. So, and I thought that math is very antisocial. When I read math books, they rubbed me the wrong way because, effectively, they they provide very like very dense statements, and then there is an answer, and in between there is a phrase like as an exercise to the reader. Yeah, yeah, yeah. Or it easily follows that and there is nothing like like it's followed easily, right? And so, I thought that I'm dumb. I don't understand it. But then you said that this is basically a wrong way for people to understand math, and you said that LLMs they should do math basically became antisocial and mean this way because mathematicians write books this way from which we shall learn to read. And so, suddenly it just occurred to me that math could could have been different. It could have been more convenient. And the And you also said that you're interested not in the achieving the result, but you want to see how a mathematician arrived at that result. This was very interesting to me. Can you explain a little bit like how do you go about it? Yes, I mean just before I get on to that, I mean I think something very important happened in the beginning of the 20th century, which was putting mathematics on a rigorous footing, developing the axioms uh ZF axioms and uh formalizing what we meant by rigorously what we meant by a mathematical proof and so on. But unfortunately, I think that development, though extremely important for mathematics and very positive development in many ways, had a slightly unfortunate stylistic consequence that people then tried to write in this kind of formal logical style. >> Dry. Yeah, which um sort of lost Something was lost in that process or something to do with the human presence. They look like computers. They They want to be machines. >> Yeah, exactly. Um So, how does one counteract that? I mean, actually I've been trying to counteract that throughout my career, uh long before anything to do with AI or automatic theorem proving, just by really examining carefully how I myself come up with proofs or thinking about things that I was taught when I was a student. Mhm. Um that I just accepted the proofs of them. So, I would think, "Actually, how could somebody have thought of that argument?" And sometimes if I thought hard enough about it, I realized actually often after teaching it myself, Mhm. I would suddenly see something that would make me realize, "Ah, yes, that's how to have probably how that was or how could that have that how how that could have been discovered." Um and so for me there's always been quite a strong link between a really good way of explaining mathematics to humans Mhm. and a really good way of explaining mathematics to computers. Mhm. Um and um what I hope is that uh Well, I don't think we have this at the moment, but I'm hoping that sometime in the future we will be able to teach computers to think about mathematics in a more human way Mhm. so that they will then be able to explain to us in a better way uh what they've been doing. So, at the moment, you know, they they've copied the style that they see in textbooks. They just give us give us the answers, basically. >> Right. And uh sometimes that's not what you want. Sometimes you want This is fascinating, right? Because I I vividly remember So, when I uh you know, went to school 57, which is the most famous math school in Soviet Union. So, a lot of our graduates basically, like Igor, like the professors of math in in famous places. And the other half became oligarchs and they're all retired. Uh because they're very good at computers. Uh but you know, So, we have this series of exams. So, basically, the the class of the math class was filled progressively. First, the half of the people who attended the evening courses, and then a quarter, and then and so, you have to pass exams. So, and um right? And so, uh and I remember that uh So, I read some book on the number theory. So, Soviet Union had these amazing math books, right? And so, basically, I was supposed to explain something, and I thought that I know I kind of mechanically memorized a lot of mathematical formulas. And so, the guy uh was looking at me. Uh I was explaining some some inference, but I mechanically memorized it. I didn't understand the underlying math. I just kind of memorized how the the proof goes. And then, I forgot midway. Uh and and basically, I did all the steps except the final step. And then, the guy looked at me smiling as like expecting me to just normally explain what follows. So, because I followed mechanically, I looked at him with horror, and like I realized that I forgot the next step. And then because I never understood the whole thing, uh I couldn't do it. And so they it just struck me that, you know, some people really understand it, and some people mechanically follow this, and I couldn't do it. And so and then basically it made me think like I'm not really I don't really get mathematics, but that's probably because the the way it was explained was very mechanical and not explaining it to me myself. Yeah, it's an interesting measure of the level of understanding of say a a proof in mathematics. >> Mhm. How much you can actually compress it. >> Yes. So uh the lowest level of understanding, you just have to learn each line and how what comes in But if if you have a better level of understanding, you might have sort of five ideas that if you first you do this and getting to that idea is a fairly standard calculation, and then you get to this by a fairly standard calculation. But then you have to remember those five ideas. Yes. And maybe you understand it better than you actually see there's only one idea, and those five ideas were natural. Yes. And then maybe at some point you reach the point where just the whole thing just you're doing what feels like the obvious thing, and that's when you've reached the sort of ultimate understanding of the proof. >> Right. But but to me it was, you know, a lot of it is like when you do integration, a lot of it is mechanical moving of parts of of formulas around. And so you can remember the mechanics of doing it, but not the underlying principle. And so I think a lot of people will do mathematical transformations as just some kind of mechanical movements, right? And they will not And I think a lot of school children do this. Yeah, I've seen that with my own children, actually. Uh-huh. Everything seems to be fine, and then they suddenly make some bizarre mistake, and then I realize that There's no understanding. Yeah, that the reason it seemed fine was just because they'd learned the manipulations very well, and uh but uh if they got sort of out of distribution, so to speak, >> Right. Right. >> then suddenly uh it fell apart. I want to kind of uh zoom in on the formal methods. So I had a friend who was in formal methods in 1993 working with a computer company, right? And so it seems like a very very kind of stagnant little like academic niche, right? And so, there were people they had the formal method conferences, and they went there, but they were not connected to the real world, right? No, so the first time I've seen a talk about formal methods actually being practical was Leslie Lamport, who gave a talk at the computer conference, and TLA+ and he mentioned how the Amazon Dyna DynamoDB team used TLA+ to basically formulate that it's a correct implementation, right? And and but now then I've seen this whole rise of Lean in conjunction with and people basically want to model the world now with Lean and prove, you know, things about it and apparently it does work in math. So, I'm just curious like do you see this is this a breakthrough for formal methods? Um I think it's certainly a breakthrough of one kind. I mean, it's uh we're seeing the the the the story always used to be that one by and large mathematicians were they didn't really need this extra guarantee of correctness because if something was important um it would be read by a lot of people. If it was if it was incorrect, you know, usually there would be small mistakes, but if there were serious mistakes, somebody would at some point realize that. Mhm. And if it wasn't important, then who cares? Um but two things have changed. And also the other the other side of the story was that uh the effort needed to write down a completely formal proof in a proof assistant such as Isabelle or Coq or Mizar or or Lean which came in a bit later was so great and so much greater than just writing out the usual style of proof Mhm. that it just wasn't worth it. So, two things have changed, I think. One is that conventional proofs have become more and more complicated Mhm. to the point where there is genuine worry about their correctness and uh Right. if the too many proofs come out >> Fermat's theorem it took a long time to show that it's correct. So sorry. And um on the other side as Lean has developed um and people have built more and more tools and added more and more to math Lean that you can then use um barrier to entry to formalizing has perhaps gone down and down and we find that uh undergraduates can formalize deep bits of mathematics Mhm. which they don't even necessarily have to understand very well as long as they can just cover it line by line. >> Right. Um so things have changed a lot and um there's now a big sort of thriving Lean community. So I think I could call that a maybe not a breakthrough exactly because it wasn't really a conceptual change. It's just more like a sort of phase transition that's taken place. And um a further phase transition seems to be about to take place which will be that auto formalization will get sufficiently good that people will be able to formalize without even bothering to learn Lean. They would just write formalizations and >> Right. Write formalizations. So that means that I mean one immediate change will be I think that uh instead of journals sending articles out to referees to check the proofs we'll just get computers to check proofs and so then the only remaining job of journals will be judging whether something's interesting or not. Do you think it will ever happen that you don't need a human in the loop? That this vibe proofing will actually be good enough? I do think it will happen. I don't know how long it'll take but I think that that is the end >> automatic proof Yeah yeah. that you will be comfortable with. >> Oh that's slightly different question whether I'm comfortable with [laughter] Will you ever accept something that computer said is correct and then Yeah, because you you like you're an editor of the journal, you send a submission to a lean verifier and it came back saying this is correct. Will you be now comfortable publishing this? Uh if I judge it to be interesting enough then I'd be I mean I'd be at least as comfortable in fact probably a lot more comfortable judging it to be correct if it had been verified in lean. Yes. Than if I just sent it out to a referee who probably didn't read it very carefully. >> Right, that's right. I mean what we have the system and one has to remember that the system we have now is very far from perfect. Right, right, right. Unless you know and trust the referee to do a good job. >> a lot on those sort of webs of trust and acquaintance with people and so on. So So I'm not thinking what you described is very interesting because and you basically mentioned in the keynote that the models in the recent months got so good that the best models operated at the level of graduate students, right? At the graduate student PhD candidate. >> I may have to qualify that but at least uh some of the time. Some of the some of the time. >> And I think there may be parts of mathematics where they haven't reached that level but Right. Um and there will be plenty of problems where yeah, but they can operate at that level if you give them the right questions to do right at least. And and and basically you said that um a lot of so you're concerned that a lot of low-level work uh will you know, students will now delegate to LLMs instead of doing this manually, right? Like a lot of steps that normally they would be doing manually, they would delegate it and and um So you you're basically worried about that. But I'm just thinking that like in in in coding now everybody uses code code and similar tools and nobody There was a period of time in ancient history 6 months ago when people questioned that. Now, the consensus is that the best developers use AI. And it just makes them even better. The rich gets richer, right? Like this is Marxism. So, the 10x developers, the magical creatures who are super productive, become even more productive, and juniors are get getting eliminated because they cannot compete with even a basic LM. So, uh, so the question is now, I wonder if if Lean now becomes approachable because machines can do a lot, right? Like it was impractical for people to do a lot of formalization. Now, this will be by formalization. Will it now become a tool in a similar fashion for mathematicians, for students? So, you will always work alongside Lean or something like this, right? So, so it will not compete it will be like a coding tool. It will help you, but human is still in charge because a smart our computer architect developer, he knows what to ask, and that really makes a difference. And like, is this can this be the course of mathematics education? So, now you will teach with Lean from see, you know, math 101. Do you think that's that's going to happen? I don't know whether we'll teach with Lean because [clears throat] I'm learning Lean presents an extra barrier somehow. And the the way that you have to do mathematics if you want to do Lean is a little bit different from the way you do normal mathematics. A little bit less intuitive in various ways. Okay. Um, or at least that's how it seems because I've grown up the other way maybe. Maybe >> Maybe it will be some something better than Lean. But something maybe a platform that has Lean running in the background >> Mhm. that is a bit more sort of um, user-friendly than Lean. Maybe Lean is integrated into LaTeX and as you write a paper, like it gets verified. Yeah, exactly. I think if you've got some interface sort of a higher level language that you're using yourself Mhm. but Lean is um, verifying what you write as you write. Or Lean combined with uh, automatic theorem proving tools. Mhm. That could be Yeah, I I think we will get to that stage. But then there's a sort of race between people developing a platform like that and just AI getting better and better at maths. Right. On its own. Um so I mean a future that it would be very I think very nice would be if um we had platforms that made it really easy to do mathematics and have it formalized as you do it and uh um in other words, sort of tools that just help you think at your screen. Um and I I know a lot of people are interested in um developing such tools, including my group in Cambridge, actually. Um but uh if you have a really good platform like that, then you can also train an AI system to use the platform, so Right. Uh So that will be our ask for developers. If you want to build such a platform, it will have an impact. So maybe, you know, I'll close with the kind of general question because, you know, I come from Soviet Union, which had very strong math and physics, and a lot of people here come from China or India or France, where they have very strong STEM education, right? And so I think that's why uh you know, for instance, like, you know, there is a question, you know, women in tech, women in science. In America, it's very, you know, much dramatized, but in India, Russia, China, France, there is more balance women in tech because everybody gets strong education. There is no question, you know, of somebody not getting math. This is I think we're of the last generation which very educated without the AI. And now, of course, everybody says, "You don't need to know anything. AI will solve it for you." So I wonder, and you are at Cambridge, right? Like the citadel of uh kind of uh academia and tradition. And so, how do you see the role of math? Uh so math uh so AI is all math, as we know, is all math. This is all the way down, but in practical application, it's so much removed now from math that very few people can do the underlying math, right? The actual gradient descent, uh uh uh understanding matrices, it's actually it used to be a part of AI education. Now, nobody really needs this. People just can like ask right? So, I think like every year more and more people in the AI have no idea what is the underlying math, how it work How do you think like it becomes specialized to like PyTorch people optimizing for GPUs, they need to know both the math and how the computation becomes a very specialized tool. So, I wonder as a professor of mathematics, how do you see uh math kind of as a foundation of science? Are we going to be able to preserve it that way? Or is it going to become a very niche uh area or like how do you see the role of math in in education, right? Uh to make the people of tomorrow? I don't know what's going to happen. I'm I'm a bit worried about that. Uh as I like I said in my uh not in the keynote panel yesterday, there was a discussion about AI and education. >> Right. And I'm worried about this perception that we don't need to know anything because we can outsource all our So, there was somebody uh Bill Wren who said that uh we can outsource knowledge, but we can't outsource understanding or something like that. I think that's I think that's quite true and I think if we don't have um a significant percentage of people in a society who really understand mathematics and uh at some level, uh then we will operate we'll be somehow under the control of these systems. We won't we'll be passive consumers of them and um So, that worries me and I I think that maybe what happens. On the other hand, I think it will remain the case Mhm. that uh people who do make the effort to have a good understanding of mathematics will have a big advantage. Um bit like what you were saying earlier about the rich getting richer. If you Right. If you know how to If you If you know maths well, then you'll be able to you'll be better at um using AI and using it to do mathematics and having an understanding of what you can what you can use the tools for and so on. Um so I hope that uh that message will get through. Do you see young people, so you're teaching in France and then in Cambridge. Do you see young people coming into maths who will make great mathematicians despite of everything else happening? Like do you see like is there supply of smart young students Well, I'm very lucky to be um at Trinity College, Cambridge and we get regularly incredibly good mathematicians coming >> Mhm. >> there. So they're still being produced somewhere and get to Trinity. And for the moment, I think they are still noticeably ahead of what AI can Mhm. Um the very best students anyway. Um So there is hope. There is hope for the future of maths. Yes, there is. But uh Yeah, it's it's It could go either way, I think. It's We We really don't know what's going to happen. That's great. I mean, it's it's it's really great to see that you're doing things with Lean. So what is your goal for the next year? So, you know, if we meet here next year, what do you want to have achieved by this like in a year with your lab? Well, I was talking in my keynote a little bit about a platform that my group is developing um Mhm. that would in sort of encourage people to produce not just proofs, but proofs that are transparent, so you can see where the ideas come from. So my sort of main short-term hope Maybe short What I think of as short-term, but in this world, a year feels like long-term as well. Is just platform will be much more developed and we'll be able to demonstrate that it really is uh a good way of thinking about how to do mathematics. This sounds great. So, if you are ever in San Francisco Bay Area, we're on the uh meet up there. Just come and give us a talk and do a demo of the platform. We'd like We'd like our center student to show it. We'd love to play with it. Well, thank you so much. We appreciate it. Thanks a lot. Yeah.