## Link https://youtu.be/K5w7VS2sxD0 ## Clips ### I had a midlife crisis or a panic attack worrying about what mathematics is about eight years ago and it led me here start = 0:00 end = 2:30 ### Mathematics is now incomprehensibly large start = 2:30 end = 4:30 ### You might hope that in the 125 years since this theorem was proved that mathematicians might have simplified it and gotten to the core of what's going on to the point where we could make it easy, but that didn't happen - We can now prove some far more general theorems and the proofs are much slicker - But the proofs of the main theorems of global class field theory occupy an entire lecture series - That's where we were by 1900 - So as you can imagine, things have got a lot worse since then start = 6:30 end = 8:35 ### So by the 1980s, mathematicians had announced the proof of the classification of finite simple groups, and then they retracted it until 2004 because there was some misunderstanding, and this proof still has not been adequately documented in the literature, it involves reading papers by hundreds of people - There's an attempt to make a second generation proof - 13 volumes, big volumes, not like Euclid's book - Twenty years after it was announced, it still hasn't been written down - So that's what mathematics looks like start = 8:30 end = 10:05 ### In my opinion, mathematical ideas have become so complex that the traditional methods we have of writing them down are now struggling to cope start = 10:05 end = 10:35 ### A hundred or even two hundred page papers are not uncommon in mathematics - These things are sent to journals and the journals send them to referees - Referee work is unpaid - Referees are now explicitly told and have been for decades that it's not the referees job to check all the details - It turns out it's the author's job - Referees are supposed to check based on a feeling - There's a problem here start = 12:00 end = 13:20 ### Another weird consequence of mathematics becoming gigantic is we can't actually teach the students about modern mathematics - The goal of our top undergraduate programs seems to be "get to the 1940s" start = 13:19 end = 14:20 ### And we think this is normal - This is now normal - And I look at what we're teaching our undergraduates and I look at what I learned as an undergraduate and it's just the same, it hasn't moved on at all - This isn't the case in computing start = 14:20 end = 15:15 ### Our papers are sometimes incorrect, more often they're not incorrect but they're incomplete start = 15:40 end = 16:10 ### About ten years ago I got an email from some random graduate student saying "I was reading one of your old papers and you said this this and therefore clearly this, can you explain exactly how you get from here to here" and I just read it and I thought "I definitely knew this at some point" - And it's just a clear indication that I'd not written enough information in that paper - And I'm skeptical about whether the refereeing process is scaling start = 16:05 end = 16:40 ### I know terrible things that I'm not going to indulge here - I'm not going to name any names, but I know important papers that just contain incorrect claims, and the experts all know they're incorrect, and there's some informal, there's some 8 page pdf that gets circulated between the experts that explain how to fix everything up start = 16:35 end = 17:05 ### I discovered one of these things myself, I was like "I can't follow this line at all, this looks wrong to me" and I asked somebody and they said "Oh yeah yeah yeah, have you not seen the erratum?" The unpublished erratum - And once you find the error you get sent the erratum start = 17:05 end = 17:33 ### But it's ok! Because it's always been like that. And the historians of maths are quite happy to tell you that. The nature of research is there's chaos at the boundary because the boundary is the living part of mathematics and the ideas are partly formed and falling into place. And this is why mathematicians don't think there's a problem start = 17:30 end = 18:40 ### So what's happening today? People have been doing maths for thousands of years, and for most of those years technology was limited. In the 1960s and 1970s, mathematicians started getting access to these things that were superhuman at calculating, but that affected mathematics much less than you'd think. A powerful computational tool isn't the sort of thing that will help them. They're doing stuff that somehow you can't compute because everything's sort of intrinsically infinite dimensional and uncountable. And if you're doing that kind of mathematics then a tool that can calculate very effectively might be less use than you might think start = 18:40 end = 20:20 ### But the point of this talk is that other things have happened in the last few years. Computers are now being used in other ways, and these other ways could impinge upon mathematics start = 20:10 end = 20:40 ### Two tools that are changing things. The well known one: the large language model, and the less well known one: the computer proof assistant start = 20:40 end = 21:20 ### The language model and mathematics start = 21:15 end = ### Then there's this more exotic thing, the computer proof assistant. Explaining why mathematics is so much harder to capture than other forms of reasoning start = 27:25 end = ### These tools are not a recent thing. They've existed for decades. But they were not on the mathematicians radar. They were being designed and used by computer scientists and mathematician adopters you could count on the fingers of one hand up until about 2020. start = 29:25 end = 30:40 ### But now they're good, and in particular the Lean theorem prover has got a lot of traction among mathematicians start = 30:15 end = 30:30 ### As a result of mathematicians getting involved, we're starting to see the work of Fields Medalists translated. This is part of why mathematicians are now waking up to these things. But the translation is currently essentially all being done manually. start = 30:25 end = 31:08 ### Where are we now? Just like the language model, these things have told us nothing profound that we didn't already know. start = 31:08 end = 31:30 ### The LLM has not yet had its deep blue moment for research level mathematics. However, the Computer Proof Assistant technologies like Lean absolutely are super human with respect to checking mathematics. I've been using these systems for 8 years, and basically every time the human says something and the computer says something else, every time the computer's been right. start = 31:20 end = 33:20 ### Language models now solve the computational problems they're bad at by writing code and running the code start = 33:20 end = 35:00 ### We've taught the language models python, why not teach them Lean? So that when you ask it a proving question, it writes Lean code. start = 36:00 end = 37:00 ### start = end =