数学は永遠に変わった — Kevin Hartnett『The Proof in the Code』とLeanの物語

The Fields Medalist, Peter Schultz, proof was just sort of six pages of technical calculations that we had skimmed through at Vess. 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 haven'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 a certificate, you have an algorithm, then you can check whether the proof is correct so much. The machine says it's right, and something has now actually finally read it. AI is coming from mathematics, this is absolutely clear. Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean. And 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. But I'm interested in understanding it. Right, and I'm still the one who has to understand it. And it can output, you know, 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. 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, and I'm just going to check it. 400 years ago when johannes kepler was in a green grocer he had an interesting idea 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. Now, two mathematicians, Thomas Hales and Samuel Ferguson, they reduced it to 1,762 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 pyramid placement. Kevin Hartnett tells this story in his brand new book proof in the code now um the book isn't just about oranges and kepler's conjecture but that's

certainly where it starts but um the the thrust of the book is mostly about this gentleman called leo demora 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 and he was saying how this guy Thomas Hells 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 0.74 and it took him many many many years to do this and eventually he did it so he had 1767 computer programs for every single configuration of these balls and he was elated 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 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. Because if you think about it, for 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. With Kevin's permission, I'm going to read out a few bits from his book, just to give you folks a little flavour 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. 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. Why would he court 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 99% confident this proof is correct. But then Tom started using proof assistance. This all happened before Lean. He used Hall Light and Isabel to do this work,

but it was a milestone. I mean, it was a big result that has been formalized in proof assistance. And Tom was famous twice for solving the Kepler conjecture and for using a proof assistance, right, in a paper that the math community cared. And the fact that he decided to do the next project using Lean was a big deal on me. 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? It's very much a social process. 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, you know, they can check a proof.

They can check the kind of the lines and 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. Yeah, I mean, I suppose like a fundamental noob question is, why does it matter that we can prove something versus just know something is true? Well, I think the main thing is that we can, when you prove something using a tool like Lean, you can get a certificate, you have an algorithm, then can check whether the proof is correct or not. For math, for example, this is useful for trust, and you can collaborate with people you never have met. 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 project I don't need to check if their proofs are correct or not A big math project You can view as engineering projects

I mean, Johan Kormelin, for example He's a really hardcore mathematician and he is 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, he's like the architect of 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 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 this is valuable earlier this year in melbourne i caught up with our favorite 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 want to talk about symbolic ai the thing that's interesting is i don't want merely things

that don't get it wrong because that's still not enough. I want to know why it comes up with a particular answer. I want new 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, right? 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? And 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. So Hales' proof was not like that. 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 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. 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 20 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. 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 ratio called the De Bruyne ratio, 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, 20 to 1, often higher. Mathematicians don't generally see the reason to invest that additional time just to verify the correctness of something. 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 CyberFund. If you're building at the frontier of AI, they want to hear from you.

CyberFund 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. It's an environment of pure focus and rapid execution for founders operating at AI native speed. And they're offering teams $2 million each to participate. Apply now at cyber.fund. Folks new to Lean, what is it all about? What can you do with Lean? Lean is both a programming language and a proof assistant. You can write calls. 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 the Lean Math Lib 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 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? The kernel is how. We have the notion of a small trust as kernel. Now, Lee's massive has zillions of bugs, right? But to trust our results in Lee, only to 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. 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 Isabel had all contained bugs in their kernels that allowed users to validate false statements. His answer was independent checking. let users build their own kernels. To make this option realistic, DeMora 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, DeMora admired the minimality of HOL Lite, which had a very small kernel. 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 the style of a mathematical proof. Like he could kind of prove with Z3 where 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 one particular direction. Leo built Z3 as a way to automatically check different pathways through Microsoft software for bugs, prove, guarantee that there were no bugs. Now 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 2000s. And 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. 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. 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 want to 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. There's kind of just a wider range of truths you can try to encode and verify,

and interactive in the sense that kind of a human user can nudge the program towards greater expressiveness. It makes it a much more powerful thing. What my book is, is ultimately the story of how Lean, this interactive theorem prover that Jamura 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, NITP breaks through into a more mainstream way of working at 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. Jeremy Abagad, a mathematician and philosopher at Carnegie Mellon, has been corresponding with Leo for many years. 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 is this and started just kind of 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, Demora sent a long email to the group, softening some of the concerns he had raised. 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 Lite's design and implementation. In my opinion, it's the most elegant by far. He acknowledged that this perspective was at odds with Avogad's. I understand Jeremy's point when he says H.O.L. light would be really inconvenient for doing abstract algebra. The design of Lean was being negotiated in real time.

I want to use Herada Logic. It's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough, right? But for doing abstract mathematics, it's not. It's important to have a good library, a math library. For verifying software, for example, cryptography, we need lots of math. Differential privacy is another example. Having a good mathematical library is important, even if you only care about software verification. And 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, Cedric Forney. He uses LeanMail.

And he told me, look, that Mathlib, the Lima Mathematical Library, have the right abstractions I need for refined cryptography. Because of all the generality that having the penance type theory provided, we have a library that's more expressive, that has the right abstractions, it's cleaner. Yeah, it paid off long term, it paid off. was a lot of extra work at the beginning. And to get it right was also a lot of work. But I think it paid off. I suppose one of the biggest tensions, and ultimately 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. I spent a sabbatical year working on the formalization, in the Fite-Thompson theorem, and that is in a proof assistant known as Ruck, and Ruck is based

on dependent type theory. Before that, I had worked with Isabel extensively, which is a proof assistant based on a simpler logical framework called simple type theory. Isabel is a wonderful system, and so for many things, it's absolutely ideal. It still, to this day, has excellent automation, automated support. So for certain types of mathematics, 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. They're really ubiquitous. There are these complex networks of algebraic structures. And simple type theory is just not good for that. And so after my year working with Ruck, It became clear to me that this was the framework that was capable of doing that type of mathematics. And I think other mathematicians who had experimented with Isabel 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 from the Spider-Man franchise, you know, with great power comes great responsibility. You know, the very powerful language is 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 foundation And so he needed convincing there that the tradeoff was worth it I think you know in the end he came around I mean, now he's one of the biggest proponents of dependent type theory. He, you know, you know, soon after he would say that, you know, it's really beautiful. And so he recognized the benefits. But again, coming from the outside and, you know, without the familiarity, 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 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. It's funny, as a developer, when you're using the developer hat, usually you want to go to whatever it's simplest to implement, and you forget that you sometimes will be the user of this tool too. I always joke, I mean, 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, there's 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. I mean, he just thinks it's terrible. 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 in 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. 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. 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 becomes 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. There ultimately are four versions of Lean. We're currently on Lean 4, but for years, you know, we were at Lean 2. And Leo saw where he wanted it to go and he felt inhibited in his ability to actually 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 Kevin Buzzard. My name's 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 realised that there was a huge amount of material that I was going to have to sort of catch up on. 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 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 to check mathematics using machines? 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 that it could check mathematics at superhuman accuracy and it absolutely could check mathematics at superhuman accuracy but the problem was the mathematics, 99% of what it was checking was really, really basic material known hundreds or maybe even thousands of years ago but by that stage I kind of got hooked

because I realised that there was this weird new way of doing mathematics I'd never really seen anything like it before and I started to realise 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 then I was just like, oh this software is really great 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 that was how I ended up switching by 2016 Kevin Buzzard had time to return to the Piadic Landlands program, a young talent named Peter Schultze had transformed the geometry of numbers with perfectoid spaces and Buzzard wanted to be part of the revolution, but as he read the papers that followed Schultze'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 his critique was not of Schultze'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. 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 Matholib. Lean then checks the proof, and it says no goals, which means the task is complete. When you boot up Lean, Lean does not know any mathematics. It's equipped with basic axioms and rules for math, so it has some kind of just like some understanding of mathematical logic. So what 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.

People like Kevin Buzzard, Johan Kamalin, Patrick Masso, Jeremy Avogad is very involved. Mario Carnero 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. That's how Lean breaks beyond 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 interested in this story back in 2020 when I was assigned an article for Quantum Magazine on the development of Mathlib when it was still quite early days. In that article, I said that Mathlib had the spirit of a barn raising. It was just like this 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 Leans mathematics library. So it was born about the same time that I started working in the field. It was 30,000 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. It didn't even have a definition of the real numbers when I started. or it just got this concept of the real numbers, which is something known to the ancient Greeks and the Babylonians, you know. There's thousands of years old. And it didn't have the complex numbers, which I guess from about 500 years ago. So there was clearly a lot of work needed doing. You know, I spend a lot of time teaching, right? That's part of my job. 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 going to 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 this basic number system that goes back to Descartes. So I kind of thought, oh, this thing doesn't have the complex numbers. Let's teach it the complex numbers. 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 for this maths library and then it got merged into the main branch and suddenly we've got complex numbers, copyright 2017 Kevin Buzzard and I'm just thinking great, now what's the next thing that we teach them because now I'm thinking what do we actually teach our undergraduates what's missing 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 in 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 like one evening a week i'd stay late at work and just let the kids muddle on by themselves and uh 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 was treating this thing as an undergraduate at the time 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 that 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

now and yeah that was sort of when I fell in love with it you know because I wanted to teach it. But when is a new mathematical idea ready to become part of the library? Mathematics is an interesting object. It's this gigantic abstract object that humans have created. And at the boundary, there are things that haven't, you know, they're not quite fully formed. There are ideas which sort of work or work in some cases. And we need to think about how these ideas should mature, what they should really look like. So mathematics needs to mature. Sometimes at the boundary, it's not material that's ideal for the library. What we want in the library is ideas which are really well understood and exist in the correct generality. We want polished mathematics, stuff which is still a bit chaotic. One can attempt to teach it to the machine. 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, beautiful conceptual ideas which sort of know their place. Essentially, all of the library now 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 when you want to commit. 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 generalised and simplified a bit and then somehow you need to rework the entire thing. We try and avoid this. We like to get things right first time. Occasionally we have had to go through and change a fundamental definition. This can be a huge amount of work because then many thousands of files then break and need to 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 Grothendijk in the mid 20th 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 type of frontier math that they themselves care about. He does it and he's met with a collective yawn because people tell him, Kevin, schemes are old math, right? 60, 80 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 Schultze, who is today and then as well considered maybe the greatest living mathematician.

Perfectoid spaces are truly state-of-the-art objects in math. And Kevin says, all right, if we can formalize them, if we can show Lean is capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything. And so he and Masso and Comlin 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. So it's essentially a punch list, like a construction project. You know, we would need to define this and this and this and this, and ultimately we'd get perfectoid spaces. And they succeed at that. And what that, I think, kind of 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. They have 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 going to build this narrow skyscraper to the frontier. Perfectoid spaces is the first example of that. That stunt works the way Buzzard hopes it will work. 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, so back in 2017 I was having this midlife crisis and trying to work out what was going on in the area of 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 this was at the Newton Institute in Cambridge and they were ahead of the game this was pre-COVID but they were already recording and live streaming their talks on the internet 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 Tom Hales and I imagined that he would be talking about his proof of the Kepler injecture but in fact that only formed a very small part of his talk, he was talking about exactly the thing that I've become worried about. He was talking about formalising modern mathematics, perhaps all of modern mathematics. And one of the things he suggested was that perhaps it was time to be 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've 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 100 pages long, 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 reality, You would imagine that maths was this sort of perfect language where everything can be expressed, you know, in a completely unambiguous way. But in practice, this is not what happens. In practice, you read section 3 of the paper, and section 3, it says, from this point, P will be a prime number, which is at least 5. 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 fact that P is at least 5, it was sort of slipped in to section 3. 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 trying to translate all the I was two weeks in and I'd realised that the systems knew nothing but somehow the idea of teaching the systems basic mathematical definitions seemed to be much more viable than teaching it 100 page long proofs of theorems because many mathematical definitions are quite short in fact that was what the library looked like in 2017 It contained some definitions that undergraduates find quite difficult. Second year and third year, fancy things like topological spaces and Notherian 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. And this just seemed to me like a viable way to move forward. whilst engaging with interesting material. So it was just a completely... My idea was just like, let's check these modern papers remarked that's completely impossible. Whereas Hales' idea was viable. In fact, it was somehow not quite viable at that moment. Hales pushed for it to be happening in 2017 and it was somehow too difficult to do in 2017. 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 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 and we're trying to translate just the statements of the theorems into the language of the software and yeah, we're 20% through. 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 going to be far more than 20% through. So Hales had these ideas which have taken years to become real, but now they are becoming... I would say that Hales was really this was a visionary talk and now his vision is coming to fruition. Formalizing a proof or writing math in this formal language 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, write, 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 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 you know it's we all know it's correct but once you actually start to think about how you would uh impress someone who's 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 it's just obvious on its surface to mathematicians, but convincing Lean it's correct is difficult. So, the point is, there are lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora'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 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 equalities numerical equalities, and then you don't have to do it yourself. 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. Schultzer was the mathematician others turned to when they needed their proofs checked. So in November 2020, I was contacted by the Fields medalist, Peter Schultzer. This was back when the library had just basically graduated in some sense. We had sort of, it knew a lot of undergraduate level mathematics, but not too much else. and Schultz asked me if I'd read, I'd carefully read his latest pre-print

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 paper, that was the term before Peter got in touch with me and so I said yes he said we looked at it, very interesting, congratulations and he said did you carefully read the proof of, I think it was theorem 8.4 and one of the theorems in this paper so this was a second email from him asking specifically about checking the details of one of the arguments in this paper so I went back and looked at the paper, which is a big paper and we had not read the details of this, we had read the statement to the theorem. We'd understood what it was trying to say and so, you know, the point of it, where it fitted into the grand scheme of things. And the proof was just sort of six pages of technical

calculations that we had skimmed through at best. You know, you get the hang of the general idea of what's going on. So we had not read the details at all. So we 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 ask people at Princeton and at Harvard. That's what everybody says. And he'd become convinced that nobody had actually read his work. People had skinned over his work. And of course, the devil is in the details in mathematics. So he said, at the end of the day, this material, 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 and I thought that would be a great test because this is interesting all we have is undergraduate level stuff and all of a sudden I've got this Phil's medalist suggesting that we could check part of his most recent paper

and I was just part of at the time nobody was taking this software seriously maybe people were just beginning to take it seriously The year before, we'd taken one of his definitions. Definitions are much easier than proofs of 100-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. People are beginning to notice that the software was able to do more complex material. But this was a complex proof of a complex theorem. It was only six pages long. But the community at that time was small. So we did wonder whether it would be feasible to actually plough 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'd be prepared to spend a substantial amount of time doing this. 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 Komelen in particular found a simplification. and so that cut the time down by a factor of two and six months later we'd checked the key thing that Peter was you know Peter was worried that the thing was wrong and Peter's like 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 and it was 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 found a more conceptual argument a part of it and something has now actually finally read it. So we got excited and wrote a second blog post, which then went viral in the community. And the next thing we know, you know, Qanta was on the, you know, and Nature was calling me up. And so at this point I realised that we'd arrived. Now the, you know, now the sort of the big league people were taking an interest. and then it sort of went on from there. Then of course 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? 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 the basics in your area and so here's where to start. So the library started growing much more quickly then. 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 playing computer games

while simultaneously engaging with interesting mathematics some mathematicians found that a very appealing way to spend their time so there was a sort of a big sort of jump in 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. 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 the proof and the code, and kind of late into the evening, we start talking about whether you could apply the alpha zero approach, the zero-knowledge approach to having an LLM recreate mathematics if you just give it kind of the basic axioms. The question we were talking about was, would an LLM rediscover essentially kind of human mathematics or how far along would it get? And there was 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 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, 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 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 those same kind of values and I think it would not stumble on the same things, the same mathematical concepts that have ultimately become meaningful to us. If you're working 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 like 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 alpha proof so this is back in 2024 and they actually used lean as part of that architecture and it's very interesting in context as well because the newer versions don't don't use lean possibly not yet but tell us the story of alpha proof very early on there's interest in using AI to do mathematics. Can AI solve math problems? It's both kind of just being an obvious like tests because math is 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, receives signal, did it do it correctly or not, do that very quickly, iterate a lot, get a lot better. 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 Math 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 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 Math Olympiad? Google DeepMind picks up this quest themselves. In the book, I talk about the 2024 IMO, which is where Google 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 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.

It receives the questions after the competitors have finished their work. There's a kind of concern about the machine upstaging the human participants. So it receives the questions after the human competitors complete their work. 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 solves the problems is by outputting Lean proofs and then using Lean to verify them. DeepMind used Lean in both the reinforcement learning stages and then the actual problem solving in the competition stages for the IMO. Alpha proof could not read the problems it was meant to solve. 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. algebra and number theory were easier because their natural language statements already contained equations and notation deep mind eventually auto formalized about 80 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 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. Both results were checked in Lean.

It resolved two of 68 problems. The other four models resolved none. And on September the 8th, OpenAI also published a claimed 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 imply others, with Lean checking the results. Within a month, the Equational Theories group had narrowed 22 million questions down to 238. by late November they were down to 138 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 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. 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 John Bays, 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 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 i think it's clearly going to be elements of both that lean and reinforcement learning in that environment is going to create these the engines is going to 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 you know 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. 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. 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 Lean, the language that the software uses, and doesn't really care about making things easy.

If now it becomes kind of gruelling to just kind of bash through this stuff in not really the generality it should be working in. Things are much more complicated, and as humans, you don't want to plough through stuff when you kind of, I should be sailing over this. you know 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 plough through so you know 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 change it would fiddle around at the roots you know break everything and then it would just plough through and fix everything and so now we have these new tools one can now question this fundamental design principle do we have to find the right level of generality the mathlib maintainers this fundamental math library which everything is building on we are still absolutely of the opinion that to get into our library

it needs to be conceptually the right way of doing things but there are of course plenty of other developments of mathematics now. This wasn't true five years ago. You know, 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 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. If you're prepared to just pour tokens into the problem, then we don't necessarily need to find the correct conceptual way of thinking about these things. We could just bash something out and formalise a paper that came out last week. Indeed this is what's happening. 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.

So the world is changing and it's not entirely clear it's going to be better. It's just going to be different. And do you think LLMs could actually help folks use things like Lean? Because if the problem with Lean is just understanding how the Lean language works and knowing what primitives to use and whatnot, could it make that better? It's in two ways. A, I mentioned that writing the fiddly Lean syntax is a real barrier to entry for mathematicians. Obviously, with agentic coding, you don't need to learn all that Lean. You can just kind of code it the way you would write JavaScript. There's an understanding that AI will make writing lean code a lot easier and probably bring more mathematicians into using the program. There's enthusiasm of 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. 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 process of auto-formalization. There is hope in May of 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. 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 a fraction of the time. It would have taken a team of humans to do the same thing. The math lab 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 is not always defined with exactly like the precision, the economy with which you want these canonical objects in MathLib to be expressed. 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 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. The checker certifies the derivation, but it doesn't certify the human choice of target. This is the formalization gap. The trust has basically moved upstream. Mathematics is a well-specified formal language, and that's exactly why we can write computer

programs that understand what humans mean when they speak in mathematical terms. So mathematics should contain no ambiguities at all. So in theory, mathematics is completely well-specified and thus perfect for this kind of game, writing it down in a formal system using a computer program. But in practice, reading recent mathematical papers, 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. so sometimes what ends up on paper is sort of 99% but not 100% representative of what humans mean by mathematics and a few years ago I would not have said that, a few years ago I would have said

humans are excellent, humans are perfect the experts, they write down they write down exactly what they mean at all times because I've been doing this project of carefully so I'll tell you a story this is a story that's not been made public yet, but I'll tell you a story. So we wrote down statements of 50 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 through an AI and asked an AI to check them. And the AI found errors. And the errors were of two forms. There were errors that my team had made. We 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 there were just slips. The humans hadn't bothered to mention that obviously N had to be at least three, or obviously this set should be non-empty. There were things that... And this was Fields' medals, right? 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, right? Strictly speaking, what they've written is false. And it's obviously not true, in fact. If you're an expert in the area, you would say, well, obviously they mean this. so the process of, you know, I think this is quite humbling I think as a community you know, we should take a look and we should step back and think well actually, you know, we say we've got this precise form of language where we can express exactly what we mean but in practice, we're only using if it's sort of 99% capacity and one of the things that machines

will offer you is the chance to upgrade that to 100% capacity you know, the machines will say, well this thing as you've written it isn't actually true, is it? And then the human will be, well, obviously not. 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 99% to 100%. You know, humans are not as smart as we think we are. In the early days of interactive proof assistance, like I said, the arguments that we need these because they're going to check correctness and get the details right, they got no traction in the mathematics community. Because mathematicians, they'd push back and just 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 a proof, that's where the mathematics is just dying. I mean, it's just, you got to do it, you got to check, you know, you got to 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 get further. So, I mean, that said, one of the things that characterizes mathematics is the level of rigor and precision and 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. So, you know, the way I like to think about it is mathematics and that level of precision and rigor, that's the medium. That's the language in which mathematicians work. And within that medium, then 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 this framework where we can be very precise. I suppose after formalism, what exactly do you know more of 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. 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 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, you want them to interact. You start thinking about them in terms of what computer scientists call the APIs, right? You know, you have information and you encapsulate things and you expose things. And 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? How do they interact? What are the interfaces? I think that they found that this gave them a way of coming back and understanding, you know, the mathematics in new and interesting ways. So it's really just, yeah, exploring the structure of mathematics and how the pieces get put together. I mean, we build up these very complex edifices on top of these kind of very, very precise rules. And understanding how you get that level of complexity down to the very simple rules at the bottom is really remarkable. Alongside concrete tactical discussions about the project, Komelin and Schultze debated philosophical aspects of formalization. Komelin saw Lean as a better way to work. Schultze did not. These different orientations came through in Komelin and Schultz'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? 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 Schultze worried that if the definitions were wrong in Lean nobody could tell Lean might verify the proof is correct even when it wasn't 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. So Komelin 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 Comelin 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. And the choice is really unique. Concepts that look equivalent on paper can be represented in several formally valid ways. A choice that works locally can become brittle or even unrecognizable when a library grows around it. Mathematics has its own integration held, 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. and he said, look, I just need to focus there

because it was getting ridiculous. I was trying to build something that works. Some people were there in the Slack 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 your noise. It doesn't work. Something that's, for me, one frustrating scenario. You throw an idea. You didn't spend five minutes Thinking about it Then I find a hole I send it back to you Then you polish a little bit Send it 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-baker idea For the person coming up with them It's fun, I think But it's not fun From your receiver Right? You have to do your work now you spend time telling people why this is not a good idea, why it's not the time to do it. So we should come up with a concrete example here.

So apparently, Kim Morrison used a Claude agent to produce a Lean implementation of the compression format Zlib and proved 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 to each passage that has suite that comes with the C version. 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 understand parts of the elephant, but they don't understand the whole. And I don't know whether it's a similar thing with this Zedlib, whether it actually encompassed the whole or just some perspective of it. But I suppose the problem, when you only have a perspective of a bigger complex whole, you get problems in terms of, you know, we're talking about reward hacking

and, you know, like Goodhart's law and all kinds of degenerate behavior can happen if you optimize only part of a system. So is that part of the story here? Was it actually encompassing the whole Zlib algorithm? Yes, yes. For example, one way to do reward hacking is compression to compression. suppose that was the only property we asked the AI to show to demonstrate to us that was achieved 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 can put more properties like saying the output 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 suite. 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 in the loop looking at the code, I think it's not super concerning, this problem you raised, but if you want to let the AI go wild and you don't even want to look at the code, it's really important to cover all aspects, right? 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 going to be broadly useful for verifying the correctness of all of this AI-generated code precisely for that reason. There's just no way to write specifications for programs that are operating at the level of complexity as most programs are. 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, yeah, 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 we're 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. 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. I think kind of formal verification of software programs will increasingly have a role to play in the new AI-powered software development lifecycle. 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 output of LLMs. So I don't know, 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, 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 from mathematics, this is absolutely clear. And what it's going to 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 going to get. So mathematicians have had various different reactions to this, ranging from, you know, what could only be described as grief, that the subject is changing and that they're going to have to adapt or die. So ranging from grief to excitement, and I'm very much at the excitement end of the scale, I think mathematics is going to be hugely accelerated by this software because, remember, it's already doing interesting things and the thing you have to remember is it's worth, you know, Today is the worst it will be, right? Going forward, it's going to be much better.

It is 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 going to end up with more understanding, we're going to end up with more theorems proved, and we're going to end up with just a better overview of what mathematics is, and great tools where we can explore new dark corners and enlighten them and enlighten our community. So going forward, things look very exciting. What makes our goals special is that they're ours. They're our 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? We're having this conversation. I mean, I'm happy to let AI have its discussion on the side about 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.

You know, again, what I care about is how am I going to 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? Um, so, I mean, it's anthropocentrism only in that that's what we are, right? Um, so, yeah, I think we should be at the center of the debate just because we're the ones that are having the debate. If it's hard, so far as it's our debate, 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, I spent a lot of time with Leo DeMora, and 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 Quantum Magazine, and wanted to run a piece on Lean and its mathematics library for quanta. So I ran into Kevin around then and, you know, we became friends. 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 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. He wanted to put together 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 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. 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 in the moment it was taking place. So that was like a tremendous benefit to writing the book. Obviously, Kevin, when he was writing the book, I think you gave him access to those emails. Were there any interesting bits that Kevin left out? You know, you don't want to air your dirty laundry, you know, in public.

I mean, the thing about people working on Lean, it's just a wonderful, it's like family. You know, it's just a wonderful community of good friends. And everybody working on the project was kind of young and idealistic and excited about it. 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 eye, and there are all the – and so, you know, initially when Kevin interviewed us, you know, there were the bumpy spots along the way, and there were the – you know, there were these tensions. But we don't want to 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 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 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 working on the project. and when there were tensions involved, sort of making it come across. 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 4 and simultaneously all the math activity and math lib is still continuing at pace. And it just never felt like I understood what was going on in those years. 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 going to go off on my own and build Lean 4. Please leave me alone, in so many words. And they kind of actually get the message. They're a little wary of angering this guy who they admire

and is so important to them. There are some particular personality conflicts that I talk about in the book between Leo and this guy, Mario Carnero, who both 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 Lean. The two of them clash quite a lot. And in certain ways, that friction pushes Leo away from the mathematicians in this way in this 2018 to 2022 period. Anyway, what was interesting for me, though, was realizing I'd 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 source that I was working with, kind of said, oh, this, in fact, is what's going on. Leo was mad and kind of had left this sphere for a little while. And, of course, once you get one person 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.

So if you read the book, there was a period where Leo was just kind of frustrated with, well, really all users, but especially the mathematical users. And while he was working on Lean 4, he kind of hold off and, you know, he kind of needed his distance. And, you know, every once in a while I would send him an email and get a quick response. But it was clear that he wanted some distance. And that was hard. You know, I missed him because he's a very good friend. And I missed just kind of constantly being able to bounce off ideas and so on. And so I contacted him. So I was in, as the book explains, I was coming to Seattle for the joint mathematics meetings, the big American, you know, big U.S. math meeting every year. And so Leo arranged the dinner. It was other people were in town for the conference. he decided to take the opportunity to bring together advisors for the Lean Focus Research Organization. So it wasn't a birthday dinner. It was really just bringing together people interested in Lean and supporting Lean.

But I told him that my birthday was that week, and he decided to make it coincide with my birthday. But what I really was looking forward to 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 we just met at Pike's place and we just kind of just walked and just walked and walked. And yeah, it was just great talking to him again. You know, we talked about Lean, but we talked about things that were not Lean. I mean, for both of us, it's been, I mean, the last several years has been surreal. I mean, we just remember the early days of Lean, you know, 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 back on all that, it almost seems surreal. I mean, it seems very surreal, you know, how far we've come. Now, Kevin Hartnett 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. you