Mathematics Just Changed Forever — Kevin Hartnett
Machine Learning Street Talk (MLST)Episode Description
Summary
This episode explores the revolutionary impact of interactive theorem provers like Lean on modern mathematics, focusing on Kevin Hartnett's book 'The Proof in the Code.' It covers the history of computer-assisted proofs, the challenges of formalizing complex mathematics, and the emerging role of AI in accelerating mathematical discovery and verification.
Chapters
Topics
People
Key Concepts (15)
References (10)
Transcript (89 segments)
In the world of expense management, SAP Concur is here to help. From cost control slipping to travel chaos, SAP Concur has an integrated travel and expense solution to help you overcome problems like overburdened teams, decisions looming. When travel, expanse, and AP are connected with a single AI supported solution, SAP Concur keeps you ahead of problems.
Visit concur.com to learn more.
This episode is brought to you by Google Chrome. You think you know a browser, but Gemini and Chrome, that's new. They can help you with practically anything on the web, like restoring a vintage motorcycle from a 50 page restoration block or finally break down that long article you've had open for weeks.
Gemini and Chrome is here for it. Ready to make anything online make sense? There's no place like Chrome.
Check responses, setup required, compatibility, and availability varies 18 plus.
The Fields Medalist, Peter Schultz, 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. You have an algorithm that can check whether the proof is correct or not.
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. Mathematicians have had various different reactions to this ranging from, you know, what could only be described as grief.
Can I make a machine prove 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 Git 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, I'm just gonna check it.
Four hundred years ago when Johannes Kepler was in a greengrocer, 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 naught point seven four, which is the ratio of the optimum, you know, pyramid placement. Kevin Hartner 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 D'Amora, 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 naught point seven four. 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.
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.
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. 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, 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 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 Hayles claimed they did. When Hayles had finished the proof in the summer of nineteen ninety eight, 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 caught frustration by applying the same methods to other problems?
the creator of Lean. The paper was accepted with a disclaimer saying something like, we're 99% confident this proof is correct, but then Tone starts using proof assistance. This all happened before Lin.
He uses Hall 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 assistance.
And and Tono was famous twice for for solving the Kepler conjecture and for using a proof assistance, right, in a paper that the math community cares.
using Lean was a big chill 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.
It's very much a social process. They kind of have a general understanding for what works already, they kind of know the person behind a proof, can kind of trust that this person kind of understands the way things should go And then they can check a proof, they can check 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 close to the existing body of knowledge, when they go just incrementally beyond things we already understand to be true.
Yeah.
why does it matter that we can prove something versus just know something is true?
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. 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. 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 Komelin, for example, he's a 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 piece. 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. 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 wanna talk about symbolic AI. 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.
Does that remind you of anything? Yes. If you look at AI proofs now, they have a similar property.
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 assess the value of a new mathematical result is it... Does it enable additional results?
Do you invent new concepts, new abstractions, new definitions in the process of prosecuting an argument that then have widespread utility for answering other questions? And in Hales's case, there were some computational methods that he would have wanted to apply to other problems, but he was not inventing broadly new mathematics. In a certain sense, the techniques he used were fairly elementary.
He himself acknowledges that. So he was not creating new math in the same way that Andrew Wiles had to create new math when he saw Fermat's last theorem, where he had to invent some very powerful new concepts that just opened up entirely new branches of the field. So Hales' proof was not like that.
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 prove stuff?
Sure. But I'm interested in, like, understanding it. Right?
And I'm still the one who has to understand it.
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'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 Broglie 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: twenty:one 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,000,000 each to participate.
Apply now at cyber dot fund. Folks 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 assistance.
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 the LeanMathLib.
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 the 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 trusted kernel. At least massive, has zillions of bugs.
Right?
in Lean, you 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. 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, ITP's such as Agda, Koch, and Isabelle 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, Damora 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 light, 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 do it in the style of a mathematical proof. He could 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. 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. Leo, though, following the great success of Z3, not just for Microsoft, but 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 correctly prove true or false for those problems most accurately wins.
Z3 was the world champion at it, so he essentially had climbed to the top of the automated theorem prover mountain, but he also was dissatisfied with the fundamental limitations of automated theorem prover technology. There's 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 just a wider range of truths you can try to encode and verify. And interactive in the sense that 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 D'Amoura 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 at math.
it can be used for solving many, many other problems in abstract mathematics, are significantly more complex.
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 assistance started just kind of as a hobby, just messing around with them because I thought they were interesting around the year 2000. So quite quite a long time ago.
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 Light's design and implementation. In my opinion, it's the most elegant by far.
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 high order logic. It's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough.
Right?
it's not... It's important to have a good library... A math library for verifying software.
For example, cryptography, we need a lots of math. Differential privacy is another example. So having a good mathematic 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. It's...
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 Fournier.
He uses Ling now. And he told me, look. The MathLib, the Ling Mathematical Library, have the right obstructions I need for verifying cryptography.
Right? I mean, because of all the generality that's having the Peninsula bacteria 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.
but it's... I think it 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.
I had worked in 2009 and 2010. I spent a sabbatical year working on the the formalization of Fight 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 Isabelle extensively, which is a proof assistant based on 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. It still to this day has excellent 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.
And so after my year working with Ruck, 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 from, you know, 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, you know, foundation.
And so he needed convincing there that the trade off was worth it. 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 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 filmm...
Familiarity, yeah, he he needed convincing at first.
Leo emails Jeremy back during that summer of twenty thirteen 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 in the way he's always wanted an interactive theorem prover to potentially be useful. It's funny.
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 I'm 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.
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, 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. 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 requests. 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 four, but for years, you know, we were at Lean two 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 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 over and they were able to look after themselves a lot more, I wanted to get back into doing hard research mathematics. I realized that there was a huge amount of material that I was going have to catch up on.
I had some kind of midlife crisis around that time. I was trying to read it, and I couldn't understand all of it. I would find what I thought were mistakes in the literature.
Then I started thinking, Well, wait a minute. This is very abstract stuff. It's not immediately clear there's any concrete applications, so there's nothing that we can test these things on in reality.
And if they're not right, then what is the point of this stuff at all? So I had some kind of crisis, and I started thinking, Would it be possible to check mathematics using machines? Because technology is moving very fast.
And so I went down some kind of rabbit hole, just 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 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 got hooked because 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. 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. 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 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 Sholte'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 whether they were correct, and if they weren't, fix them.
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.
which means the task is complete. When Lean... 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 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 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, Johann Komelen, Patrick Massow, 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 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 Quanta 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 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 Lean's mathematics library.
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.
It just got this concept of the real numbers, which was something known to the ancient Greeks and the Babylonians. It was thousands of years old. It didn't have the complex numbers, which are from about five hundred years ago.
So there was clearly a lot of work needed doing. I spend a lot of time teaching, and 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 that you kind of say, Okay, you learn all this stuff at school, but actually, we're to start again from the basics and just work through everything quite quickly. 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. I 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 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.
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 set anything on fire, or it be illegal. So I could stay late at work. One evening a week I'd stay late at work and just let the kids muddle on by themselves.
And I would teach undergraduates how to use this software, and then I would get them to start transcribing what they were learning in their undergraduate degree, just teaching it to this machine. So the library just like I mean, there was lots of other people around the world doing well, not lots, but there were plenty of other people around the world doing the same thing. I was treating this thing as an undergraduate at the time.
So it's 2017, and the question was, Let's just imagine you've enrolled on our degree. Can we actually teach you at the same rate as we teach the undergraduates? And it was just about possible.
The thing was learning at the same rate as our students at the time, but three years later, we could 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... They're not quite fully formed. There are ideas which sort 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.
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.
If we want polished mathematics, stuff which is still a bit chaotic, One can attempt to teach it the software, but we don't necessarily want to add it to the library. The library wants to take fully formed, well thought out, beautiful conceptual ideas which 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, 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. We try and avoid this. Like to get things right first time.
Occasionally we have had to go through and change a fundamental definition.
then break and need to be fixed. Kevin Buzzard has the instincts of a showman. He's 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 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, 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 Schulze, who is today and then as well considered maybe the greatest living mathematician.
Perfectoid spaces are truly state of the art objects 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 Kamlan start this effort just the three of them to create a blueprint, essentially a guide to the things they would need to define and lean in able order to to write the definition of a perfectoid space. So it's essentially a punch list, like a construction project.
We would need you to define this, and then this, and this, and this, and ultimately we'd 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. They have about 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 space 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 starts to convince people. It starts the process described in the book of convincing people Lean can be used for real math.
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. 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. 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. Even though I couldn't go to the conference, I could still watch the talks.
The first talk was given 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 exactly the thing that I'd become worried about. He was talking about formalizing modern mathematics, perhaps all of modern mathematics.
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'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 like a PhD thesis worth of work, 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.
In reality, you would imagine that maths was this perfect language where everything can be expressed you know, in a in a completely unambiguous way. But in practice, this is not this is not what happens. In practice, you you read you read section three of the paper.
In section three, it says, from this point, p will be a prime number which is at least five. And then you read something in section seven 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 three, If you start reading in section seven, 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, what's going on in section seven, 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 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 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, was what the library looked like in 2017. It contained some definitions that 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. This just seemed to me like a viable way to move forwards whilst engaging with interesting material. 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, to do the same thing. We've spent a year working on this now, and it's becoming viable. We're taking theorems published in the top pure maths journal this decade, We're trying to translate just the statements of the theorems into the language of the software.
We're 20% through, so that's some indication that at least this dream is slowly becoming a reality. I would imagine that in a year's time, we're gonna be far more than 20% through. So Hales had these ideas which have taken years to become real, but now they are becoming...
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 tedious. You have to spell out every little detail.
Even things that are trivial or obvious to mathematicians, you need to convince the computer of their correctness. There are a few moments in the book where a mathematician is reading a proof it's written informally on a PDF and they want to formalize it, incorporate it, 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.
How would you convince me one plus one is two? We all know it's correct, but once you actually start to think about how you would impress someone who's not it's hard. Terry Tau, 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 D'Amora'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 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.
Scholzer was the mathematician others turned to when they needed their proofs checked. So in in November 2020, I was contacted by the Fields Medalist, Peter Scholzer. This was back when the library had just basically graduated in some sense.
It knew a lot of undergraduate level mathematics, but not too much else. Scholzer asked me if I'd carefully read his latest preprint. And the answer to this was, well, absolutely.
You know, we'd had a study group on it at my university. In 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...
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. Yes. Yes.
We'd 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. 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'd read the statement of the theorem, we'd understood what it was trying to say, and the point of it, where it fitted into the grander scheme of things. And the proof was just six pages of technical calculations that we had skimmed through at best.
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 and said, We looked at it.
We didn't read the details. And he said, That's what everybody says. And he'd asked 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 skimmed over his work. And of course, the devil is in the details in mathematics.
He said, At the end of the day, this material 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 staff. And all of a sudden, I've got this Fields Medalist suggesting that we could check part of his most recent paper. 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. As I said, 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. We did wonder whether it would be feasible to plough through these six pages. 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. Johann Komelon in particular found a simplification.
So that cut the time down by a factor of two. And six months later, we'd checked the key thing that Peter was... Peter was worried that the thing was wrong.
Peter's like, I think it's right. My co author thinks it's right, Dustin Clauson. No one else has read it.
Maybe it's wrong. So six months later, we'd read it through him was like, It's okay, it's right. The machine says it's right.
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.
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, Quanta was on the, you know, nature was calling me up. So at this point, I realized that we had arrived.
Now the, you know, now the sort of the big league people were taking an interest. Then it sort of, you know, it went on from there. Then of course, 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?
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, so here's where to start. And 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 was some mathematicians found that a very appealing way to spend their time.
So there was a big jump in the rate of growth of the library.
When you have a mathematical proof in lean fully spelled out, you can 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 started talking about whether you could apply the AlphaZero approach, the zero knowledge approach, to having an LLM recreate mathematics, if you just give it the basic axioms. The question we were talking about was, would an LLM rediscover essentially human mathematics, or how far along would it get? And 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 advancing along the human understanding of math, starting at the rational so almost at the very, very beginning they expected computer math would diverge from what has become human discovered math. And I think the reason is we have this feel for the right abstractions, these satisfying concepts and definitions that feel right to us, that feel complete, that feel expansive in 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 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...
that have ultimately become meaningful to us. 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, 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, told the story of Alpha Proof.
So this was back in 2024 and they actually used lean as part of that architecture. It's very interesting in context as well, because the newer versions don't use Lean, possibly not yet, but 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 both just an obvious test 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, receive 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. 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 twenty twenty four 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 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.
for the IMO. AlphaProof 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. DeepMind eventually auto formalized about 80% 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 EpochAI's fixed budget test, a prerelease open AI 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 8, 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 Tau 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,000,000 questions down to 238. By late November, they were down to a 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. Tau 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 Tau sometimes calls math from Mars.
As the team crossed implications off its immense table, it stumbled onto genuinely new constructions, including magma cohomology. John Bayes, an expert in cohomology who had initially called the project a colossal waste of time, admitted that he had never encountered it. To Tau, 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 the engines, is going be essential for model training. I think it's also extremely useful for exploring a wide variety of possible proofs.
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. 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.
The philosophy of the library has always been: find the right abstraction and develop everything in that correct generality.
has been quite interesting because we always firmly believed that finding the right abstraction would just make our lives easier later. 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 grueling to just kind of bash through this stuff in not really the generality it should be working.
Things are much more complicated. As humans, you don't want to plow through stuff when you feel, I should be sailing over this. 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. As an example, if we did want to change a fundamental definition in the library now, AI would be great at that.
AI would fiddle around at the roots, break everything, and then it would just plow through and fix everything. 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 Math Lib maintainers, this fundamental maths library which everything is building on, we are still absolutely of the opinion that to get into our library, it needs be conceptually the right way of doing things. But there are of course plenty of other developments in mathematics now. This wasn't true five years ago.
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, we don't necessarily need to find 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: 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.
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.
I mentioned writing the fiddly lean syntax as a real barrier to entry for mathematicians.
Obviously with identic coding, you don't need to learn all that lean. You can just 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 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. 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 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 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 is not always defined with exactly the precision, the economy with which you want these canonical objects in MathLib to be expressed.
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 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, you know, is a well specified formal language, and that's exactly why we can write computer programs that what humans mean when they speak in mathematical terms. Mathematics should contain no ambiguities at all. 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 of people speaking to other experts just knowing experts know what humans mean when they say things. So sometimes what ends up on paper is sort of 99%, but not a 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 exactly what they mean at all times. But because I've been doing this project of carefully so I'll tell you a story.
This is a this is a story that's not been made public yet, but I'll tell you a I'll tell you a story. 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.
The AI found errors. The errors were of two forms: there were errors that my team had made. 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 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 nonempty. There were there were things that that he...
And 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.
Right? It it... That strictly speaking, what they've written is false, and And it's obviously not true, in fact.
If you're an expert in the area, you would say, Well, obviously they mean this. I think this is quite humbling. I think as a community, we should take a look and we should step back and think, Well, actually, we say we've got this precise formal language where we can express exactly what we mean, but in practice, we're only using it at 99% capacity.
And one of the things that machines will offer you is the chance to upgrade that to 100% capacity. The machines will say, well, this theorem 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 a 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 argument 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 a proof, that... That's where the mathematics just...
Is is just is just dying. I mean, it's just... You gotta do it.
You gotta check, 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.
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 form... In this framework where we can be very precise.
Well, I suppose after formalism, what exactly do you know more of,
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. 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 and 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 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, and 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 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.
Alongside concrete tactical discussions about the project, Komelin and Sholte say debated philosophical aspects of formalization. Komelin saw lean as a better way to work. Sholtze did not.
These different orientations came through in Komelin and Sholtze'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 Sholtze 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, the 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 look like a duck and quacked like a duck, perhaps they really were defining a duck. The examples were not watertight evidence, but Komelin 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 hell, and every plausible looking contribution creates a review burden for somebody else.
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 just need to focus now because it's just...
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 you, no. This doesn't work. Something that's, for me, one frustrating scenario.
You throw an idea. You you didn't spend five minutes thinking about it. 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 the receiver.
Right? You have to do your work now.
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 a Claude agent 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 to its passage that are suites that comes with the c version.
you get the original data back. I liken it to the blind men and the elephant, 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 Zedlib, whether it actually encompass the whole or just some perspective of it. But I suppose the problem when you only have a perspective of a bigger complex whole, get problems in terms of, you know, we're talking about reward hacking and, you know, like Goodhat's law and 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...
algorithm? Yes. Yes.
For for example, one way to do... He was hacking this compression decompression. Suppose that's that's what's the only property we ask is the the the AI to show, to demonstrate was that was achieved.
The AI could hack by saying compression, you just hit on the data. It's the identity functions. You just hit the decompression, you hit on its 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 the AI.
You have to show that you compress as much as the Rust implementation in the test suites. But you're completely right. It's really easy to give cheese that do not cover the whole thing.
Right? And if you want to do... If you see the AI as an assistant 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... Want to let the AI go wild and you don't even want to look at the codes, it's really important to cover all aspects. Right?
but you do not fully specify what you wanted. You... You're not really getting what you want.
There's some scepticism that formal verification is going to be broadly useful for verifying the correctness of all of this AI generated code precisely for that reason.
most programmes 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 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, There's this problem of we're building things we no longer understand, we can't verify them.
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 much more powerful because you can use AI to write these specifications themselves, they don't have to be written by hand.
I think formal verification of software programs will increasingly have a role to play in the new AI powered software development lifecycle. There are players 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.
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.
is coming from mathematics. This is absolutely clear. 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. Mathematicians have had various different reactions to this, ranging from what could only be described as grief, that the subject is changing and that they're going to have to adapt or die. 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 it's its worst. Today is the worst it will be. Going forward, it's going to be much better.
It's already awesome, and it's much worse than what it will be this time next year. 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 and great tools where we can explore new dark corners and enlighten them and enlighten our community.
So going forward, things look very exciting.
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. You know, again, what I care about is how am I gonna interact with it?
So, 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?
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. It's... If it's our...
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 D'Amora, and that was actually the first moment in which I understood, in a certain way, the significance of what I was doing. Not for the world, but just as 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.
My book was likely to be the only start to finish story of the development of Lean and just started to feel extremely important to tell the story well.
who at the time worked for QUANTA Magazine and wanted to run a piece on Lean and its mathematics library for QUANTA. So I ran into Kevin around then, and 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 worth writing a book on.
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 how it happened. He wanted to put together the people behind the story and what was going on.
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 the story that Kevin decided to tell.
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 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 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. 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 when Kevin interviewed us, you know, there were there were the the the bumpy spots along the way, and there were the... You know, there there were these tensions.
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.
And and when there were tensions involved, sort of, you know, making them... Making it come across that. Again, it wasn't a matter of good guys and bad guys, but just people looking for different things.
all the math activity and MathLib is still continuing apace. It just never felt like I understood what was going on in those years. 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 Lean4. Please leave me alone, in so many words.
They get the message, they're a little wary of angering this guy who they admire and is so important to them. There's 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 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 twenty eighteen to twenty twenty two period. Anyway, what was interesting for me though was realizing I'd been hearing this story, it didn't quite make sense to me, I didn't quite know why, and then almost 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 the 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.
if you read the book, there was 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 four, he kind of hold 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 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'd contact 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 US 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 advisers for the lean focused research org...
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. But but I told him that my birthday was that week, and he decided to make it coincide with my birthday.
But but what I really was looking forward to was not not 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 kinda just walked and just walked and walked.
And, yeah, it was it was just... I don't know. It was just...
It was talking to him again. You know, we 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 can... 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 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. Now, Kevin Hartner really brought this story to life.
speaking of all of these guys. So I highly recommend you read Kevin's book. And until the next time, cheers.
Mister Monopoly here. Miss me? Monopoly is back at McDonald's with millions of prizes.
and Best Buy. Peel then play in the McDonald's app. Get your bag.
No purchase necessary. 50 US and DC age 18 plus. See play at mcd.
com for rules and play at mcd.com/amoe for info and playing without purchase by mail by November 2. Chance card game ends November 8.
Game ends 11/22/2026.
See rules for price details. Monopoly is a registered trademark of Hasbro. Shaq here.
What's it like to buy a car from Carvana a 100 online and get it delivered to your door? Let me tell you. Your car is here, mister Shaq.
Thank you, mister Carvana guy. Can't wait to take it for a spin. Only the best for you, mister Shaq.
Hey. Have you always been so big, tall, and handsome? Not always.
I was six ten once. Seven days to love it or return it, mister Shaq. Not that I would.
You never do. No. I never do.
So buy your car today on Carvana. Delivery fees may apply. See our seven day return policy at carvana.
com.
Shared via Hopper