Mathematics Just Changed Forever — Kevin Hartnett

16,707 words · about 67 min to read

0:01 The Fields Medalist, Peter Scholze.

AI and proof assistants revolutionize mathematical verification

0:03 The proof was just sort of six pages of technical calculations that we had skimmed through at best. He'd become convinced that nobody had actually read his work. We found four Fields Medalists have actually proved theorems in the annals of mathematics. Strictly speaking, that theorem is not true. The humans hadn't bothered to mention that, obviously, n had to be at least three. When you prove something using a tool like Lean, you can get certificates.

0:33 You have an algorithm then can check whether the proof is correct or not. The machine says it's right. Something has now actually finally read it. AI is coming for mathematics. This is absolutely clear. Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean mathematicians have had various different reactions to this, ranging from you know, what could only be described as grief Can I make a machine proof stuff? Sure.

1:08 But I'm interested in understanding it. Right? And I'm still the one who has to understand it. It can output millions of potential proofs but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are. But a checked proof can still be a proof of the wrong thing. It's about the ideas. It's about the understanding.

1:33 You know? Here's the GitHub repo. Read it if you want kind of thing. Does anyone want that? You multiply two numbers on a calculator, you get a result. You just take the calculator's word for it. Nobody's gonna check it. four hundred years ago when Johannes Kepler was in a greengrocer, he had an interesting idea.

Massive computer-assisted proofs create a peer review crisis

1:55 He was looking at the way the oranges were stacked on top of each other in a pyramid structure, and he thought that that might be provably the densest possible configuration. Unfortunately, it was impossible for him to know for sure whether his idea was correct. So fast forward to about 1990. This had become Kepler's conjecture. It was one of the most interesting problems in mathematics, and many famous mathematicians had spent decades trying to solve it, honestly, without making too much progress.

2:27 Now, two mathematicians, Thomas Hales and Samuel Ferguson, they reduced it to 1762 combinations. Now, back in these days, computers were incredibly slow. So almost on a case by case basis, they had to write this insanely optimized computer program with lots of heuristics doing intersection checking and so on to individually prove that each one was less than about 0.74, which is the ratio of the optimum, you know, pyramid placement.

2:58 Kevin Hartnett tells this story in his brand new book, Proof in the Code. Now, the book isn't just about oranges and, Kepler's conjecture, but that's certainly where it starts. But, the the thrust of the book is mostly about this gentleman called Leo de Moura, who is the creator of Lean and the tumultuous and interesting fascinating journey that he went on with many of his collaborators to get to where Lean is today.

3:27 And he was saying how this guy Thomas Hales, he actually had a bit of paper on his on his wall. And every single one represented one of these configurations, and they became harder and harder as the density converged towards naught 0.74. And it took him many, many, many years to do this, and eventually he did it. So he had 1,767 computer programs for every single configuration of these balls and he was elated.

3:53 So he published his work to the Annals of Mathematics expecting a celebration that he had just, you know, proven Kepler's conjecture. Unfortunately, that's not what happened. He dumps this proof on the journal on the editors of the Annals of Mathematics, the most prestigious journal in the field and they essentially don't know how to referee it, how to kind of send it out to other mathematicians to verify its correctness and it languishes for like many years without actually being kind of determined true or false.

4:23 Because if you think about it, many years, the way mathematical proofs were done were high up the abstraction mountain. So they would make these really high level arguments and it would just go without saying that certain arguments had been proved before. So you didn't need to go step by step and it was very very parsimonious. And when you submitted your paper to a journal, they would be able to review it and they would be able to check your work. But this was different. The sheer volume of it made it almost impossible to check.

4:52 With Kevin's permission, I'm going to read out a few bits from his book just to give you folks a little flavor of the story. So here we go. Every part of the proof that reviewers looked at seemed correct, but the proof as a whole was such a sprawling edifice of calculations buried deep in computer code, and it was hard to determine how they all hung together and whether in the end they yielded the proof Hales claimed they did.

5:20 When Hales had finished the proof in the summer of 1998, he had imagined he would use the methods he had developed for Kepler to attack other similar problems. That's how it goes in math. Methods that solve one hard problem are generally good for solving others. Yet as the review process dragged on without resolution, Hales changed his mind. He couldn't get the math community to verify his proof of Kepler's conjecture.

5:49 Why would he caught frustration by applying the same methods to other problems? This is Leo Demora, the creator of Lean The paper was accepted with a disclaimer saying something like, we're ninety-nine percent confident this proof is correct. But then Tom starts using proof assistants.

Large math proofs resemble modular software engineering projects

6:08 This all happened before Lean. He uses HOL Light and Isabelle to to do this work, but it was a milestone. I mean, it was a big result that has been formalized in a in proof assistant. And and Tom was famous twice for for solving the Kepler conjecture and for using a proof assistant. Right? In our paper that the math community cares.

6:35 And the fact that he decided to do the next projects using Lean was a big deal on Lean. But the remarkable thing is that it still feels unsatisfying. Even if we can solve problems from first principles end to end, there's a kind of understanding debt because we can't hold it all in our brains at the same time. So how do mathematicians know when a proof is correct when they can trust a new theorem and then use that as an input into additional proofs?

7:01 It's very much a social process. They, they kind of have a general understanding for what works already. They kind of like know the person behind a proof. They can kind of like trust that this person kind of understands the way things should go. And then they can check a proof. They can check the kind of the lines in the argument but they don't necessarily check every last line all the time. And for the most part that works especially when proofs are kind of close to the existing body of knowledge when they kind of go just incrementally beyond things we already understand to be true.

7:33 Yeah. I mean, suppose, like, a fundamental noob question is, why does it matter that we can prove something versus just know something is true? Well, I I I think the main thing is that we can when you prove something using a tool like Lean, you can get certificates. You you have an algorithm then can check whether the proof is correct or not. for math, for example, this is useful for trust. I mean, you can collaborate with people you never have met.

7:59 I think many people in the math community got excited about that even before AI. It's like saying, oh, wow. I can work even with high schoolers, and they can contribute to my projects.

1 Highlight · Treating massive math proofs as engineering projects

8:11 I don't need to check if their proofs are correct or not. a big math projects, you can view as engineering projects. I mean, Johan Commelin, for example, he's a really hardcore mathematician. And he he he's a software engineer. He doesn't know, but he's a software engineer. He breaks big projects in smaller pieces, and people can fill the smaller pieces.

8:37 He's like the architect of the the project. And people start filling the holes and he doesn't need to check manually. Right? Of course, he will look later for to see if he's he can people can maintain this proof later. But you don't have to keep thinking about is this the proof is correct or not. He knows the proof is correct. He can clean up, improve, but the proof is correct.

9:03 This is valuable. Earlier this year in Melbourne, I caught up with our favourite category theorist Paul Lessard we want provenance. We want to know why. Right? And that's the thing that I'm much more interested with if you wanna talk about symbolic AI.

9:17 The thing that's interesting is I don't want merely things that don't get it wrong because, like, that's still not enough. I wanna know why it comes up with a particular answer. I want the reason. Thomas Hales' proof was extremely verbose. It was complex. He was going through on an instance by instance basis, and it wasn't very abstract like the proofs that came before. And does that remind you of anything? Yes. If you look at AI proofs now, they have a similar property.

9:44 Right? They are they look a bit like spaghetti, and they're inscrutable to us, and that doesn't give us a very satisfying feeling. So can we say that they are still legitimate? Are they still as good as the abstract versions? Well, it's not less legitimate because he settled the question. I think one thing that one way in which you can kind of like assess the value of a new mathematical result is it like does it enable additional results? Do you invent new concepts, new abstractions, new definitions in the process of prosecuting an argument that then have like widespread utility for answering other questions?

10:17 In Hales' case, I mean there were some computational methods that he would have wanted to apply to other problems but he was not inventing kind of like broadly new mathematics. In a certain sense the techniques he used were like fairly elementary, he himself kind of acknowledges that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he saw Fermat's Last Theorem where he had to like invent some very like powerful new concepts that just opened up entirely new branches of the field.

10:45 So Hales' Hales' proof was not like that. So there's utility probably in the generation of proofs that are not constrained by our desire for interpretability. But once you talk about, like, doing actual mathematics, like, that's I'd like I still like to think that, you know, the human understanding is still centered in this. It may not be, but I think those those are different quests at some point. It's like, can I make a machine proof stuff? Sure. But I'm interested in, like, understanding it.

11:13 Right? And I'm still the one who has to understand it. There is resistance because mathematicians don't see, by and large or didn't see the value in that type of time investment. So Hales invests twenty person years in formalizing his Kepler conjecture result and at the end all he gets out of it is assurance that the thing is correct. Now that is like that's much less exciting than getting new math and new discoveries.

11:39 It's especially not exciting in situations where you're already fairly confident that things are correct. So in most cases, mathematicians know when things are right or not. They're not troubled by correctness. there's a factor called the de Bruijn factor which is the amount of lines of code you need to write in lean for every one line of informal math like in a LaTeX PDF and it's very high, twenty to one often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something.

12:09 So that's really where the resistance comes from. They don't see the utility of lean for the thing they most care about which is discovering new math. This episode is supported by Cyber Fund. If you're building at the frontier of AI, they want to hear from you. Cyber Fund believes the future belongs to AI natives who want to achieve the impossible. And that's why they're introducing the Monastery for AI native founders.

12:38 It's an environment of pure focus and rapid execution for founders operating at AI native speed, and they're offering teams $2,000,000 each to participate.

The small trusted kernel guarantees interactive theorem prover correctness

12:50 Apply now at cyber.fund. folks who are new to Lean, what what is it what is it all about? What can you do with Lean? Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. But the cool thing is that you can prove properties about your codes. You can state mathematical theorems. You can prove them. You can build a mathematical library like Lean's mathlib.

13:16 So in Kevin's book Proof and the Code he gives a precise definition of a kernel which is a component in an interactive theorem prover like LEAN. An interactive theorem prover has two basic components: a logical foundation, which determines

2 Highlight · The critical role of the small trusted kernel

13:33 how ideas are expressed and interact with each other, and a checker program, called a kernel, which verifies that programs correctly adhere to the rules of the logical foundation. The kernel answers the first question anyone asks when they learn about an ITP, which is that if the ITP says a proof is correct, how do I know it hasn't made a mistake?

13:58 The kernel is how. we have the notion of a small trusted kernel. Lean's massive, has zillions of bugs. Right? But to trust our results in Lean, we only trust the kernel. That's much smaller. Right? The cardinal sin for a kernel is to verify false statements as true, which is far worse than rejecting true statements as false.

14:25 Calling true statements false merely creates a roadblock. It's an inconvenience. But calling false statements true opens the door to validating countless more false statements, all justified by the original false claim. At that point, the ITP is useless until the bug in the kernel is fixed. Over the years, ITPs such as Agda, Coq, and Isabelle had all contained bugs in their kernels that allowed users to validate false statements.

14:57 His answer was independent checking. Let users build their own kernels. To make this option realistic, de Moura knew he would need to keep the kernel as small and minimalistic as possible, comprising as few lines of code as he could possibly achieve. Among the ITPs already on the market, de Moura admired the minimality of HOL Light, which had a very small kernel.

15:23 Back in 2006, there was loads of duplicate effort at Microsoft. Some were building their own theorem provers, some were working on obsolete theorem provers and it was at that point that LEO decided to start working on Z3. Leo built Z3 in order to provide a systematic way of checking that software had no bad pathways and he could kind of do it in in the style of a mathematical proof.

15:49 Like he could kind of prove with Z3 where you construct you construct a pathway through the software as a series of variables and you prove that those variables can never take the right combination of values that would make a statement true. And if you prove that it cannot take, the software cannot arrive at that state, that set of variables, then you just have ruled out categorically a bug at least in this like one particular direction.

16:15 Leo built Z3 as a way to automatically check different pathways through Microsoft software for bugs, prove, guarantee that there were no bugs. Z3 is a type of program called an automated theorem prover because all of this work once you set things up is done automatically. There's not a lot of human input at that point. Z3 was quite powerful. It caught lots of bugs and saved Microsoft hundreds of millions of dollars in the early two thousands.

16:45 Leo though, following the great success of Z3, not just for Microsoft but like he and his collaborator entered it into these automated theorem prover competitions where all the ATPs from all over the world come together and they're given a bunch of problems in a set amount of time and whichever ATP can kind of correctly prove true or false for those problems, most accurately wins. Z3 was the world champion at. So he essentially had climbed to the top of the automated theorem prover mountain but he also was dissatisfied with the kind of the fundamental limitations of automated theorem prover technology.

17:19 Like there's kind of a limited range of things that programs of that sort can prove. A limited range of knowledge that they can verify is correct if you wanna go a little broader. And so he turns his attention to building a related but more powerful type of program called an interactive theorem prover where you have a much richer expressive language that kind of just a wider range of truths you can try to encode and verify and interactive in the sense that the human kind of a human user can can nudge the program towards greater expressiveness.

17:52 It makes it a much more powerful thing. what my book is is ultimately the story of how Lean, this interactive theorem prover that de Moura builds to verify the correctness of software programs in a richer way than he could with Z3 gets in a sense co opted by mathematicians who see the potential in it and for the first time an ITP breaks through into a more mainstream way of working in math. But in Lean, because it uses this dependent type theory, it can be used for solving many, many other problems in abstract mathematics which are significantly more complex.

18:22 Jeremy Avigad, a mathematician and philosopher at Carnegie Mellon, has been corresponding with Leo for many years.

Dependent type theory enables modern abstract mathematics

18:30 I'm a mathematician by training, specifically a logician. And so, you know, what I like about logic is that it's somewhere between mathematics, computer science, and philosophy. So here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started just as a hobby, just messing around with them because I thought they were interesting around the year 2000, so quite a long time ago. Just after midnight on the West Coast, de Moura sent a long email to the group softening some of the concerns he had raised.

19:00 I apologize if I sounded too negative today. I'm still trying to understand the alternatives, he wrote. I've been reading about all of these proof assistants and studying their implementations. When I questioned the need for dependent types or any other feature, it's because I'm really impressed with HOL Light's design and implementation. In my opinion, it's the most elegant by far.

19:27 He acknowledged that this perspective was at odds with Avigad's. I understand Jeremy's point when he says HOL Light would be really inconvenient for doing abstract algebra. The design of Lean was being negotiated in real time. I want to use higher-order logic. It's a simpler foundation, much easier to implement.

19:53 And for many software verification tasks, it's enough. Right? But for doing it abstract mathematics, it's not. it's important to have a good library math library for verifying software. For example, cryptography, we need a lots of math. Differential privacy is another example. So having a good mathematical library is important even if you only care about software verification.

20:20 In in my point of view, you have it's important to have users. that's what the users wanted. And I want support. I want to have Jeremy as a user. I knew others would come and pay off. I mean, many people, many of my colleagues that work on cryptography, they say. For example, one of them is a former colleague of mine, Cédric Fournet. He uses Lean now.

20:47 And he told me, look, mathlib, the Lean Mathematical Library, have the right abstractions I need for verifying cryptography. Right? So I mean, because of all the generality that's having dependent type theory provided, we have a library that's more expressive, that has the right abstractions, is cleaner. Yeah. It paid off long long term. It paid off.

21:13 It was a lot of extra work at the beginning. And to get it right, it was also lots of work. But it's I think it's paid off. I suppose one of the biggest tensions and and ultimately the the battle that you won was that you wanted Leo to support this dependent type theory because that was very useful for solving the types of problems that you were interested in. before starting the Lean project, I had worked in 2009 and 2010.

21:39 I spent a sabbatical year working on the formalization of Feit Thompson theorem. And that is in a proof assistant known as Rocq. And Rocq is based on dependent type theory. Before that, I had worked with Isabelle extensively, which is a proof assistant based on a simpler logical framework called simple type theory. Isabelle is a wonderful system, and so for many things, it's it's absolutely ideal.

22:04 It still to this day has excellent

3 Highlight · Why dependent type theory is essential for modern math

22:07 automation, automated support. So for certain types of mathematics, it it was really a great system. But then for certain types of things, you hit a wall. So, in modern mathematics, mathematicians talk about algebraic structures, you know, axiomatically characterized. It they're really ubiquitous. There are these complex networks of algebraic structures, and simple type theory is just not good for that.

22:33 And so after my year working with Rocq, it became clear to me that this was the framework that was capable of of doing that type of mathematics. And I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions, that to do the mathematics that they wanted to do, they needed this very expressive framework. So the thing about dependent type theory is that it's very powerful, and very expressive. But I like to quote, you know, the Spider Man franchise.

22:59 You know, with great power comes great responsibility. You know, the very powerful language. It's also very hard to implement. It can be more difficult to use. There are a lot of gotchas and kind of corner cases. And so it was a more weighty and complicated and difficult framework. And when Leo first started the project, he was aiming for simplicity, you know, a very simple, formal, you know, foundation. And so he needed convincing there that the trade off was worth it.

23:27 I think, you know, in the end he came around. I mean, now he's one of the the biggest proponents of dependent type theory. He, you know, you know, soon after, he

23:34 would say that, you know, it's it's really beautiful. And so he he recognized the benefits. But again, coming coming from the outside and, you know, without the filament familiarity, yeah, he he needed convincing at first. But ultimately Leo emails Jeremy back during that summer of 2013 and tells him, I've decided to go with dependent type theory and Jeremy basically does a dance at home in Pittsburgh because he just knows the the seeds are there now for Lean to be useful in math and the way he's always wanted an interactive theorem prover to potentially be useful.

24:06 It's funny as a developer. When you're using the developer hats, usually, you want to go to whatever it's simpler to implement, and you forget that you sometimes will be the user of this tool too. I I always joke, honey. If I'm using my user hats, I want this feature. If using the developer hats, I don't want it. Oh yeah. So Leo is like extremely self critical. I mean, just there there are many moments in the story of the development of Lean where he has some users and they love it and he says it's shit.

24:35 I mean he just thinks it's terrible. He all he sees is its flaws. He wants to very doggedly fix those flaws. At Microsoft, Leo feared a poor annual rating would jeopardize his research. His manager never gave him one, but the fear persisted. Leo is just a researcher, a computer science at Microsoft Research. He's not a project manager, he's not a product manager, he doesn't have like a team of engineers working with him, it's just him and idea.

25:03 Through Jeremy, suddenly Lean very quickly gets a number of mathematicians who want to start using it. They love it, they don't think it's shit, they think it's way better than Leo does but they also have all these additional feature requests. Wouldn't it be great if we could do this? It would be much easier if we could do that? Can we have like a richer UI? Leo wants to please the users. He's extremely like users oriented in that way. It's very hard for him to receive a piece of feedback especially if he recognizes it's kind of fundamentally correct and ignore it.

25:30 So he finds himself kind of responding rapidly to all these users who are not even the users he intended to be building for who are doing something that's not even what he planned lean to be useful for. But he starts fulfilling the request. I think he's like barraged by emails ultimately later by Slack messages. He can't really say no to them but he comes intensely frustrated because he feels like they're taking him for granted. he feels like they think that he has more time than he does and most importantly, he has like a vision for where he wants lean to go.

25:57 There ultimately are four versions of lean. We're currently on lean four but for years, you know, we're at lean two and Leo saw where he wanted it to go and he felt inhibited in his ability to find the time to do it because he was answering all these essentially like user support questions and queries from mathematicians. one of the earliest adopters of lean and kind of most enthusiastic evangelist for lean is a mathematician at Imperial College in London named

Mathlib crowdsources a digital library of mathematics from scratch

26:24 Kevin Buzzard My name is Kevin Buzzard. I'm a number theorist working at Imperial College London. I spent some time at the beginning of this century bringing up three kids. when that was sort of over and they were able to look after themselves a lot more, I wanted to get back into doing hard research mathematics. And I realized that there was a huge amount of material that I was gonna have to sort of catch up I had some kind of midlife crisis around that time because I was trying to read it, and I couldn't understand all of it.

26:58 And I would find what I thought were mistakes in the literature. then I started thinking, well, wait a minute. Like, what are we like, what this is very abstract stuff, it's not immediately clear there's any sort of concrete applications, so there's nothing that we can sort of test these things on in reality. And if they're not right, then almost, you know, what is the point of this stuff at all? So I had some kind of crisis, and I started thinking, you know, would it be possible check mathematics using machines?

27:29 Because, you know, technology is moving very fast. and so I went down some kind of rabbit hole, just kind of exploring the software that was out there that was claiming, you know, that it could check mathematics at superhuman accuracy. And it absolutely could check mathematics at superhuman accuracy, but the problem was the mathematic ninety-nine percent of what it was checking was really, really basic material known hundreds or maybe even thousands of years ago.

27:55 So the but but by that stage, I kind of got hooked, cause I realized that there was this weird new way of doing mathematics, I'd never really seen anything like it before. And I started to realize that actually, doing mathematics in the software, even though it was very basic mathematics, was a huge amount of fun very different to doing it on paper and pencil. And so then I was in this hole, and then suddenly the original questions just went out the window.

28:20 Then I was just like, oh, this software is really great. You know? What can we actually get this software to do? And at the time, it was just like we could barely get it to do undergraduate level mathematics. But because it was great fun using it, You know, that was how I ended up switching. By 2016, Kevin Buzzard had time to return to the p adic landlins program. A young talent named Peter Scholze had transformed the geometry of numbers with perfectoid spaces, and Buzzard wanted to be part of the revolution.

4 Highlight · Preventing mathematical research from becoming a house of cards

28:50 But as he read the papers that followed Scholze's work, his enthusiasm gave way to concern. Buzzard liked to see every detail spelled out. disliked vagueness and assurances from authority, what he called the opinion of the elders. And that perspective could bless promising ideas before they were fully defined. But in the papers he reviewed, Buzzard thought that it had become a permission slip for sloppiness.

29:19 His critique was not of Scholze's work, which he actually found brilliant and rigorous, but of the results built on top of it. He noticed mistakes in some papers and logical gaps in others, and experts just brushed him off, assuring him that the thrust was correct even if the particular arguments were loose. Buzzard understood that young fields can be inexact while mathematicians work out how all of the pieces fit together, He saw one sloppy incomplete paper building atop another and worried that his area of mathematics was turning into a house of cards.

29:54 So to him that was the draw of Lean, was he wanted to take these papers that had developed in his field, formalize them, like convert them into this computer programming language, determine with complete certainty whether they were correct and if they weren't fix them but if they were then it would just kind of give him renewed confidence to kind of proceed in research in this area. So here's a small example. The ring tactic constructs a proof of this algebraic identity using machinery from Mathlib.

30:23 Lean then checks the proof, and it says no goals, which means the task is complete. When Lean, when you boot up Lean, Lean does not know any mathematics.

Crowdsourcing mathlib to build a digital library of mathematics

30:32 It's equipped with basic axioms and rules for math, so it has some kind of just like some understanding of mathematical logic, What So you need to do is equip it with a library of definitions. And this is the parallel story in my book. There are kind of two key stories, two dreams almost that are very dependent on each other, sometimes in tension with each other. So one is Leo's vision for Lean, the software he wants to build. The other is the development of what comes to be called mathlib, a library of digital mathematics which is spearheaded by several of the main characters in the book.

31:05 People like Kevin Buzzard, Johan Commelin, Patrick Massot, Jeremy Avigad is very involved, Mario Carneiro is another figure who's very important in the development of mathlib. The vision for that is it will be a crowdsourced effort to define in lean language basic concepts in math from the ground up. So starting with even just like high school level math to college level math so that you have the ingredients to then later encode more sophisticated forms of math.

31:36 That's kind of the that's how lean breaks beyond just these combinatorial results like the four color theorem and Kepler's conjecture and becomes a place where you can express very deep kind of frontier level abstract math. It's through the development of mathlib and actually I got in interested in this story back in 2020 when I was assigned an article for Quanta Magazine on the development of mathlib when it was still quite early days. In that article, I say I said that mathlib had the spirit of a barn raising.

32:04 It was just like this like community effort to get this massive thing done without any central authority, no central resources. And so slowly, this library of digital mathematics is created mathlib is Lean's mathematics library. so it was born about the same time that I started working in the field. it was thirty thousand lines of code containing a bunch of completely basic theorems about finite sets, and some very basic undergraduate level mathematical definitions, and that was it.

32:37 It didn't even have a definition of the real numbers when I started, or it it just got this concept of the real numbers, which is something known to, yeah, known to the ancient Greeks and the Babylonians, you know, is, you know, thousands of years old. And it didn't have the complex numbers, which are, I guess, from about five hundred years ago. So there was clearly a lot of work needed you know, I spend a lot of time teaching. Right? That's part of my job.

33:03 I teach these undergraduates. They come in. And the way it works at university in a mathematics department is you kind of say, okay. You learn all this stuff at school, but actually, we're start again from the basics and just work through everything quite quickly. And, one of the things we teach them is how to define the complex numbers, which are these basic number system that goes back to Descartes. I kind of thought, oh, this thing doesn't have the complex numbers. Let's teach it the complex numbers.

33:29 So there we go. We define the complex numbers, prove basic things about it, and it was great. And I made a pull request. You know, this is a free open source maths library. So I made a pull request to this maths library, and then it got merged into the main branch. And suddenly, we've got complex numbers copyright 2017 Kevin Buzzard. I'm just thinking, great. Now what's the next thing that we teach them? Because I'm now I'm thinking, you know, what what do we actually teach our undergraduates?

33:55 What's missing? And and what should be in this library? Why don't we just contribute to this library? But, of course, there's so much stuff that one person can't do it. So I wrote the undergraduates it was absolutely critical. We'd just got to the point where all my kids could make their way to school by themselves. They could make their way to and from school, you could leave them in the house, and they were unlikely to, you know, set anything on fire or, you know, it'd be illegal. So so I could stay late at work.

34:21 Like, one evening a week, I'd stay late at work and just let the kids muddle on by themselves. And, and I would teach undergraduates how to use this software, and then I would get them to start, you know, transcribing what they were learning in their in their undergraduate degree, just just teaching it to this machine. So the library just I mean, there was lots of other people around the world well, not lots, but there were plenty of other people around the world doing the same thing, you know, I I was treating this thing as an undergraduate at the time.

34:49 So it's 2017, and the question was, you know, let's just imagine you've enrolled on our degree. You know, can we can we actually teach you at the same rate as we teach the undergraduates? And it was it was just about possible. You know, the the the thing was learning at the same rate as our students at the time. But, you know, three years later, we could sort of step back and say, well, actually, you do basically know most of the things we teach our undergraduates And, yeah, that was sort of when I fell in love with it, you know, because I'd wanted to teach it.

35:19 But when is a new mathematical idea ready to become part of the library? mathematics is is an interesting object. It's this gigantic abstract object that humans have created.

Only polished and well-understood concepts belong in the central library

35:31 And at the boundary, there are things that haven't you know, they're not quite fully formed. There are ideas which sort of sort of work or work in some cases, and, yeah, we we need to think about how these ideas should mature what they should really look like. Mathematics needs to mature, sometimes at the boundary, it's it's not material that's ideal for the library. Yeah. What we want in the library is ideas which are really well understood and that exist in the correct generality.

36:02 You know, we want polished we want polished mathematics. stuff which is still a bit chaotic, you know, one can attempt to teach it to the you know, we can teach it to the software, but we don't necessarily want to add it to the library. The library wants to take sort of fully formed, well thought out, you know, beautiful conceptual ideas, which sort of know their place. essentially, all of the library now is is is well thought out, beautiful ideas some of the things in the library are actually stuff that happened in the last few years, but a lot of it is much more basic stuff that we feel like we understand well because that's, you know, that's when you want to commit.

36:43 Right? this is part of the work of our community, trying to understand what humans have done and to get it into the correct, you know, most abstract, most useful form for future work. Because you don't really want to put some concept in the library, and then it gets generalized and simplified a bit, and then somehow you need to rework the entire thing. This we we try and avoid this. We we like to get things right first time. Occasionally, we have had to go through and change a fundamental definition, can be a huge amount of work because then, you know, many thousands of files then break and need to

5 Highlight · Using high-profile theorems as marketing stunts for Lean

37:16 be fixed. Kevin Buzzard has like the instincts of a showman. He's like a natural marketer and he comes up with a couple essentially schemes or stunts for doing this. And one of them actually is to formalize a mathematical object called schemes which is an algebraic geometry. It comes from Alexander Grothendieck in the mid twentieth century. He says to himself, if we can formalize schemes in lean and I can tell the world about it then mathematicians will suddenly start to believe that this is useful for the types of type of like frontier math that they themselves care about.

37:49 He does it and he's met with like a collective yawn because people tell him, Kevin schemes are old math. Right? Sixty, eighty years old. I knew this when I was in graduate school. This is not frontier math. And Kevin's like, okay. That's true. What is frontier math? And in this period, around 2018, frontier math is this object called perfectoid spaces which is something that was created by a German mathematician named Peter Scholze who is today and then as well considered maybe the greatest living mathematician.

38:20 Perfectoid spaces are truly state of the art objects in in math and Kevin says, alright, if we can formalize them, if we can show lean is capable capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything. And so he and Massot and Commelin start this effort, just the three of them to create a blueprint essentially, a kind of a guide to the things they would need to define and lean in order to be able to write the definition of a perfectoid space.

38:51 It's essentially a punch list like a construction project. You know, we would need you to find this and this and this and this and ultimately we get perfectoid spaces. They succeed at that and what that I think an important point to emphasize is mathlib is all of the math that anyone working in lean can draw on. At the moment it's essentially maybe first year graduate level math. They have all of undergraduate math modulo a few things here and there.

39:19 They've got all of first year graduate level math. Then there are these extreme spikes from grad math to the far frontier of the field which is like extremely far from graduate school math. Perfectoid spaces is one of the first examples of we have this foundation, now we're gonna build this like narrow skyscraper to the frontier. Perfectoid spaces is is the first example of that. That stunt works the way Buzzard hopes it will work.

39:45 It captures a lot of people's attention, it boosts Lean's profile and it kind of starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math. So I was just beginning this was back back so back in 2017, I was having this

Formalizing theorem statements before tackling complex proofs

40:07 midlife crisis and trying to work out what was going on in the area of, you know, computers proving theorems. And I discovered, to my amusement, that there was a big conference in the area that I was far too late to register for in Cambridge taking place in two years' time. But came this was at the Newton Institute in Cambridge, and they were ahead of the game. This is pre COVID. But they were already recording and live streaming their talks on the Internet.

40:37 So, even though I couldn't go to the conference, I could still watch the talks. And the first talk was given by Tom, and I imagined, that he would be, by by Tom Hales. And I imagined that he would be talking about his proof of the Kepler conjecture. But in fact, that only formed a very small part of his talk. He was talking about, you know, exactly the thing that I've become worried about. He he was talking about formalizing modern mathematics, you know, perhaps all of modern mathematics.

41:07 And one of the things he suggested was that perhaps it was time, that we got mathematicians not to learn enough about these computer theorem proving languages to actually type in all their proofs, but just to literally type in the statements of their theorems. Because that's a much easier job, just saying, okay. I claim that I proved this, and here's what it looks like in English. But here's what the statement of the theorem looks like in a formal language, and then the proof is a hundred pages long.

41:35 And and translating the proof into this language would be, you know, would be like a PhD thesis worth of work, you know, a gigantic problem. But perhaps we should start persuading mathematicians to state what they're doing in this formal language because then there's no ambiguity. You see, in in reality, you you would imagine that maths was this sort of perfect language where everything can be expressed, you know, in a in a completely unambiguous way.

42:01 But in practice, this is not this is not what happens. In practice, you you read you read section 3 of the paper. In section 3, it says, from this point, p will be a prime number which is at least five. And then you read something in section 7 of the paper, and it's just talking about a number called p. And you know from reading lots of number theory papers that p will be a prime number. But this this this fact that p is at least five, that was sort of slipped in to section 3.

42:27 If you start reading in section 7, you don't notice this hypothesis. And so it looks like the theorem says something. You know, the theorem isn't the theorem if you read the whole paper, then the theorem is correctly stated. But if you're just trying to work out, you know, what's going on in section 7, then you might make an error. And Hales was like, we need to fix these errors. We've got tools that can do this now. And I just thought, this is a great idea.

42:53 You're trying to trying to translate all the I'd I'd I was two weeks in, and I'd realized that the systems knew nothing. But somehow, the idea of teaching the system's basic mathematical definitions seemed to be much more viable than teaching it, you know, a hundred page long proofs of theorems because many mathematical definitions are quite short. In fact, that was what the library looked like in 2017.

43:18 It contained some some definitions that mathematic that, you know, undergraduates find quite difficult. You know, second year and third year, fancy things like topological spaces and, you know, theory and rings and things like this. But actually, just writing the definition down is only a few lines of code in the computer. It's proving all the theorems about it where all the work is. So if you can just write down the definitions, then we can start stating the theorems.

43:44 And, this just seemed to me like a viable way to move forwards whilst engaging, you know, with interesting material. So it it was just a completely my idea was just like, let's check these modern papers, remark that's completely impossible. Whereas Hales' idea was viable. In fact, it was somehow not quite viable at that moment. You know, Hales pushed for Hales pushed for it to be happening in 2017, and it was somehow too difficult to do in 2017.

44:14 But actually seven years later, I wrote a grant proposal to do exactly what Hales had said, you know, just to do the same thing. And, and we've spent a year working on this now, and it now is sort of it's becoming viable. We're taking, theorems published in, you know, the top pure maths journal, this decade, We're trying to translate just the statements of the theorems, into the language of the software.

44:43 And, again, we're twenty percent through. And so that's some indication, that at least, you know, this dream is slowly becoming a reality. And I would imagine that in a year's time, we're gonna be far more than twenty percent through. So some so so Hales had these ideas which have taken years to become real, but now, you know, now they are becoming so, yeah, I I would say that Hales was really of you know, this this was a visionary talk, and now his vision is coming to fruition.

45:12 Formalizing a proof or writing math in this formal language, right, is very kind of tedious. You have to spell out every little detail. Even things that are kind of trivial or obvious to mathematicians, you need to kind of convince the computer of their correctness. There are a few moments in the book where a mathematician is reading a proof that's written informally on a PDF and they want to formalize it, incorporate it, right, they want to formalize it in lean and what they discover is often it's the most trivial statements that are most obviously true to humans are the hardest to convince lean are correct.

45:45 Things like one plus one is two. Like Kevin Buzzard confronts the difficulty of formalizing simple statements in just the first few weeks he's using lean where he wants to just convince the program that one plus one is two. That is a hard thing to do. Like how would you convince me one plus one is two? It's like, know, it's we all know it's correct but once you actually start to think about how you would, you know, impress someone who's not not it's hard. Terry Tao much later when he is formalizing some of his own work in Lean, he confronts a similarly elementary fact that is just obvious on its surface to mathematicians but convincing Lean it's correct is difficult.

46:21 So the point is there's a there are lots of lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leonardo de Moura's ideas for Lean is it would have these little helper programs called tactics which will automate some of those repeated steps. Those kind of things, steps that happen regularly in proofs instead of having to explain to lean why one plus one is two, you can invoke a certain tactic that just does those type of arithmetic guarantees that kind of proves the qualities, numerical qualities and then you don't have to do it yourself.

46:54 So Leo builds out the capability, he writes some specific tactics that are useful for lean but he also builds out the capability for people in the community, lean users to write their own tactics. That becomes one way in which Lean becomes much more powerful and this pain of writing proofs in Lean starts to diminish.

Checking Peter Scholze's complex paper validates formal verification

47:12 Scholze was the mathematician others turn to when they needed their proofs checked. So in in November 2020, I was contacted by, the Fields Medalist, Peter Scholze. This was back when the library had just basically graduated in some sense. You know, we had sort of it it it knew a lot of undergraduate level mathematics, but not too much else. And Scholze asked me if I'd read I'd carefully read his latest preprint.

47:43 And the answer to this was, well, absolutely. You know, we'd had a study group on it at my university, a London wide study group. There were people from other universities in London. We would meet every week, and we would read another section from this you know, spend two hours reading another section from this paper. And during the term, we'd read the entire we'd read the entire paper. That was the term before Peter got in touch with me. And, so I said, yes. He said, you know, we'd looked at it. Very interesting. You know, congratulations.

48:09 And, he said, did you carefully read the proof of I think it was the theorem 8.4 and, one of the theorems in this paper. So this was a second email from him, you know, asking specifically about checking the details of one of one of the arguments in this paper. So I went back and looked at the paper, which is a big paper, and, and, we had not read the details of this. We'd read the statement of the theorem. Understood We what it was trying to say until, you know, the point of it, where it fitted into the grand scheme of things.

48:40 And the proof was just sort of six pages of technical calculations that we had skimmed through at best. You know? Oh, it's you get the hang of the general idea of what's going on. So we had not read the details at all. So I emailed him back, said, you know, we looked at it. We didn't read the details. And he said, that's what everybody says. And he'd asked people at, you know, at Princeton and at Harvard.

49:05 That's what everybody says. Like, that and, he'd become convinced that nobody had actually read his work. You know, people had skinned over his work. But and, of course, the devil is in the details in mathematics. So he said, at the end of the day, this material is it sort of looks technical, but at the end of the day, a lot of it is undergraduate level material. So maybe it would be possible for your system to check this material.

49:32 And I thought that would be a great test because this is interesting. All we have is is undergraduate level stuff. And all of a sudden, I've got this Fields medalist suggesting that we could check part of his most recent paper. And and I was just, you know, part of at at the time, nobody was taking this software seriously. Maybe people were just beginning to take it seriously. The year before, we'd we'd taken one of his definitions.

49:59 As I said, definitions are much easier than proofs of a hundred page theorems. The year before, we'd taken one of his definitions and taught it to the machine, and we got a certain amount of traction. You know, and and people are beginning to notice, the the software was able to do more complex material. But this is, yeah, this was a complex proof of a complex theorem. It was only it was only six pages long, but the community at that time was small.

50:25 we did wonder we did wonder whether it would be feasible, to, to actually plow through these six pages. And I asked various people, and they were just like, well, could we make this email public? So I asked Peter if he would write a blog post for my blog. I'd started a blog that was sort of promoting the software so Peter wrote a blog post on my blog putting this as a challenge, and then people started popping up in the community saying, actually, I'll be prepared to spend a substantial amount of time doing this.

50:57 And at the time, we imagined it would be about a year's worth of work. But then we started reading. We had to start reading the material, and we had to start reading it. We were really the first people to be reading it possibly, the first people not to skim through it. And, we started going through it with a fine tooth comb, and we found a simplification. Johan Commelin in particular found a simplification. And, six months so that cut the that cut the time down by a factor of two.

51:25 And six months later, we'd we'd checked the key thing that Peter was you know, Peter was worried that the thing was wrong. And Peter's like, no. I think it's right. My co author thinks it's right, Dustin Clausen. No one else has read it. Maybe it's wrong. So six months later, we'd read it through him. He like, it's okay. It's right. The machine says it's right. And Peter got very excited, which is like, okay. So these systems are actually useful because they taught me something about how the proof works. You know, we've we've found a more conceptual argument a part of it, and and something has now actually finally read it.

51:56 So we got excited and wrote a second blog post, which then which then went viral in the community. And the next thing we know, you know, Quanta was on the you know, you know, and and nature was calling me up. And I so at this point, I realized that we had arrived now that, you know, now the sort of the big league people were taking an interest. And and then it sort of, you know, it went on from there. Then, of course, once, you know, once we have some visibility, more and more people start coming into the community, professional mathematicians, saying, well, can we actually do some stuff in my area here?

52:28 Yeah. An expert would come along, and their first question would be like, can we do my latest theorem? And the answer was no, but we can do, you know, the basics in your area, and so here's where to start. And so the library started growing much more quickly then. The the other thing, of course, that happened around that time was COVID. So people were sort of stuck at home, and, playing computer games was sort of an appealing way. You know, playing computer games while simultaneously engaging with interesting mathematics.

52:55 It was some mathematicians found that a very appealing way to spend their time. So there was a sort of a a big sort of jump in the the rate of growth of the library, When you have a mathematical proof in lean fully spelled out you can kind of click into elements of it, investigate and see how different parts of an argument really relate to each other. This ability to interact with the proof is something that lean provides that a static PDF does not.

53:21 And could that same machinery teach an AI to find proofs? so I was recently talking with some mathematicians at a book launch party for Proof in the Code. And kind of late into the evening we start talking about whether you could apply the AlphaZero approach, the zero knowledge approach to like having an LLM recreate mathematics if you just give it kind of the basic axioms. question we were talking about was would an LLM rediscover essentially kind of human mathematics or how far along would it get?

53:48 And there was the kind of the consensus among these three mathematicians I was talking with was that it would not necessarily discover more than the rational numbers. If you were kind of advancing along the kind of the human understanding of math starting at the rational, so almost at the very very beginning they expected computer math would diverge from kind of what has become human discovered math. And I think the reason is like we have this feel for the right abstractions.

54:13 These kind of like satisfying concepts and definitions that feel right to us, that feel complete, that feel expansive in what they can in the kind of the work they can do when you you know when you start applying them in different scenarios. And I think you're right to say that a computer doing this kind of search for things that are just like correct in some strict sense, some concrete sense would not be its search would not be informed by that those same kind of values and I think it would not stumble on the same things that the same mathematical concepts that have ultimately become meaningful to us.

54:43 if you're working on a on a proof say, there are a lot of intermediate phases where you go and look at the whole thing and you're just like, oh, this is wrong, but it felt right. Like, I don't think that's just like a weird artifact of, the reasoning about mathematics process. The idea that it felt right, I think that's probably native to to cognition. So in your book, you you told the story of AlphaProof. So this was back in 2024, and they actually used lean as part of that architecture.

55:10 It's very interesting in context as well because the newer versions don't don't use lean, possibly not yet.

AlphaProof uses reinforcement learning and Lean to solve olympiad problems

55:16 But tell tell us the story of AlphaProof. Very early on, there's this interest in using AI to do mathematics. Can AI solve math problems? It's a it's both kind of just like an obvious like tests because math is, you know, the pinnacle of human thought. If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI because you get a clear reward signal at the end. Has it done the problem correctly or not? That enables reinforcement learning where you can have an AI system solve a problem, receive signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better.

55:52 You need then to identify certain targets in math to set your AI against and early on one of the targets that's established is the International Mathematical Olympiad. It's the premier pre college math competition in the world. These are high school age students doing things that only require high school math. Those are the the problems on the competition but extraordinarily sophisticated versions of those questions. So early on it set out, can AI achieve a gold medal level score on the International Mathematical Olympiad?

56:22 Google DeepMind picks up this quest themselves. In the book, I talk about the 2024 IMO which is where DeepMind designs a system called AlphaProof which is based on the same architecture as AlphaGo from a decade earlier almost. They set it to work on the IMO, they train it to answer competition math level

6 Highlight · Automating translation of competition math into Lean

56:43 problems starting with basic middle school level things, they do reinforcement learning to like slowly reward climb until it is within range of IMO level problems and then they essentially administer the 2024 exam to AlphaProof. They receive the questions after the competitors have finished their work to there's a kind of concern about the machine upstaging the human participants so it receives the questions after the the human competitors complete their work.

57:10 It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal level score and the way in which it it solves the problems is by outputting lean proofs and then using lean to verify them. DeepMind used lean in both the the reinforcement learning stages and then the actual problem solving in the competition stages of for the IMO. AlphaProof could not read the problems it was meant to solve.

57:37 It took statements expressed in lean and devised proofs in lean, but competition problems arrive in natural language. DeepMind needed potentially millions of training problems. Formalizing each one by hand would create an impossible bottleneck. So the team had to find a way to translate competition mathematics into lean automatically. The translation itself had structure.

58:03 Algebra and number theory were easier because their natural language statements already contained equations and notation. DeepMind eventually auto formalized about eighty percent of questions in those areas nearly perfectly. Combinatorics was harder, its questions read like stories, full of natural language and relatively little notation. The mathematics could be discrete and computational,

58:27 yet the human presentation made the formalization difficult. Despite that limitation, DeepMind produced on the order of tens of millions of problems stated in Lean. Only then could AlphaProof's proof search begin. By September 2026, AI systems were tackling open research problems. In epoch AI's fixed budget test, a pre release OpenAI model proved Erdos problem 126 and disproved problem 74 by finding a counterexample.

59:00 Both results were checked in Lean. It resolved two of sixty-eight problems the other four models resolved none and, on September 8, OpenAI also published a claimed

Mapping algebraic laws with automated verification

59:11 resolution of the Navier Stokes Millennium Problem alongside a lean formalization, but unfortunately not under the best circumstances. But that's outside the scope of this particular video. Back in September 2024, Terence Tao launched Equational Theories, an open collaboration mapping which algebraic laws

7 Highlight · Exploring new mathematical spaces with automated collaboration

59:33 imply others, with Lean checking the results. Within a month, the Equational Theories group had narrowed twenty-two million questions down to two hundred and thirty-eight. By late November, they were down to a hundred and thirty-eight. By the end of March, they'd been stuck for several weeks on just four. But settling every implication had never really been the goal.

59:58 Tao viewed equational theories as a pilot project for a fundamentally new way of doing mathematics. And in that regard, it was an unqualified success. He imagined an experimental branch of mathematics, analogous to modern physics, massive collaborations generating huge volumes of data, not replacing theory, but complementing it. The space of algebraic laws was a vast, largely unexplored planet.

1:00:27 Familiar islands such as commutativity and associativity had been thoroughly studied, but most potential laws were unknown. Hidden among them might be structures strange and unlike anything mathematics had seen before, what Tao sometimes calls math from Mars. As the team crossed implications off its immense table, it stumbled onto genuinely new constructions, including magma cohomology.

1:00:56 John Baez, an expert in cohomology who had initially called the project a colossal waste of time, admitted that he had never encountered it. To Tao, that was exactly the point. The project had demonstrated the efficacy of a new kind of mathematical machine. In July 2025, Google DeepMind and

1:01:17 OpenAI reported gold level scores on the International Mathematical Olympiad using natural language proofs. Google's result was officially graded by the IMO, and OpenAI's was separately evaluated. Neither relied on Lean to verify those competition answers. does that in any way negate the need for this kind of verification when we now have proofs that are just written in natural language?

1:01:44 I think it's clearly gonna be elements of both. That lean and reinforcement learning in that environment is gonna create these the engines, is gonna be like essential for model training. I think it's also extremely useful for exploring a wide variety of possible proofs. I mean that's kind of the value of an LLM that it can output millions of potential proofs but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are.

1:02:09 At the same time, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness. So the philosophy of the library has always been find the right abstraction and develop everything in that correct generality.

AI brute force challenges mathematical abstraction

1:02:29 And the advent of AI has been quite interesting because we always firmly believed that finding the right abstraction would just make our lives easier later. And what seems to be happening now is you can have an AI tool which just sees something in a book, doesn't think about it at all, just blindly translates that human written, mathematics into, you know, into Lean, the language, you know, the language that the software uses, and, doesn't really care about making things easy.

1:03:08 If if now it becomes kind of grueling to just kind of bash through this stuff in not really the generality it should be working in, things are much more complicated, and it's as humans, you don't want to plow through stuff when you kind of feel, I should be sailing over this. know, why why is everything so bogged down? Maybe I should think about redesigning. But AI in its current state doesn't really care about redesigning, and it's very happy to just plow through.

1:03:35 So, you know, as as an example, if we did want to change a fundamental definition in the library now, AI would be great at that. AI would just it would fiddle around the roots, you know, break everything, and then it would just plow through and fix everything. And so now we have these new tools, you know, one can now question this fundamental design principle that, you know, do we do we have to find the right level of generality? the math lib maintainers, you know, this this fundamental math library, which everything is building on, we are still absolutely of the the opinion that to get into our library, it needs to be it needs to be, you know, conceptually, the right the right way of doing things.

1:04:17 But there are, of course, plenty of other developments in mathematics now. This wasn't true five years ago. You know, the the largest amount of Lean code in the world was or at least publicly available Lean code was Lean's maths library. And that's probably still just about the case, but, you know, in a year's time, there will be AI developed libraries that will be much more poorly thought out in those terms because somehow trying to make it easy seems to be less of an issue.

1:04:46 If you're prepared to just pour tokens into the problem, then we don't necessarily need to find, you know, the correct conceptual way of thinking about these things. We could just bash something out and formalize a paper that came out last week. Indeed, this is what's happening. You know? Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean and not really thinking about whether this is all done in the correct generality.

1:05:12 So the world is changing, and it's and it's it's not entirely clear it's gonna be better. It's just gonna be different. And do you think LLMs could actually help folks use things like lean? Because if if the problem with lean is just understanding how the lean language works and knowing what primitives to use and and whatnot, could it make that better? It's in two ways. A, right, I mentioned that kind of writing the fiddly lean syntax as a real barrier to entry for mathematicians.

1:05:39 Obviously with like agentic coding, you don't need to like learn all that lean, can just kind of code it the way you would write, you know, JavaScript. there there's an understanding that AI will make writing lean code a lot easier and help probably bring more mathematicians into using the program. There's enthusiasm about that. And then second, I mentioned that you need this library of digital mathematics, mathlib. And all of that is very hand curated material defined very manually.

1:06:05 There's a dream that you could take a full math textbook, show it to an AI and have it automatically translate it, convert it into lean code. This is the the process of auto formalization. There is hope in May 2025 that auto formalization will dramatically accelerate the rate at which new math is added to mathlib. What's been interesting since the book came out, it came out in The States in June of this year, it's going to come out in Europe later this month.

1:06:32 What's been interesting is auto formalization is now happening. You can now give an LLM a math paper and it can spit out the lean code version of it in, you know, a fraction of the time it would have taken a team of humans to do the same thing. The mathlib community actually finds that there is a little bit of a Trojan horse like there's kind of a downside to LLM auto formalization and that is you just end up with this profusion of lean mathematics that are is not always defined with exactly like the precision, the economy with which you want these canonical objects in mathlib to be expressed.

1:07:08 And so they're kind of confronting in a certain way the same challenge that the rest of the world is confronting everywhere which is the volume of AI generated everything. In this case, lean code you might admit to mathlib is not always at the standard the community itself wants and they have to figure out how to kind of sift through

Uncovering hidden errors in published mathematics

1:07:24 all of this new material. So we have a real serious problem now with the spaghetti monster. Right? We are writing code that we no longer understand. We don't understand our code bases anymore. And we need to have some kind of way of building specifications which are computer checkable But a checked proof can still be a proof of the wrong thing. When an AI produces a lean proof of a famous conjecture, someone must still establish that the formal statement captures the intended conjecture with appropriate definitions and assumptions.

1:07:56 The checker certifies the derivation, but it doesn't certify the human choice of target. This is the formalisation gap. The trust has basically moved upstream. Mathematics is a, you know, is a well specified formal language, and that's exactly why that's exactly why we can write computer programs that understand this math you know, that understand what what humans mean when they speak in mathematical terms.

1:08:27 So mathematics should contain no ambiguities at all. So in theory in in theory, mathematics is completely well specified and and thus perfect for this kind of game, you know, writing it down in a formal system using a computer program. But in practice, reading recent mathematical papers, we we do see that there's a certain amount there is a certain amount of people speaking to other experts and just knowing experts sort of know what humans mean when they say things.

1:09:05 So sometimes what ends up on paper is sort of ninety-nine percent, but not a hundred percent representative, of what humans mean by mathematics. And a few years ago, I would not have said that. A few years ago, would have said humans are excellent. Humans are perfect. You know, the the experts, they write down they write down exactly what they mean at all times. But because I've been doing this project of carefully, so I'll tell you a this is a this is a story, that's not been made public yet, but I'll tell you I'll tell you a story.

1:09:37 So we wrote down statements of fifty, fifty theorems from this top pure maths journal, the annals of mathematics. And we're going to make them public this week, but before we made them public, we ran them we ran them through an AI and asked an AI to check them. And the AI found and the AI found

8 Highlight · Discovering false statements in top math papers

1:09:57 errors, and the errors were of two forms. There were errors that my team had made. You know, we'd, we'd failed to correctly translate what it said on the page, into the language of the software. But there were more interesting errors where we had faithfully translated exactly what it said in the paper, but what it said in the paper was just not true because they were just they were just slips.

1:10:22 They were the humans hadn't bothered to mention that, obviously, n had to be at least three or, this set should be nonempty. There there were there were things that that this was Fields medals. Right? We found we found four Fields medalists have actually proved theorems in the annals of mathematics. And if you actually read the statement of the theorem, then strictly speaking, that theorem is not true.

1:10:49 Right? It it's strictly speaking, what they've written is false, and it is obviously not true, in fact. If you're an expert in the area, you would say, well, obviously, they mean this. So the the process of you know, I think this is quite humbling. I think as the as a community, yeah, we should take a look and we we should step back and think, well, actually, you know, we say we've got this precise formal language where we can express exactly what we mean.

1:11:16 But in practice, we're only using it at sort of ninety-nine percent capacity. And one of the things that machines will offer you is the chance to upgrade that to a hundred percent capacity. You know, the machines will say, well, this theorem as you've written it isn't actually true, is it? And then the human will well, obviously not. Always everybody knows that we mean this. But now but why don't we just write that down now? So, you know, this is one of the ways in which the software is making mathematics better. It's getting you from ninety-nine percent to a hundred percent.

1:11:43 You know, humans are not as smart as we think we are.

1:11:46 in the early days of interactive proof assistants, like I said, the argument is that we need these because they're gonna check correctness and get the details right. That got no traction in the mathematics community. Because mathematicians, they push back and they say, look. Mathematics isn't about formalism. It isn't about axioms and rules. It's not about checking the details. It's about the ideas. It's about the understanding. And, you know, you come up with ideas. You know, when you go to formalize or prove it, that that's where the mathematics just is is just just dying.

1:12:12 I mean, it's just you gotta do it. You gotta check. You know, you gotta check carefully. But that's not what we really care about. We care about the ideas. And often, the ideas, they are about coming up with a new representations, ways of thinking about things that will let you solve harder problems and and get further. So, I mean, that said, one of the things that characterizes mathematics is the level of rigor and precision. The fact that, you know, we can come to consensus about whether proof is correct or not, and that's a matter of checking the details and the rules at the bottom.

1:12:42 So, you know, the way I like to think about it is mathematics and that level of precision and rigor, that that's the medium. That's the language, right, in which, you know, mathematicians work. And within that medium, then you have this, you know, you have this platform on which to build these incredibly creative ideas and modes of representation and understandings. So what we really love are the ideas, but they're couched in in this in this framework where we can be very precise.

1:13:08 And I suppose after formalism, what exactly do you know more of?

Applying software engineering principles to math

1:13:13 And and and who knows it? just arguing for formalization in terms of checking correctness didn't get a lot of mathematicians interested. To my surprise, you know, around 2000 after, you know, Kevin Buzzard started blogging and, you know, his blog went viral, a lot of very talented mathematicians came to the subject and got really excited about formalization.

9 Highlight · Treating mathematical concepts like software APIs

1:13:34 And I think what they liked about it was, you know, when you go back to a piece of mathematics that you think you understood, but now you have to represent it formally, you have to represent it in a way that the computer can can understand and check every detail, you find yourself getting very efficient about how you represent concepts and put them together, and especially when you're building a library with lots of moving parts, want them to interact.

1:14:01 You start thinking about them in terms of what computer scientists call the APIs. Right? You know, you have information, and you you encapsulate things, and you expose things, and what, you know, what kind of information you're kind of making public for other people using it, what's the kind of the internals. And so I think mathematicians found it useful to think about mathematics in this kind of software engineering, you know, kind of way of thinking about, okay. You know, what are the different modules? What are the pieces?

1:14:26 How do they interact? What are the the interfaces? I think that they found that this gave them a way of coming back and and understanding, you know, the mathematics in in in new and interesting ways. So it's really just, yeah, exploring the the structure of of mathematics and how the pieces get put together. I mean, we we built up these these these very complex edifices on top of these, you know, kind of very, very precise rules and understanding how you get that level of complexity, you know, down to the the very simple rules at the bottom, is really remarkable.

1:14:57 Alongside concrete tactical discussions about the

1:14:59 projects, Commelin and Scholze debated philosophical aspects of formalization. Commelin saw lean as a better way to work. Scholze did not. These different orientations came through in Commelin and Scholze's Zulip exchanges about what it meant to write definitions in math. How do you know that a definition written in lean is faithful to the definition of an object as mathematicians conventionally understand it?

1:15:30 In many ways, coming up with the right definition for an object is the whole game in mathematics. When mathematicians define new objects or new frameworks and abstractions, they are equipping the field with new tools and perspectives. And Scholze worried that if the definitions were wrong in Lean, nobody could tell. Lean might verify the proof is correct even when it wasn't.

1:15:56 He summed up the conundrum on Zulip. I'm just currently feeling that mathematics remains a human activity. Because if I were to truly check that the computer did the right thing, I would have to unravel the whole proof in my head and check that it really adds up. Lean could verify proofs, but it couldn't check definitions because, logically speaking, definitions aren't right or wrong. They're just what you say they are.

1:16:21 So Commelin and Topaz looked for another form of reassurance. They created a file of concrete examples, unit tests for the most important definitions. If the definitions yielded objects that looked like a duck and quacked like a duck, perhaps they really were defining a duck. The examples were not watertight evidence, but Commelin thought they were at least as reliable as reading definitions in a mathematical paper, perhaps even more so, given how easy it is for mathematicians to see what they expect to see when reviewing one another's work.

1:16:58 And the choice is rarely unique. Concepts that look equivalent on paper can be represented in several formally valid ways.

Preventing reward hacking in AI code generation

1:17:08 A choice that works locally can become brittle or even unrecognizable when a library grows around it. Mathematics has its own integration hell, and every plausible looking contribution creates a review burden for somebody else. I remember there was a bit in Kevin's book where he said at some point, you just kicked a load of people off the Slack channel. You said, look, I just need to I just need to focus now because it's just it was getting ridiculous.

1:17:33 I was trying to build something that works. Some people were there in this, like, channel having fun throwing ideas on the wall. Right? I mean, it's cheap. I mean, you can throw ideas on the wall, and the other side has to keep telling you, no. This doesn't work. Something that's, for me, one frustrating scenario. You throw an idea. You didn't spend five minutes thinking about it.

1:18:00 Then I find a hole. I send back to you. Then you polish a little bit, send back. Now it takes ten minutes to find the hole the next hole. It keeps taking exponentially longer to find the holes on the half-baked idea. For the person coming up with them, it's fun. I mean but it's not fun from your receiver. Right? You have to do your work now.

1:18:26 You spend time telling people why this is not a good idea, why it's not the time you should do it. So we we should come up with a concrete example here. So, apparently, Kim Morrison used the Claude agents to produce a Lean implementation of the compression format zlib and and and prove some specific properties of it. So what exactly did they manage to prove? But the AI managed to translate from C to Lean, the code, then managed to keep fixing the Lean implementation till it passed the test suite that comes with the C version.

1:18:59 And then it proves that for any compression level, for any data, if you compress the data and then decompress, you get the original data back. I liken it to the blind men and the elephant, which is that you have all of these blind men feeling different parts of the elephant. And they they understand parts of the elephant, but they don't understand the whole. And I I don't know whether it's a similar thing with this zlib, whether it actually encompass the whole or just some perspective of it.

1:19:26 But I I suppose the problem when you only have a a perspective of a bigger complex whole, you you get problems in terms

10 Highlight · Reward hacking in automated code verification

1:19:32 of, know, we're talking about reward hacking and, you know, like, Goodhart's law and and all all kinds of, you know, degenerate behavior can happen if you optimize only part of a system. So is is that is that part of the story here? What what was it actually encompassing the whole Zlib algorithm? Yes. Yes. For for example, one way to do reward hacking in this compression decompression. Suppose that's that's what's the only property we ask is the the AI to show, to demonstrate to us that was achieved.

1:20:02 The AI could hack by saying compression, you just return the data. It's the identity function. You just return. Decompression, you return it back. You prove the property. Right? But then you you can put more properties like saying you the outputs should be smaller than inputs. Right? Then you should also tell the AI. You have to show that you compress as much as the Rust implementation in the test suites.

1:20:31 But you're completely right. It's really easy to give properties that do not cover the whole thing. Right? And if you want to do if you see the AI as an assistance to you, that's you're in the loop looking at the codes. I I think this is not super concerning this problem you raised. But if you let once you let the AI go wild and you don't even want to look at the codes, It's really important to cover all aspects.

1:21:05 Right? So otherwise, you can have implementation that satisfies all your properties, but you do not fully specify what you wanted. You're not really getting what you want. there's some skepticism that formal verification is gonna be broadly useful for verifying the correctness of all of this AI generated code precisely for that reason. There's just like no way to write specifications for programs that are operating at the level of complexity as most programs are.

1:21:32 And how do you see this panning out in the future with agentic engineering? So do you think we will come up with some kind of, yes, specifications, systems of constraints, new ways of working, new ways of engineering to essentially solve this divergence problem? I guess you could call it understanding debt, right? There's this problem of building things we no longer understand. We can't verify them. Like, practically, how do you think we can engineer this problem away? the utility of agentic coding is completely bottlenecked right now on this review and verification phase.

1:22:03 I think that AI itself makes software verification kind of much more powerful because you can use AI to write these specifications themselves. They don't have to be written by hand. Basically, I I think kind of formal verification of software programs will like increasingly have a role to play in the new AI powered software development life cycle. there are places like Harmonic which believe that if you can train an AI model to write math proofs, that same intelligence will be useful for writing proofs about software for verifying the the output of of LLMs.

1:22:35 So I don't know. That that kind of bet is underway. Whether or not it pans out, I don't know. So underneath all of this software was a very human story of fracturous relationships, of innovation,

Navigating grief and excitement in mathematical AI

1:22:49 of incredible persistence. And it has led to something which has just revolutionized the world of mathematics and is continuing to do so on a daily basis. So AI is coming for mathematics. This is absolutely clear. And what it's gonna do to it, nobody really knows. All that we know is it's getting really good really quickly, and no one has any understanding of how much better it's gonna get.

1:23:17 So mathematicians have had various different reactions to this ranging from, you know, what could only be described as grief, that that the subject is changing and and that they're gonna have to adapt or or die. So ranging from grief to excitement, and I'm very much excitement end of the scale, I think mathematics is gonna be hugely accelerated by this software because, remember, it's already doing interesting things.

1:23:47 And the thing you have to remember is it's it's it's worst. You know, today is the worst it will be. Right? Going forward, it's gonna be much better. It's already awesome, and it's much worse than what it will be this time next year. So I think AI opens up huge new possibilities for mathematics. It will change many things about it, but at the end of the day, we're gonna end up with more understanding. We're gonna end up with more theorems proved, and we're gonna end up, you know, with just a better overview of what mathematics is and and and great tools where we can explore new dark corners and enlighten them and enlighten our community.

1:24:28 So going forward, things look very exciting. what what makes our goals special is that they're ours. They are goals. I mean, you and I are having this conversation. Right? And the conversation is what should we do? What should we make of AI, and how should we respond to AI? What should we do with AI? Right? We're having this converse I mean, I'm happy to let AI have its discussion on the side about what what its goals are and what it should be trying to do. Right? That doesn't interest me. Right? I mean, you tell me that there's some server in the corner, and it's doing whatever it's doing and proving theorems and so on.

1:24:58 You know, again, what I care about is how how am I gonna interact with it? So, yeah, it's not that I don't know. It's, again, the questions I think that we should be interested in are what are our goals, and what should we be doing to achieve them? I don't know. So, I mean, it's anthropocentrism only in that. That's what we are. Right? So, yeah, I I think we should be at the center of the debate just because we're the ones having the debate.

1:25:27 And so if it's our and so far as it's our debate, we we can't help it make it about help but make it about what, you know, what we want. Once I started writing the book, spent a lot of time with Leonardo de Moura and

The interpersonal dynamics of the Lean community

1:25:40 that was actually kind of the first moment in which I understood in a certain way the significance of what I was doing. Not like for the world, but just like as a kind of an ethical contract almost between me and the sources which is this was Leo's life work and he cared a tremendous amount about it. And my book was likely to be the only kind of start to finish story of the development of lean and just started to feel extremely important to tell the story well. And I was contacted by a guy called Kevin Hartnett, who at the time worked for Quanta magazine and wanted to run a piece on on Lean's Lean and its mathematics library, for Quanta.

1:26:15 So I I ran into Kevin around then, and, you know, we became friends. And and he interviewed me several times about several things, and then later on decided that this was such an interesting story that it was sort of worth writing a book on. You know, a decision which I thought was quite an interesting one, but he he went for it. And during that time, he interviewed me many more times and tried to get some kind of idea as to sort of how it happened.

1:26:48 You you know, he wanted to put together, you know, the people behind the story and what was going on. And so my midlife crisis, where I started worrying about human generated mathematics and asking whether machines could do it better somehow played a role in Kevin's in the story that Kevin decided to tell. As I met more and more figures in the book, more mathematicians, I similarly understood how important it was to them. I spent a lot of time with the six or seven key core sources for the book.

1:27:17 It was also very useful to me that this group of people left a tremendous digital record of all of their work. They were initially very active over email and they shared a large number of their private emails with me. They also then later migrated to this chat platform called Zulip where they conducted a lot of their work in these public threads and then also in private DMs which they shared with me. And so I was able to kind of reconstruct a lot of the work as if I was like there observing it and in the moment it was taking place.

1:27:49 So that was like a tremendous benefit to writing the book. Obviously, Kevin, when he was writing the book, I think you gave you gave him access to those emails. Were there any interesting bits that Kevin left out? you know, you don't wanna air your dirty laundry, you know, in in public. I mean, the the thing about the people working on Lean, it's just a wonder it's like family. You know? It's just a wonderful community of of good friends, and everybody working on the project was kind of young and idealistic and excited about it.

1:28:16 And, you know, we all felt that we were doing something interesting and important. But, you know, like a lot of things with family, sometimes family drives you crazy. You know, you get to the family get together, and there's the crazy ah, and they're all the and so, you know, initially when Kevin interviewed us you know, there were there were the bumpy spots along the way, and there were the you know, there were these tensions.

1:28:41 And but we don't wanna dwell on them. Right? And so an outside reporter, you know, journalist comes in. And so we were very guarded at first. But I think we we came to trust Kevin when it really became clear that he wasn't looking for, you know, good guys and bad guys or an expose or a scandal story or anything like that, that he was really trying to tell us tell the story in a way that was respectful to everyone involved. So when that when that was the case, I think I mean, he really spoke to a lot of people, And I think he really did a good job of capturing the feel and the excitement of of working on the project.

1:29:14 And and when there were tensions involved, sort of, you know, making them making it come across it. Again, it wasn't a matter of good guys and bad guys, but just people looking for different things. there was this experience I had reporting it where for a period around 2018 Leo goes off and builds lean four and simultaneously all the math activity and mathlib is still continuing apace and it just never felt like kind of like I understood what was going on in those years.

1:29:41 It was very not clear to me if Leo was talking to the mathematicians or not. It was kind of a situation where someone has told you a story, it doesn't quite make sense to you but you don't know why. Ultimately what I learned is there had been a somewhat decisive fracture between Leo and the math community where he says, I'm gonna go off on my own and build lean lean four. Please leave me alone in so many words. And they kind of they kind of actually they get the message. They're a little wary of like angering this guy who they admire and it's so it's so important to them.

1:30:11 There's some particular personality conflicts that I talked about in the book between Leo and this guy Mario Carneiro who both are just have strong visions for what they want this kind of emerging world to look like. Mario's vision is what he wants mathlib to look like. He's very much a big open source believer. Leo's vision is for like lean. The two of them clash quite a lot and in certain ways kind of that friction pushes Leo away from the mathematicians in this way, in this 2018 to 2022 period.

1:30:39 Anyway, what was interesting for me though was realizing I've been like hearing this story, it didn't quite make sense to me, I didn't quite know why, and then almost in like in a rush, the various figures, the sources I was working with kind of said, oh, this in fact is what's going on. Leo was mad and kind of had left left the sphere for a little while. And of course once once you get one person to to explain their side of the story, others are kind of more forthcoming about theirs as well. So I think that's how I felt like by the end, I had understood at least kind of interpersonally fully what was going on with Lean.

1:31:10 So so so if if you read the book, there was a a period where Leo was just kind of frustrated with with well, really all users, but especially the mathematical users. And while he was working on Lean 4, he kind of pulled off and, you know, he kind of needed his distance. And, you know, every once in while, I'd send him an email and get a quick response, but it was clear that he he wanted some distance. And that was hard. You know, I I missed him because he's he's a very good friend, and and I I missed just kind of constantly being able to bounce off ideas and so on.

1:31:43 And so I I contact him. So I was in, as the book explains, I was coming to Seattle for the joint mathematics, the big American you know, big US math meeting every year. And so so Leo arranged the dinner. It was, other people were in town for the conference. He decided to take the opportunity to bring together advisers for the Lean Focused Research. So it wasn't it wasn't a birthday dinner. It was it was really just bringing together people, you know, interested in Lean and and, supporting Lean.

1:32:12 But I told him that my birthday was that week, and he decided to make it coincide with my birthday. I really was looking forward to it. Was not that dinner, but the next day. He just took an afternoon off from work. I took an afternoon off from the conference. And and we just met at Pike's place, and we just kinda just walked and just walked and walked. And, yeah, it was it was just it was just it was great talking to him again.

1:32:41 Yeah. We we talked about Lean, but we talked about things that were not Lean. Yeah. I mean, for both of us, it's been I mean, the last several years has been surreal. I mean, we we just remember the early days of Lean, you know. Yeah. Again, I can remember when it was just me and some students, and I remember my time visiting Leo at Microsoft and working on the project. And so looking looking back on all that, it it almost seems surreal. I mean, it it seems very surreal, you know, how far we've come.

1:33:06 Now, Kevin Hartner really brought this story to life. He spent, I think, years researching this story, speaking of all of these guys. So I highly recommend you read Kevin's book. And until the next time, cheers.