Mathematics Just Changed Forever — Kevin Hartnett

The Fields Medalist, Peter Scholze.

The proof was just 6 pages of technical calculations that we had skimmed through at best. He’d become convinced that nobody had actually read his work. We found 4 Fields Medalists who had 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 3.

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. Something has now actually finally read it.

AI is coming for mathematics. This is absolutely clear. Companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean.

Mathematicians have had various different reactions to this, ranging from what could only be described as grief.

Can I make a machine prove stuff? Sure. But I’m interested in understanding it, right? I’m still the one who has to understand it.

It can output millions of potential proofs, but you need to quickly sort through them to find 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. Here’s the GitHub repo. Read it if you want. Does anyone want that?

You multiply 2 numbers on a calculator, you get a result. You just take the calculator’s word for it. Nobody’s going to check it.

1. Kepler's oranges and the proof nobody could check

400 years ago, when Johannes Kepler was at a greengrocer’s, he had an interesting idea. He was looking at the way oranges were stacked on top of each other in a pyramid, and thought that might be provably the densest possible configuration. Unfortunately, it was impossible for him to know for sure whether his idea was correct.

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 without making too much progress. Two mathematicians, Thomas Hales and Samuel Ferguson, reduced it to a finite set of cases. Back in those days, computers were incredibly slow, so almost on a case-by-case basis, they had to write an insanely optimized computer program, with lots of heuristics doing intersection checking and so on, to show that each case was less than about 0.74, the ratio for the optimal packing.

Kevin Hartnett tells this story in his brand-new book, Proof in the Code. The book isn’t just about oranges and Kepler’s conjecture, but that’s certainly where it starts. The thrust of the book is mostly about Leonardo de Moura, the creator of Lean, and the tumultuous, fascinating journey he went on with many of his collaborators to get Lean to where it is today.

Hales had a bit of paper on his wall, and every single one represented one of these configurations. They became harder and harder as the density converged toward 0.74. It took him many, many years to do this, and eventually he did it. He had 1,767 computer programs, one for every single configuration of these balls, and he was elated.

So he published his work in the Annals of Mathematics, expecting a celebration: he had just proved Kepler’s conjecture. Unfortunately, that’s not what happened. He dumped this proof on the editors of the Annals of Mathematics, the most prestigious journal in the field, and they essentially didn’t know how to referee it or send it to other mathematicians to verify its correctness. It languished for many years without actually being determined true or false.

For many years, mathematical proofs were done high up the abstraction mountain. Mathematicians made high-level arguments, and it went without saying that certain arguments had been proved before. You didn’t need to go step by step; the proofs were very parsimonious. When you submitted your paper to a journal, the reviewers could 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. 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 that 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?”

The paper was accepted with a disclaimer saying something like, “We’re 99% confident this proof is correct.” Then Tom started using proof assistants. This all happened before Lean. He used HOL Light and Isabelle to do this work, but it was a milestone. It was a big result that had been formalized in a proof assistant.

Tom was famous twice over: for solving the Kepler conjecture and for using a proof assistant. And the fact that he decided to do the next projects using Lean was a big deal for Lean. That’s a paper the math community cares about.

2. How mathematicians decide a proof is true

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? How can they trust a new theorem and then use it as an input into additional proofs?

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

Yeah. I mean, suppose a fundamental noob question is: why does it matter that we can prove something, versus just know something is true?

I think the main thing is that 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. For math, this is useful for trust. You can collaborate with people you’ve never 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 with high schoolers, and they can contribute to my projects. I don’t need to check whether their proofs are correct.”

You can view big math projects as engineering projects. Johan Commelin, for example, is a really hardcore mathematician, and he’s a software engineer. He doesn’t know it, but he’s a software engineer. He breaks big projects into smaller pieces, and people can fill in the smaller pieces. He’s like the architect of the project, and people start filling the holes. He doesn’t need to check everything manually. Of course, he’ll look later to see whether people can maintain the proof. But you don’t have to keep thinking about whether the proof is correct. He knows the proof is correct. He can clean it up and improve it, but the proof is correct. That’s valuable.

3. Correct is not the same as useful

Earlier this year in Melbourne, I caught up with our favorite category theorist, Paul Lessard.

We want provenance. We want to know why. That’s the thing I’m much more interested in if you want to talk about symbolic AI. The thing that’s interesting is, I don’t merely want 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 the reason.

Thomas Hales’ proof was extremely verbose. It was complex. He was going through it 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. 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. One way you can assess the value of a new mathematical result is to ask whether it enables 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?

In Hales’ case, there were some computational methods that he would have wanted to apply to other problems, but he wasn’t inventing broadly new mathematics. In a certain sense, the techniques he used were fairly elementary; he himself acknowledges that. He wasn’t creating new math in the same way that Andrew Wiles had to create new math when he proved Fermat’s Last Theorem, inventing powerful new concepts that opened up entirely new branches of the field.

So Hales’s proof was not like that. There’s probably utility in generating proofs that aren’t constrained by our desire for interpretability. But when you talk about doing actual mathematics, I’d still like to think human understanding is at the center of it. It may not be, but I think those are different quests.

Can I make a machine prove stuff? Sure. But I’m interested in understanding it, and I’m still the one who has to understand it. There’s resistance because mathematicians, by and large, didn’t see the value in that kind of time investment. Hales invests 20 person-years in formalizing his Kepler conjecture result, and at the end all he gets out of it is assurance that it’s correct.

That’s much less exciting than getting new math and new discoveries, especially in situations where you’re already fairly confident things are correct. In most cases, mathematicians know when things are right or not. They’re not troubled by correctness. There’s a factor called the de Bruijn factor: the number of lines of code you need to write in Lean for every 1 line of informal math in a LaTeX PDF. It’s very high—20 to 1, often higher. Mathematicians generally don’t see a reason to invest that additional time just to verify correctness. That’s really where the resistance comes from: they don’t see the utility of Lean for the thing they care about most, which is discovering new math.

4. Sponsor: Cyber Fund

This episode is supported by Cyber Fund. If you're building at the frontier of AI, they want to hear from you. Cyber Fund believes the future belongs to AI natives who want to achieve the impossible. And that's why they're introducing the Monastery for AI native founders. 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.fund.

5. What Lean is, and the small kernel it trusts

For folks who are 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 code, and Lean is actually implemented in Lean itself. The cool thing is that you can prove properties about your code. You can state mathematical theorems and prove them. You can build a mathematical library like Lean’s mathlib.

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 2 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 proofs correctly adhere to the rules of the logical foundation. The kernel answers the first question anyone asks when they learn about an ITP: if the ITP says a proof is correct, how do I know it hasn’t made a mistake?

We have the notion of a small, trusted kernel. Lean is massive; it has zillions of bugs. But to trust our results in Lean, we only trust the kernel. That’s much smaller.

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 Isabelle have 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, de Moura knew he would need to keep the kernel as small and minimalistic as possible, comprising as few lines of code as he could. Among the ITPs already on the market, de Moura admired the minimality of HOL Light, which had a very small kernel.

6. From Microsoft's Z3 to Lean

Back in 2006, there was a lot of duplicated effort at Microsoft. Some people were building their own theorem provers, while others were working on obsolete theorem provers. It was at that point that Leo decided to start working on Z3. Leo built Z3 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.

With Z3, you can construct a pathway through the software as a series of variables and prove that those variables can never take the right combination of values that would make a statement true. If you prove that the software cannot arrive at that state—that set of variables—then you’ve categorically ruled out a bug, at least in one particular direction. Leo built Z3 as a way to automatically check different pathways through Microsoft software for bugs and guarantee that there were no bugs.

Z3 is a type of program called an automated theorem prover, because all of this work is done automatically once you set things up. There isn’t much 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.

Following Z3’s great success, not just at Microsoft, Leo and his collaborator entered it in automated theorem prover competitions. ATPs from all over the world were given a set of problems within a set amount of time, and whichever ATP could most accurately prove them true or false won. Z3 was the world champion.

Following Z3’s success, though, Leo 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 they can verify as correct, if you want to put it more broadly. So he turned his attention to building a related but more powerful type of program called an interactive theorem prover. It has a much richer, more expressive language, so there’s a wider range of truths you can try to encode and verify. It’s interactive in the sense that a human user can nudge the program toward greater expressiveness, which makes it much more powerful.

What my book is, ultimately, is the story of how Lean, this interactive theorem prover that de Moura builds to verify the correctness of software programs in a richer way than he could with Z3, gets co-opted by mathematicians who see its potential. For the first time, an ITP breaks through into a more mainstream way of working in math. In Lean, because it uses dependent type theory, it can be used for solving many other problems in abstract mathematics that are significantly more complex.

7. The argument over Lean's foundations

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

I’m a mathematician by training, specifically a logician. What I like about logic is that it’s somewhere between mathematics, computer science, and philosophy. Here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started as a hobby for me, just messing around with them because I thought they were interesting, around the year 2000, so quite a long time ago.

Just after midnight on the West Coast, de Moura sent a long email to the group, softening some of the concerns he had raised. “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.”

I want to use higher-order logic. It’s a simpler foundation, much easier to implement. And for many software verification tasks, it’s enough. But for doing abstract mathematics, it’s not. It’s important to have a good mathematical library for verifying software. For example, in cryptography, we need a lot of math. Differential privacy is another example. So having a good mathematical library is important even if you only care about software verification.

From my point of view, it’s important to have users. That’s what the users wanted. I wanted support. I wanted to have Jeremy as a user. I knew others would come and it would pay off. Many of my colleagues who work on cryptography say that. For example, one of them is a former colleague of mine, Cédric Fournet. He uses Lean now, and he told me, “Look, mathlib, the Lean mathematical library, has the right abstractions I need for verifying cryptography.” Because of all the generality that dependent type theory provided, we have a library that’s more expressive, has the right abstractions, and is cleaner. It paid off in the long term. It was a lot of extra work at the beginning, and getting 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 dependent type theory because it was useful for solving the types of problems you were interested in.

Before starting the Lean project, I had worked on the formalization of the Feit–Thompson theorem in 2009 and 2010. I spent a sabbatical year working on it.

And that is in a proof assistant known as Rocq, which is based on dependent type theory. Before that, I had worked extensively with Isabelle, a proof assistant based on a simpler logical framework called simple type theory. Isabelle is a wonderful system, and for many things, it’s absolutely ideal. To this day, it has excellent automated support, so for certain types of mathematics, it was a really great system.

But for certain things, you hit a wall. In modern mathematics, mathematicians talk about algebraic structures characterized axiomatically. They’re ubiquitous, and there are complex networks of them. Simple type theory just isn’t good for that. After my year working with Rocq, it became clear to me that this was the framework capable of doing that type of mathematics. I think other mathematicians who had experimented with Isabelle and other systems were coming to similar conclusions: to do the mathematics they wanted to do, they needed this very expressive framework.

The thing about dependent type theory is that it’s very powerful and expressive. But I like to quote the Spider-Man franchise: “With great power comes great responsibility.” It’s a very powerful language, but it’s also very hard to implement and can be more difficult to use. There are a lot of gotchas and corner cases, so it’s a weightier, more complicated, and more difficult framework.

When Leo first started the project, he was aiming for simplicity—a very simple, formal foundation. He needed convincing that the trade-off was worth it. In the end, he came around. Now he’s one of the biggest proponents of dependent type theory. Soon after, he would say that it was really beautiful. He recognized the benefits, but coming from the outside, without familiarity with it, he needed convincing at first.

Ultimately, Leo emailed Jeremy back during the summer of 2013 and told him, “I’ve decided to go with dependent type theory.” Jeremy basically did a dance at home in Pittsburgh because he knew the seeds were there for Lean to be useful in math, in the way he’d always wanted an interactive theorem prover to potentially be useful.

It’s funny as a developer. When you’re wearing your developer hat, usually you want to go with whatever is simpler to implement, and you forget that you’ll sometimes be a user of the tool too. I always joke, “Honey, if I’m wearing my user hat, I want this feature. If I’m wearing my developer hat, I don’t want it.”

Oh, yeah. So Leo is extremely self-critical. There are many moments in the story of Lean’s development when he has users who love it, and he says it’s shit. He just thinks it’s terrible. All he sees are its flaws, and he wants to fix them very doggedly.

8. One researcher versus a growing user base

At Microsoft, Leo feared that 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 scientist at Microsoft Research. He’s not a project manager or a product manager, and he doesn’t have a team of engineers working with him. It’s just him and an idea.

Through Jeremy, Lean very quickly gained a number of mathematicians who wanted to start using it. They loved it; they didn’t think it was shit. They thought it was way better than Leo did, but they also had additional feature requests. Wouldn’t it be great if they could do this? Wouldn’t it be much easier if they could do that? Could they have a richer UI?

Leo wants to please the users. He’s extremely user-oriented, and it’s very hard for him to receive a piece of feedback—especially if he recognizes it’s fundamentally correct—and ignore it. He found himself responding rapidly to users who weren’t even the users he’d intended to build for, doing something that wasn’t even what he’d planned Lean to be useful for. He started fulfilling their requests.

I think he was bombarded by emails and, later, Slack messages. He couldn’t really say no to them, but he became intensely frustrated because he felt they were taking him for granted. He felt they thought he had more time than he did. Most importantly, he had a vision for where he wanted Lean to go. There have ultimately been 4 versions of Lean; we’re currently on Lean 4. For years, we were on Lean 2, and Leo saw where he wanted it to go. He felt inhibited in his ability to find the time to get it there because he was answering all these user-support questions and queries from mathematicians.

9. Kevin Buzzard's house of cards

One of Lean’s earliest adopters and most enthusiastic evangelists was a mathematician at Imperial College London named Kevin Buzzard.

My name is Kevin Buzzard. I’m a number theorist working at Imperial College London. At the beginning of this century, I spent some time bringing up 3 kids. When that was more or less over and they were able to look after themselves a lot more, I wanted to get back into doing hard research mathematics.

I realized there was a huge amount of material I was going to have to catch up on. I had a kind of midlife crisis around that time because 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, “Wait a minute. This is very abstract stuff. It’s not immediately clear that there are any concrete applications, so there’s nothing we can test these things on in reality. If they’re not right, what is the point of this stuff at all?”

I had a kind of crisis, and I started thinking about whether it would be possible to check mathematics using machines, because technology was moving very fast. I went down a rabbit hole, exploring the software that claimed it could check mathematics with superhuman accuracy. It absolutely could, but the problem was that 99% of what it was checking was really basic material known for hundreds, or maybe even thousands, of years.

By that stage, I’d gotten hooked, because I realized there was this weird new way of doing mathematics. I’d never really seen anything like it before. I started to realize that doing mathematics in software, even though it was very basic mathematics, was a lot of fun and very different from doing it with paper and pencil.

Then I was in this hole, and suddenly the original questions just went out the window. I was thinking, “This software is really great. What can we actually get it to do?” At the time, we could barely get it to do undergraduate-level mathematics. But it was great fun using it, and that was how I ended up switching.

By 2016, Kevin Buzzard had time to return to the p-adic Langlands program. A young talent named Peter Scholze had transformed the geometry of numbers with perfectoid spaces, and Buzzard wanted to be part of the revolution. But as he read the papers that followed Scholze’s work, his enthusiasm gave way to concern.

Buzzard liked to see every detail spelled out. He disliked vagueness and assurances from authority, what he called “the opinion of the elders.” That perspective could bless promising ideas before they were fully defined. But in the papers he reviewed, Buzzard thought it had become a permission slip for sloppiness.

His critique was not of Scholze’s work, which he actually found brilliant and rigorous, but of the results built on top of it. He noticed mistakes in some papers and logical gaps in others, and experts 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 the pieces fit together. He saw one sloppy, incomplete paper building on another and worried that his area of mathematics was turning into a house of cards. To him, that was the draw of Lean: he wanted to take papers that had developed in his field, formalize them by converting them into a computer programming language, and determine with complete certainty whether they were correct. If they weren’t, he wanted to fix them; if they were, it would renew his confidence to proceed with research in that area.

Here’s a small example. The ring tactic constructs a proof of this algebraic identity using machinery from Mathlib. Lean then checks the proof and says, “No goals,” which means the task is complete.

When you boot up Lean, it doesn’t know any mathematics. It’s equipped with basic axioms and rules for math, so it has some understanding of mathematical logic. What you need to do is equip it with a library of definitions.

10. Mathlib as a barn raising

This is the parallel story in my book. There are 2 key stories, 2 dreams almost, that are very dependent on each other and sometimes in tension with each other. 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 spearheaded by several of the main characters in the book.

People like Kevin Buzzard, Johan Commelin, Patrick Massot, and Jeremy Avigad are very involved. Mario Carneiro is another important figure in the development of Mathlib. The vision is for it to be a crowdsourced effort to define basic concepts in math, in Lean, from the ground up. That means starting with high-school-level math and going up to college-level math, so you have the ingredients to encode more sophisticated forms of mathematics later.

That’s how Lean breaks beyond combinatorial results like the four-color theorem and Kepler’s conjecture, and becomes a place where you can express deep, frontier-level abstract math. It’s through the development of mathlib. 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 a community effort to get this massive thing done without any central authority or 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 had just got this concept of the real numbers, something known to the ancient Greeks and the Babylonians, thousands of years old. And it didn’t have the complex numbers, which are, I guess, from about 500 years ago.

There was clearly a lot of work needed. I spend a lot of time teaching. That’s part of my job. I teach undergraduates. They come in, and the way it works at university in a mathematics department is you say, “Okay, you learned all this stuff at school, but actually, we’re starting again from the basics and just working through everything quite quickly.” One of the things we teach them is how to define the complex numbers, this basic number system that goes back to Descartes.

I thought, “This thing doesn’t have the complex numbers. Let’s teach it the complex numbers.” So we defined the complex numbers and proved basic things about them, and it was great. I made a pull request to this free, open-source maths library, and it got merged into the main branch. Suddenly, we had “complex numbers, copyright 2017 Kevin Buzzard.” I was thinking, “Great. What’s the next thing that we teach them?” I was thinking about what we actually teach our undergraduates, what’s missing, and what should be in this library. Why don’t we just contribute to this library?

Of course, there’s so much stuff that one person can’t do it. So I roped in the undergraduates. It was absolutely critical. We’d just got to the point where all my kids could make their way to school by themselves. They could make their way to and from school, and you could leave them in the house, and they were unlikely to set anything on fire or do anything illegal. So I could stay late at work one evening a week and let the kids muddle along by themselves.

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, teaching it to this machine. There were other people around the world doing the same thing—not lots, but plenty. I was treating this thing as an undergraduate at the time. It was 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?” It was just about possible. The thing was learning at the same rate as our students at the time.

Three years later, we could step back and say, “Well, actually, you do basically know most of the things we teach our undergraduates.” That was when I fell in love with it, because I’d 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 aren’t quite fully formed. There are ideas that sort of work, or work in some cases, and we need to think about how these ideas should mature and 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 that are really well understood and exist in the correct generality. We want polished mathematics. We can teach things that are still a bit chaotic to the software, but we don’t necessarily want to add them to the library. The library wants to take fully formed, well-thought-out, beautiful conceptual ideas that know their place.

Essentially, all of the library now is well-thought-out, beautiful ideas. Some of the things in the library are from the last few years, but a lot of it is more basic stuff that we feel we understand well, because that’s when you want to commit. This is part of the work of our community: trying to understand what humans have done and get it into the most abstract, most useful form for future work. You don’t want to put some concept in the library, then have it get generalized and simplified, and somehow need to rework the entire thing. We try to avoid that. We like to get things right the first time. Occasionally, we’ve had to change a fundamental definition, and that can be a huge amount of work because many thousands of files then break and need to be fixed.

11. The perfectoid-spaces stunt

Kevin Buzzard has the instincts of a showman. He’s a natural marketer, and he comes up with a couple of schemes, or stunts, for doing this. One of them is to formalize a mathematical object called schemes in algebraic geometry, which comes from Alexander Grothendieck 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 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. Right? Sixty or 80 years old. I knew this when I was in graduate school. This is not frontier math.” Kevin says, “Okay, that’s true. What is frontier math?” In this period, around 2018, frontier math is this object called perfectoid spaces, created by a German mathematician named Peter Scholze, who was then, and is today, considered maybe the greatest living mathematician.

Perfectoid spaces are truly state-of-the-art objects in math. 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.” So he, Patrick Massot, and Johan Commelin start this effort, just the three of them, to create a blueprint—a kind of guide to the things they would need to define in Lean in order to write the definition of a perfectoid space. It’s essentially a punch list, like a construction project: “We would need you to define this and this and this and this, and ultimately we get perfectoid spaces.”

They succeed at that. An important point to emphasize is that mathlib is all 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’ve got all of first-year graduate-level math. Then there are these extreme spikes from graduate math to the far frontier of the field, which is extremely far from graduate-school math.

Perfectoid spaces is one of the first examples of this: We have this foundation, and now we’re going to build this narrow skyscraper to the frontier. Perfectoid spaces is the first example of that. The stunt works the way Buzzard hopes it will. It captures a lot of people’s attention, boosts Lean’s profile, and starts to convince people. It starts the process described in the book of convincing people that Lean can be used for real math.

So I was just beginning. This was back in 2017. I was having this midlife crisis and trying to work out what was going on in the area of computer theorem proving. 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 2 years’ time. 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. 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 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: formalizing modern mathematics, perhaps all of modern mathematics. One of the things he suggested was that perhaps it was time we got mathematicians not to learn enough about these computer theorem-proving languages to type in all their proofs, but just to literally type in the statements of their theorems. That’s a much easier job, just saying, “Okay.”

I claim that I proved this, and here’s what it looks like in English. But here’s what the statement of the theorem looks like in a formal language. The proof is 100 pages long, and translating it into this language would be like a PhD thesis worth of work—a gigantic problem.

Perhaps we should start persuading mathematicians to state what they’re doing in this formal language, because then there’s no ambiguity. You would imagine that mathematics was this sort of perfect language where everything could be expressed in a completely unambiguous way. But in practice, that’s not what happens.

You read Section 3 of a paper, and it says, “From this point, p will be a prime number that is at least 5.” Then you read something in Section 7, and it’s just talking about a number called p. From reading lots of number theory papers, you know that p will be a prime number. But the fact that p is at least 5 was slipped into Section 3. If you start reading in Section 7, you don’t notice that hypothesis, and so it looks like the theorem says something else. The theorem is correctly stated if you read the whole paper, but if you’re just trying to work out what’s going on in Section 7, you might make an error.

Hales was saying, “We need to fix these errors. We’ve got tools that can do this now.” I just thought that was a great idea. I was 2 weeks in, and I’d realized that the systems knew nothing. But the idea of teaching the systems basic mathematical definitions seemed much more viable than teaching them 100-page proofs of theorems, because many mathematical definitions are quite short.

That was what the library looked like in 2017. It contained some definitions that undergraduates find quite difficult in their second and third years: fancy things like topological spaces, category theory, and rings. But writing down the definition takes only a few lines of code in the computer. Proving all the theorems about it is where all the work is. So if you can just write down the definitions, then we can start stating the theorems. This seemed to me like a viable way to move forward while engaging with interesting material.

My idea was, “Let’s check these modern papers,” which seemed completely impossible. Hales’s idea was viable. In fact, it wasn’t quite viable at that moment. Hales pushed for it to happen in 2017, but it was somehow too difficult then. Seven years later, I wrote a grant proposal to do exactly what Hales had suggested, and we’ve spent a year working on it. Now it’s becoming viable.

We’re taking theorems published in a top pure math journal this decade and trying to translate just the statements of the theorems into the language of the software. We’re 20 percent through, which is some indication that this dream is slowly becoming a reality. I would imagine that in a year’s time, we’ll be far more than 20 percent through. Hales had these ideas that took years to become real, but now they’re coming to fruition. I’d say Hales gave 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 have to be explained to the computer so it can verify them.

There are a few moments in the book where a mathematician is reading a proof written informally in a PDF and wants to formalize it and incorporate it into Lean. What they discover is that often the most trivial statements—the ones that are most obviously true to humans—are the hardest to convince Lean are correct.

Things like “1 + 1 = 2.” Kevin Buzzard confronts the difficulty of formalizing simple statements in the first few weeks he’s using Lean. He wants to convince the program that 1 + 1 is 2, and that’s a hard thing to do. How would you convince me that 1 + 1 is 2? We all know it’s correct, but once you start to think about how you would convince someone who isn’t already convinced, it’s hard.

Much later, when Terry Tao is formalizing some of his own work in Lean, he confronts a similarly elementary fact that’s obvious on its surface to mathematicians, but difficult to convince Lean is correct. There are lots of steps in writing math in this formal language that become tedious and difficult.

One of Leonardo de Moura’s ideas for Lean was to have little helper programs called tactics that would automate some of those repeated steps. Instead of having to explain to Lean why 1 + 1 is 2, you can invoke a certain tactic that proves those types of arithmetic equalities. Then you don’t have to do it yourself.

Leo builds out the capability by writing specific tactics that are useful for Lean. He also builds out the capability for people in the community—Lean users—to write their own tactics. That becomes one way Lean grows much more powerful, and the pain of writing proofs in Lean starts to diminish.

12. Scholze's proof nobody had read: Liquid Tensor

Scholze was the mathematician others turned to when they needed their proofs checked.

In November 2020, I was contacted by the Fields Medalist Peter Scholze. This was back when the library had just basically graduated, in some sense. It knew a lot of undergraduate-level mathematics, but not too much else. Scholze asked me if I’d carefully read his latest preprint.

The answer was absolutely. We’d had a study group on it at my university—a London-wide study group, with people from other universities in London. We’d meet every week and spend 2 hours reading another section of the paper. During the term before Peter got in touch with me, we’d read the entire paper.

I said, “Yes, we’ve looked at it. Very interesting—congratulations.” Then he asked specifically whether I’d carefully read the proof of, I think, Theorem 8.4, one of the theorems in the paper. I went back and looked at the paper, which was a big paper. We had not read the details. We’d read the statement of the theorem and understood what it was trying to say, its point, and where it fitted into the grand scheme of things. The proof was 6 pages of technical calculations that we’d skimmed through at best. You get the general idea of what’s going on, but we hadn’t read the details at all.

I emailed him back and said we’d looked at it, but hadn’t read the details. He said, “That’s what everybody says.” He’d asked people at Princeton and Harvard, and that’s what everybody said. He’d become convinced that nobody had actually read his work; people had skimmed over it. Of course, the devil is in the details in mathematics.

He said that the material looked technical, but a lot of it was undergraduate-level material. Maybe it would be possible for my system to check it. I thought that would be a great test. All we had was undergraduate-level stuff, and all of a sudden I had 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—and taught it to the machine. We got a certain amount of traction, and people were beginning to notice that the software could handle more complex material.

This was a complex proof of a complex theorem. It was only 6 pages long, but the community was small. We wondered whether it would be feasible to plow through those 6 pages. I asked various people, and they said, “Well, could we make this email public?”

I asked Peter if he’d write a blog post for my blog. I’d started a blog promoting the software, so Peter wrote a blog post putting this forward as a challenge. Then people started popping up in the community saying, “Actually, I’d be prepared to spend a substantial amount of time doing this.” At the time, we imagined it would take about a year’s worth of work.

Then we started reading the material. We were really the first people to read it—possibly the first people not to skim through it. We went through it with a fine-tooth comb, and we found a simplification.

Johan Commelin in particular found a simplification. That cut the time down by a factor of 2, to 6 months. Six months later, we’d checked the key thing Peter was worried about: that the proof might be wrong. Peter said, “No, I think it’s right. My co-author, Dustin Clausen, thinks it’s right. No one else has read it. Maybe it’s wrong.”

Six months later, we’d read it through with him. He was like, “It’s okay. It’s right. The machine says it’s right.” Peter got very excited. It was like, okay, these systems are actually useful because they taught me something about how the proof works. We’d found a more conceptual argument for part of it, and something had finally read it.

So we got excited and wrote a second blog post, which went viral in the community. The next thing we knew, Quanta was on the story, and Nature was calling me up. At that point, I realized we’d arrived: the big-league people were taking an interest. Then, once we had some visibility, more and more people started coming into the community—professional mathematicians asking, “Can we do some stuff in my area?”

An expert would come along, and their first question would be, “Can we do my latest theorem?” The answer was no, but we could do the basics in their area, and show them where to start. The library started growing much more quickly. The other thing that happened around that time was COVID. People were stuck at home, and playing computer games while simultaneously engaging with interesting mathematics was a very appealing way for some mathematicians to spend their time. There was a big jump in the rate of growth of the library.

13. Can AI learn to find proofs? AlphaProof

When you have a mathematical proof in Lean fully spelled out, you can click into its elements, investigate them, and see how different parts of an argument relate to each other. This ability to interact with the proof is something Lean provides that a static PDF does not. Could that same machinery teach an AI to find proofs? I was recently talking with some mathematicians at a book launch party for Proof in the Code.

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 gave it the basic axioms. The question was whether an LLM would rediscover human mathematics, or how far along it would get. The consensus among the 3 mathematicians I was talking with was that it would not necessarily discover more than the rational numbers. Starting from the rational numbers, almost at the very beginning of human mathematical understanding, they expected computer mathematics to diverge from what humans have discovered.

I think the reason is that we have a feel for the right abstractions: satisfying concepts and definitions that feel right, complete, and expansive in the work they can do when you start applying them in different scenarios. I think you’re right that a computer searching for things that are correct in some strict, concrete sense would not be guided by those same values. It would not stumble on the same mathematical concepts that have ultimately become meaningful to us. When you’re working on a proof, there are intermediate phases where you look at the whole thing and think, “Oh, this is wrong, but it felt right.” I don’t think that’s just a weird artifact of the process of reasoning about mathematics. The idea that it felt right is probably native to cognition.

So, in your book, you told the story of AlphaProof. This was back in 2024, and they 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. Tell us the story of AlphaProof.

Very early on, there was an interest in using AI to do mathematics. Can AI solve math problems? It’s 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 an AI system can solve a problem, receive a signal about whether it did it correctly, do that very quickly, iterate a lot, and get much better.

You then need to identify targets in math to set your AI against. Early on, one target that was established was the International Mathematical Olympiad, the premier pre-college math competition in the world. High-school-age students solve problems that only require high-school math, but the questions are extraordinarily sophisticated. Early on, the goal became to see whether AI could achieve a gold-medal-level score on the International Mathematical Olympiad.

Google DeepMind picked up this quest. In the book, I talk about the 2024 IMO, where DeepMind designed a system called AlphaProof, based on the same architecture as AlphaGo from almost a decade earlier. They set it to work on the IMO, training it to answer competition-math-level problems, starting with basic middle-school-level problems. They used reinforcement learning to climb toward IMO-level problems, and then essentially administered the 2024 exam to AlphaProof.

They received the questions after the competitors had finished their work, because there was concern about the machine upstaging the human participants. AlphaProof had more time than the human competitors and massive amounts of compute. Ultimately, it got a silver-medal-level score. It solved the problems by outputting Lean proofs and then using Lean to verify them. DeepMind used Lean in both the reinforcement-learning stages and the actual problem-solving stages of 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, and formalizing each one by hand would create an impossible bottleneck. 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 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.

14. AI mathematics in 2026 and Tao's experiment

By September 2026, AI systems were tackling open research problems. In Epoch AI’s fixed-budget test, a pre-release OpenAI model proved Erdős problem 126 and disproved problem 74 by finding a counterexample. Both results were checked in Lean. It resolved 2 of 68 problems; the other 4 models resolved none. 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. 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 4.

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. 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 Baez, an expert in cohomology who had initially called the project a colossal waste of time, admitted 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.

15. Lean's place in AI mathematics

Google’s result was officially graded by the IMO, and OpenAI’s was evaluated separately. Neither relied on Lean to verify those competition answers. Does that in any way negate the need for this kind of verification, now that we have proofs written in natural language?

I think it’s clearly going to be elements of both. Lean and reinforcement learning in that environment are going to create these engines; that’s going to be essential for model training. I think it’s also extremely useful for exploring a wide variety of possible proofs. That’s kind of the value of an LLM: it can output millions of potential proofs, but you need to quickly sort through them to find the ones that are plausible or correct. Lean can tell you which ones those are.

16. AI brute force versus the right abstraction

At the same time, the expressive power of the models is getting so much better that you don’t need everything to be output 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. 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.

What seems to be happening now is that you can have an AI tool that sees something in a book, doesn’t think about it at all, and blindly translates that human-written mathematics into Lean, the language the software uses. It doesn’t really care about making things easy. If it becomes grueling to bash through this stuff without working at the level of generality it should, things get 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.”

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 wanted to change a fundamental definition in the library now, AI would be great at that. It would fiddle around in the repo, break everything, and then plow through and fix everything. Now that we have these new tools, one can question this fundamental design principle: Do we have to find the right level of generality?

The Mathlib maintainers, who maintain this fundamental math library that everything is building on, are still absolutely of the opinion that, to get into our library, something needs to be conceptually the right way of doing things. But there are, of course, plenty of other developments in mathematics now. This wasn’t true 5 years ago. The largest amount of Lean code in the world—or at least the largest amount of publicly available Lean code—was Lean’s math library. That’s probably still just about the case, but in a year’s time, there will be AI-developed libraries that are much more poorly thought out in those terms.

Somehow, trying to make things 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, without really thinking about whether it’s all done at the correct level of generality. The world is changing, and it’s not entirely clear that it’s going to be better. It’s just going to be different.

17. Autoformalisation's Trojan horse

And do you think LLMs could actually help folks use things like Lean? If the problem with Lean is just understanding how the language works and knowing what primitives to use, could it make that better?

There are 2 ways. First, as I mentioned, 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 code it the way you would write JavaScript. There’s an understanding that AI will make writing Lean code a lot easier and probably help bring more mathematicians into using the program. There’s enthusiasm about that.

Second, you need this library of digital mathematics, Mathlib. 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 into Lean code. This is the process of autoformalization. In May 2025, there was hope that autoformalization would 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, and it’s going to come out in Europe later this month—is that autoformalization is now happening. You can now give an LLM a math paper, and it can spit out the Lean code version in a fraction of the time it would have taken a team of humans to do the same thing. The Mathlib community finds that there’s a bit of a Trojan horse: there’s a downside to LLM autoformalization. You end up with a profusion of Lean mathematics that isn’t always defined with the precision and economy you want for canonical objects in Mathlib.

They’re confronting, in a certain way, the same challenge that the rest of the world is confronting: the volume of AI-generated everything. In this case, Lean code you might admit to Mathlib isn’t always at the standard the community itself wants, and they have to figure out how to sift through all this new material.

18. The formalisation gap

We have a real, serious problem now with the spaghetti monster. We’re writing code that we no longer understand. We don’t understand our codebases anymore, and we need some way of building specifications that 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 this math—that understand 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, when reading recent mathematical papers, we see that there’s a certain amount of people speaking to other experts and just knowing that experts understand what humans mean. Sometimes what ends up on paper is 99% representative of what humans mean by mathematics, but not 100%. A few years ago, I wouldn’t have said that. I would have said humans are excellent, humans are perfect; the experts write down exactly what they mean at all times.

But I’ve been doing this project of carefully—so I’ll tell you a story. This is a story that hasn’t been made public yet, but I’ll tell you. We wrote down the statements of 50 theorems from this top pure-maths journal, the Annals of Mathematics. We’re going to make them public this week, but before we did, we ran them through an AI and asked it to check them.

The AI found errors, and the errors were of 2 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. They were slips. The humans hadn’t bothered to mention that, obviously, n had to be at least 3, or that this set should be nonempty.

These were Fields Medalists, right? We found that 4 Fields Medalists had proved theorems in the Annals of Mathematics where, if you actually read the statement of the theorem, strictly speaking, it wasn’t true. What they’d written was false, and in fact, obviously not true. If you’re an expert in the area, you would say, “Well, obviously, they mean this.”

I think this is quite humbling. As a community, we should take a look and step back and think: 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 about 99% capacity. One of the things machines will offer 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?” Then the human will say, “Well, obviously not. Everybody knows that we mean this.” But why don’t we just write that down now? This is one of the ways in which the software is making mathematics better.

19. A proof is not understanding

It’s getting you from 99% to 100%. Humans are not as smart as we think we are. In the early days of interactive proof assistants, as I said, the argument was that we need these because they’re going to check correctness and get the details right. That got no traction in the mathematics community. Mathematicians pushed back and said, “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.”

You come up with ideas, and when you go to formalize or prove them, that’s where the mathematics just dies. You have to do it. You have to check carefully. But that’s not what we really care about. We care about the ideas. Often, the ideas are about coming up with new representations, ways of thinking about things that will let you solve harder problems and get further.

That said, one of the things that characterizes mathematics is its level of rigor and precision: the fact that we can come to a consensus about whether a proof is correct or not. That’s a matter of checking the details and the rules at the bottom. The way I like to think about it is that mathematics, and that level of precision and rigor, is the medium. It’s the language in which mathematicians work.

Within that medium, you have a platform on which to build these incredibly creative ideas, modes of representation, and understandings. What we really love are the ideas, but they’re couched in a framework where we can be very precise.

And 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, around 2000, after Kevin Buzzard started blogging and his blog went viral, a lot of very talented mathematicians came to the subject and got really excited about formalization.

I think what they liked about it was that when you go back to a piece of mathematics you think you understood, but now have to represent it formally in a way that the computer can understand and check in every detail, you find yourself getting very efficient about how you represent concepts and put them together.

Especially when you’re building a library with lots of moving parts that you want to interact, you start thinking about what computer scientists call APIs. You have information, and you encapsulate things and expose things. You think about what kind of information you’re making public for other people using it, and what the internals are.

I think mathematicians found it useful to think about mathematics in this kind of software-engineering way: What are the different modules? What are the pieces? How do they interact? What are the interfaces? They found that this gave them a way of coming back and understanding the mathematics in new and interesting ways.

It’s really just exploring the structure of mathematics and how the pieces get put together. We build up these very complex edifices on top of very precise rules, and understanding how you get that level of complexity down to the very simple rules at the bottom is remarkable.

Alongside concrete, tactical discussions about the projects, Commelin and Scholze debated philosophical aspects of formalization. Commelin saw Lean as a better way to work. Scholze did not. These different orientations came through in Commelin and Scholze’s Zulip exchanges about what it meant to write definitions in mathematics.

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 equip the field with new tools and perspectives.

Scholze worried that if the definitions were wrong in Lean, nobody could tell. Lean might verify that a proof was 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 Commelin and Topaz looked for another form of reassurance. They created a file of concrete examples: unit tests for the most important definitions. If the definitions yielded objects that looked like a duck and quacked like a duck, perhaps they really were defining a duck.

The examples were not watertight evidence, but Commelin thought they were at least as reliable as reading definitions in a mathematical paper, perhaps even more so, given how easy it is for mathematicians to see what they expect to see when reviewing one another’s work.

20. Integration hell and the zlib specification

And the choice is rarely 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.

I remember there was a bit in Kevin’s book where he said that at some point you just kicked a load of people off the Zulip channel. You said, “Look, I just need to focus now,” because it was getting ridiculous. “I was trying to build something that works.”

Some people were there in this channel having fun, throwing ideas at the wall. It’s cheap to throw ideas at the wall, and the other side has to keep telling you, “No, this doesn’t work.”

One frustrating scenario for me is when you throw out an idea without spending 5 minutes thinking about it. Then I find a hole and send it back to you. You polish it a little and send it back. Now it takes 10 minutes to find the next hole. It keeps taking exponentially longer to find the holes in the half-baked idea.

For the person coming up with the ideas, it’s fun, but it’s not fun for the receiver. You have to do your work now. You spend time telling people why this isn’t a good idea and why it’s not the time to do it.

So we should come up with a concrete example here. Apparently, Kim Morrison used Claude agents to produce a Lean implementation of the compression format zlib and prove some specific properties of it. What exactly did they manage to prove?

The AI managed to translate the code from C to Lean, then kept fixing the Lean implementation until it passed the test suite that comes with the C version. It proves that for any compression level and any data, if you compress the data and then decompress it, you get the original data back.

I liken it to the blind men and the elephant: you have all these blind men feeling different parts of the elephant. They understand parts of it, but they don’t understand the whole. I don’t know whether it’s the same thing with zlib, whether it actually encompasses the whole or just some perspective of it.

I suppose the problem when you only have a perspective of a bigger, complex whole is that you get problems with reward hacking, Goodhart’s law, and all kinds of degenerate behavior that can happen if you optimize only part of a system. Is that part of the story here? What was it actually encompassing—the whole zlib algorithm?

Yes. For example, one way to reward-hack this compression-decompression task would be if the only property we asked the AI to show was that it achieved the goal. The AI could hack it by making compression just return the data. It’s the identity function. Decompression returns it back, and you prove the property.

But then you can add more properties, like saying the outputs should be smaller than the inputs. You should also tell the AI, “You have to show that you compress as much as the Rust implementation in the test suite.”

You’re completely right: it’s really easy to give properties that don’t cover the whole thing. If you see AI as an assistant to you, and you’re in the loop looking at the code, I don’t think the problem you raised is super concerning. But once you let the AI go wild and you don’t even want to look at the code, it’s really important to cover all aspects.

Otherwise, you can have an implementation that satisfies all your properties, but you haven’t fully specified what you wanted. You’re not really getting what you want.

21. Verification in the AI software lifecycle

There’s some skepticism that formal verification is going to be broadly useful for verifying the correctness of all this AI-generated code, precisely for that reason. There’s just no way to write specifications for programs that operate at the level of complexity of most programs.

How do you see this panning out in the future with agentic engineering? Do you think we’ll come up with specifications, systems of constraints, new ways of working, new ways of engineering to essentially solve this divergence problem? I guess you could call it understanding debt, right? There’s this problem of building things we no longer understand.

We can’t verify them. 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 AI itself makes software verification much more powerful because you can use AI to write the specifications. 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 life cycle. There are places like Harmonic that believe if you can train an AI model to write math proofs, that same intelligence will be useful for writing proofs about software and verifying the output of LLMs.

I don’t know. That kind of bet is underway. Whether or not it pans out, I don’t know.

22. The human story behind Lean

Underneath all of this software was a very human story of fractious relationships, innovation, and incredible persistence. It has led to something that has revolutionized the world of mathematics and continues to do so every day.

AI is coming for mathematics. That’s absolutely clear. What it’s going to do to mathematics, nobody really knows. All we know is that it’s getting really good, really quickly, and no one understands how much better it’s going to get. Mathematicians have had various reactions to this, ranging from what could only be described as grief—that the subject is changing and they’re going to have to adapt or die—to excitement. 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.

The thing you have to remember is that it’s at its worst today. 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 it will be this time next year. 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, more theorems proved, and a better overview of what mathematics is. We’ll have great tools to explore new dark corners, enlighten them, and enlighten our community.

What makes our goals special is that they’re ours. They are goals. You and I are having this conversation, and the conversation is: What should we do? What should we make of AI, and how should we respond to it? What should we do with AI? I’m happy to let AI have its own discussion on the side about what its goals are and what it should be trying to do. That doesn’t interest me. You tell me there’s some server in the corner doing whatever it’s doing and proving theorems. What I care about is how I’m going to interact with it.

So, yeah, it’s not that I don’t know. The questions I think we should be interested in are: What are our goals, and what should we be doing to achieve them? I don’t know. It’s anthropocentrism only in that that’s what we are. I think we should be at the center of the debate because we’re the ones having it. Insofar as it’s our debate, we can’t help but make it about what we want.

Once I started writing the book, I spent a lot of time with Leonardo de Moura. That was the first moment when I understood, in a certain way, the significance of what I was doing—not for the world, but as a kind of ethical contract between me and the sources. This was Leo’s life’s 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 it started to feel extremely important to tell the story well.

I was contacted by a guy called Kevin Hartnett, who at the time worked for Quanta Magazine and wanted to run a piece on Lean and its mathematics library for Quanta. I ran into Kevin around then, and we became friends. He interviewed me several times about several things, then later decided this was such an interesting story that it was worth writing a book about. I thought that was quite an interesting decision, but he went for it.

During that time, he interviewed me many more times and tried to get some idea of how it happened. He wanted to put together the people behind the story and what was going on. 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 Kevin decided to tell.

As I met more and more figures in the book, more mathematicians, I similarly understood how important it was to them. I spent a lot of time with the six or seven key sources for the book. It was also very useful that this group of people left a tremendous digital record of their work. They were initially very active over email and shared a large number of their private emails with me.

They later migrated to a chat platform called Zulip, where they conducted a lot of their work in public threads and private DMs, which they shared with me. I was able to reconstruct a lot of the work as if I were there observing it as it was taking place. That was 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 don’t want to air your dirty laundry in public. The thing about the people working on Lean is that it’s just wonderful—it’s like family. Everybody working on the project was young, idealistic, and excited about it. We all felt we were doing something interesting and important. But, like a lot of things with family, sometimes family drives you crazy. You get to the family get-together, and there’s the crazy aunt.

Initially, when Kevin interviewed us, there were bumpy spots along the way and tensions. We didn’t want to dwell on them, so we were very guarded at first when an outside reporter came in. But I think we came to trust Kevin when it became clear he wasn’t looking for good guys and bad guys, an exposé, or a scandal story. He was really trying to tell the story in a way that was respectful to everyone involved.

When that was clear, I think he really spoke to a lot of people, and did a good job of capturing the feel and excitement of working on the project. When there were tensions, he made them come across as what they were: not a matter of good guys and bad guys, but people looking for different things.

There was this experience I had reporting it where, around 2018, Leo went off and built Lean 4 while all the math activity in mathlib continued apace. It never felt like I understood what was going on in those years. It wasn’t clear to me whether Leo was talking to the mathematicians. It was a situation where someone had told you a story that didn’t quite make sense, but you didn’t know why.

Ultimately, what I learned was that there had been a somewhat decisive fracture between Leo and the math community. He was saying, “I’m going to go off on my own and build Lean 4. Please leave me alone,” in so many words. They got the message. They were a little wary of angering this guy whom they admired, and Lean was so important to them.

There were particular personality conflicts that I talk about in the book between Leo and Mario Carneiro. They both have strong visions for what this emerging world should look like. Mario’s vision is for 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 clashed quite a lot, and in certain ways that friction pushed Leo away from the mathematicians during the 2018-to-2022 period.

What was interesting for me was realizing I’d been hearing this story, but it didn’t quite make sense to me and I didn’t know why. Then, almost in a rush, the various figures I was working with said, “Oh, this is what’s going on. Leo was mad and had left the sphere for a little while.” Once you get one person to explain their side of the story, others are more forthcoming about theirs as well. By the end, I felt I had fully understood, at least interpersonally, what was going on with Lean.

23. The birthday walk

If you read the book, there was a period when Leo was frustrated with really all users, but especially the mathematical users. While he was working on Lean 4, he pulled away and needed his distance. Every once in a while, I’d send him an email and get a quick response, but it was clear that he wanted some distance.

That was hard. I missed him because he’s a very good friend, and I missed being able to constantly bounce ideas off him.

And so I contacted him. As the book explains, I was coming to Seattle for the Joint Mathematics Meetings, the big U.S. math meeting every year. Leo arranged the dinner, and other people were in town for the conference. He decided to take the opportunity to bring together advisers for the Lean Focused Research Organization. It wasn’t a birthday dinner; it was really just bringing together people interested in and supporting Lean.

But I told him that my birthday was that week, and he decided to make the dinner coincide with my birthday. I was really looking forward to it. It wasn’t the dinner I was looking forward to, though, but the next day. He took an afternoon off from work, and I took an afternoon off from the conference. We met at Pike Place and just walked and walked and walked.

24. Farewell

It was great talking to him again. We talked about Lean, but we also talked about things that weren’t Lean. For both of us, the last several years have been surreal. We remember the early days of Lean. I can remember when it was just me and some students, and I remember visiting Leo at Microsoft and working on the project. Looking back on all that, it almost seems surreal. It’s very surreal how far we’ve come. Now, Kevin Hartner really brought this story to life. He spent, I think, years researching this story, speaking of all of these guys. So I highly recommend you read Kevin’s book. And until the next time, cheers.