Mathematics Just Changed Forever — Kevin Hartnett

Kevin Hartnett is the author of *The Proof in the Code*. SPONSOR:---Cyber Fund built the Monastery to help founders ship products that were impossible a year ago. Applications for Batch 1 are now open. Apply now: https://cyber.fund---In 1998 Thomas Hales finished a proof of the Kepler conjecture that leaned so heavily on computer code that the Annals of Mathematics could not say whether it was true. That impasse opens Kevin Hartnett's book *The Proof in the Code*, and this documentary. Built around Tim's conversation with Hartnett, the film follows Lean from a side project at Microsoft Research to the system mathematicians now use to check their own field. Leonardo de Moura, Lean's creator, explains why everything rests on a small trusted kernel. Jeremy Avigad recalls the argument over foundations that changed Lean. Kevin Buzzard describes his fear that his corner of mathematics was becoming a house of cards, and Paul Lessard separates a correct proof from a useful one. Mathlib, Peter Scholze's Liquid Tensor challenge and Terence Tao's Equational Theories project all pass through. The second half turns to AI. AlphaProof, natural-language olympiad proofs and autoformalisation sharpen the question the book keeps asking: when a machine produces a proof nobody can read, what has actually been checked? The answer lies in the formalisation gap, the distance between the mathematics people mean and the statement a checker certifies. The film closes on the human story behind the software.---TIMESTAMPS:0:00 Cold open: proof, code and the wrong problem1:50 Kepler's oranges and the proof nobody could check6:54 How mathematicians decide a proof is true9:04 Correct is not the same as useful12:17 Sponsor: Cyber Fund12:53 What Lean is, and the small kernel it trusts15:23 From Microsoft's Z3 to Lean18:22 The argument over Lean's foundations24:52 One researcher versus a growing user base26:16 Kevin Buzzard's house of cards30:43 Mathlib as a barn raising37:16 The perfectoid-spaces stunt47:12 Scholze's proof nobody had read: Liquid Tensor53:20 Can AI learn to find proofs? AlphaProof58:43 AI mathematics in 2026 and Tao's experiment1:01:36 Lean's place in AI mathematics1:02:17 AI brute force versus the right abstraction1:05:19 Autoformalisation's Trojan horse1:07:25 The formalisation gap1:11:45 A proof is not understanding1:16:58 Integration hell and the zlib specification1:21:14 Verification in the AI software lifecycle1:22:38 The human story behind Lean1:31:09 The birthday walk1:33:05 Farewell---REFERENCES:[2:12] Thomas Hales, A proof of the Kepler conjecture (Annals of Mathematics, 2005)https://annals.math.princeton.edu/2005/162-3/p01[2:12] The Flyspeck project (the formal proof of the Kepler conjecture)https://github.com/flyspeck/flyspeck[12:53] Leanhttps://lean-lang.org/[30:43] Mathlibhttps://github.com/leanprover-community/mathlib4[30:43] Kevin Hartnett, "Building the Mathematical Library of the Future" (Quanta Magazine, 2020)https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/[47:12] The Liquid Tensor Experimenthttps://github.com/leanprover-community/lean-liquid[53:20] AlphaProof (Google DeepMind): AI achieves silver-medal standard solving International Mathematical Olympiad problemshttps://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/[59:23] The Equational Theories Project (Terence Tao)https://github.com/teorth/equational_theories[1:18:30] lean-zip (the zlib proof)https://github.com/kim-em/lean-zipFrontierMath Erdős (Epoch AI, 2026)https://epoch.ai/benchmarks/frontiermath-erdosBook: Kevin Hartnett, *The Proof in the Code* (Quanta Books, 2026)https://www.quantabooks.org/books/the-proof-in-the-code/---RESCRIPT: https://app.rescript.info/share/8604a0cd6ea4604a368028a05f4e6be4Support MLST on Patreon: https://www.patreon.com/mlstDiscord: https://discord.gg/HNnAwSduud

Speaker names marked ? are inferred from speaking time and the show’s known hosts — they are not voice-verified.

• 0:02Tim Scarfe?

  Now for a quick message from Anthropic, the team behind Claude, the AI built for businesses. Imagination doesn't need permission, just room to play. Claude is an AI that works alongside you to give your ideas the space they need to grow. And then it helps you make them real and ready to ship. Discover more with Claude at claude.ai/span.

• 0:30Speaker 01

  Buy smart, drive for less and trade for more. That's Toyota Fortability. And it starts with a great deal on an all-wheel-drive Camry, Corolla Cross or Corolla Sedan with the latest features in tech. Or test drive a spacious Grand Highlander or adventure-ready RAV4. And with so many hybrid models available, you can enjoy longer trips without all the stops. While Toyota's legendary resale value means you could get more at TradeIn. Get a great deal today and a great value tomorrow. Shop toyota.com for deals and details. Toyota, let's go places.

• 1:01Speaker 02

  The Fields Medalist Peter Scholz, 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.

• 1:28Speaker 03

  When you prove something using a tool like Lean, you can get certificates. You have an algorithm, then can check whether the proof is correct or not.

• 1:38Speaker 02

  The machine says it's right. And something has now actually finally read it.

• 1:44Speaker 02

  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.

• 2:05Speaker 04

  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.

• 2:13Speaker 05

  And 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.

• 2:24Tim Scarfe?

  But a checked proof can still be a proof of the wrong thing.

• 2:30Tim Scarfe?

  It's about the ideas. It's about the understanding.

• 2:33Speaker 06

  You know, here's the GitHub repo. Read it if you want, kind of thing. Does anyone want that? You multiply two numbers on a calculator, you get a result. You just take the calculator's word for it. Nobody's going to check it.

• 2:50Tim Scarfe?

  400 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,

• 3:31Tim Scarfe?

  they reduced it to 1762 combinations. Now, back in these days, computers were incredibly slow. So almost on a case-by-case basis, they had to write this insanely optimized computer program with lots of heuristics, doing intersection checking and so on, to individually prove that each one was less than about 0.74, which is the ratio of the optimum pyramid placement. Kevin Hartnett tells this story in his brand-new book, Proof in the Code. Now, the book isn't just about oranges and Kepler's conjecture, but that's certainly where it starts. But the thrust of the book is mostly about this gentleman called Leo Demora,

• 4:15Tim Scarfe?

  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 Hales, he actually had a bit of paper on his wall. And every single one represented one of these configurations. And they became harder and harder as the density converged towards 0.74. And it took him many, many, many years to do this. And eventually, he did it. So he had 1767 computer programs for every single configuration of these balls. And he was elated. So he published his work to the Annals of Mathematics, expecting a celebration

• 4:59Tim Scarfe?

  that he had just proven Kepler's conjecture. Unfortunately, that's not what happened.

• 5:05Speaker 05

  He dumps this proof on the editors of the Annals of Mathematics, the most prestigious journal in the field. And they essentially don't know how to referee it, how to kind of send it out to other mathematicians to verify its correctness. And it languishes for like many years without actually being kind of determined true or false.

• 5:23Tim Scarfe?

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

• 5:52Speaker 02

  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.

• 6:01Tim Scarfe?

  Every part of the proof that reviewers looked at seemed correct. But the proof as a whole was such a sprawling edifice of calculations, buried deep in computer code. And it was hard to determine how they all hung together and whether in the end they yielded the proof Hales claimed they did. When Hales had finished the proof in the summer of 1998, he had imagined he would use the methods he had developed for Kepler to attack other similar problems. That's how it goes in math. Methods that solve one hard problem are generally good for solving others. Yet, as the review process dragged on without resolution, Hales changed his mind. He couldn't get the math community

• 6:45Tim Scarfe?

  to verify his proof of Kepler's conjecture. Why would he cause frustration by applying the same methods to other problems?

• 6:54Speaker 02

  This is Leo Demora, the creator of Lean.

• 6:58Speaker 03

  The paper was accepted with disclaimer saying something like a 99% confidence this proof is correct. But then Tom starts using proof assistants. This all happened before Lean. He uses Hallite and Isabelle to do this work. But it was a milestone. I mean, it was a big result that has been formalized in proof assistants. And Tom was famous twice for solving the Kepler conjecture and for using a proof assistant, right? In our paper that the math community cares. And the fact that he decided to do the next project using Lean was a big deal on him.

• 7:41Speaker 02

  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.

• 7:54Speaker 05

  So how do mathematicians know when a proof is correct, when they can trust a new theorem and then use that as an input into additional proofs? It's very much a social process. They kind of have a general understanding for what works already. They kind of like know the person behind a proof. They can kind of like trust that this person kind of understands the way things should go. And then they, you know, they can check a proof. They can check the kind of the lines in the argument. But they don't necessarily check every last line all the time. And for the most part, that works, especially when proofs are kind of close to the existing body of knowledge, when they kind of go just incrementally beyond things we already understand to be true.

• 8:33Speaker 02

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

• 8:40Speaker 03

  Well, I think the main thing is that we can. When you prove something using a tool like Lean, you can get certificates. 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'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 even with high schoolers. And they can contribute to my project. I don't need to check if their proofs are correct or not. A big math project, you can view as engineering projects. I mean, Johann Komele, for example, he's a...

• 9:24Speaker 03

  Really hardcore mathematician and he, he is a software engineer. He doesn't know, but he's a software engineer. He breaks big projects in smaller pieces and people can feel the smaller piece. He's like the architect of the, the project and people start feeling the holes and he doesn't need to check manually, right? Of course, he will look later for, to see if 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.

• 10:04Tim Scarfe?

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

• 10:10Speaker 04

  We want provenance. We want to know why, right? And that's the thing that I'm much more interested with. If you want to talk about symbolic AI, the thing that's interesting is I don't want merely things that don't get it wrong. Cause like, that's still not enough. I want to know why it comes up with a particular answer. I want the reason.

• 10:27Tim Scarfe?

  Thomas Hales's proof was extremely verbose. It was complex. He was going through on an instance by instance basis, and it wasn't very abstract like the proofs that came before. And does that remind you of anything? Yes, if you look at AI proofs now, they have a similar property, right? They are, they look a bit like spaghetti and they're inscrutable to us. And that doesn't give us a very satisfying feeling. So can we say that they are still legitimate? Are they still as good as the abstract versions?

• 10:57Speaker 05

  Well, it's not less legitimate because he settled the question. I think one thing that, one way in which you can kind of like assess the value of a new mathematical result is it like, does it enable additional results? Do you invent new concepts, new abstractions, new definitions in the process of prosecuting an argument that then have like widespread utility for answering other questions? And in Hales's case, I mean, there were some computational methods that he, that he would have wanted to apply to other problems, but he was not inventing kind of like broadly new mathematics. In a certain sense, the techniques he used were like fairly elementary. He himself kind of acknowledges that. So he was not creating new math in the same way that like Andrew Wiles had to create new math when he solved Fermat's Last Theorem, where he had to like invent some very like

• 11:41Speaker 05

  powerful new concepts that just opened up entirely new branches of the field. So Hales, Hales's proof was not like that.

• 11:48Speaker 04

  There's utility probably in the generation of proofs that are not constrained by our desire for interpretability. But once you talk about like doing actual mathematics, like that's, I'd like, I still like to think that, you know, the human understanding is still center in this. It may not be, but I think those, those are different quests at some point is 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.

• 12:15Speaker 05

  There, there is resistance because mathematicians don't see by and large, or didn't see the value in that type of time investment. So Hales invests 20 person years in formalizing his Kepler conjecture result. And at the end, all he gets out of it is, is assurance that the thing is correct. Now that is like, that's, 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.

• 12:59Speaker 05

  And it's very high, 20 to 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.

• 13:18Tim Scarfe?

  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 million each to participate. Apply now at cyber.fund. Um, folks are new to Lean. What, what is it, what is it all about? What can you do with Lean?

• 13:58Speaker 03

  Oh, Lean is both a programming language and a proof assistant. You can write codes. Lean is actually implemented in Lean itself. But the cool thing is that you can prove properties about your codes. You can state mathematical theorems. You can prove them. You can build a mathematical library like the Lean math lib.

• 14:17Tim Scarfe?

  So in Kevin's book, Proof in the Code, he gives a precise definition of a kernel, which is a component in an interactive theorem prover like Lean. An interactive theorem prover has two basic components, a logical foundation, which determines how ideas are expressed and interact with each other, and a checker program called a kernel, which verifies that programs correctly adhere to the rules of the logical foundation. The kernel answers the first question anyone asks when they learn about an ITP, which is that if the ITP says a proof is correct, how do I know it hasn't made a mistake? The kernel is how?

• 15:00Speaker 03

  We have the notion of a small trust as kernel. Lean is massive, has zillions of bugs, right? But to trust our results in Lean, only to trust the kernel that's much smaller, right?

• 15:16Tim Scarfe?

  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, Cock and Isabelle had all contained bugs in their kernels that allowed users to validate false statements. His answer was independent checking.

• 15:59Tim Scarfe?

  Let users build their own kernels. To make this option realistic, Demora knew he would need to keep the kernel as small and minimalistic as possible, comprising as few lines of code as he could possibly achieve. Among the ITPs already on the market, Demora admired the minimality of H O L Lite, which had a very small kernel. Back in 2006, there was loads of duplicate effort at Microsoft. Some were building their own theorem provers. Some were working on obsolete theorem provers. And it was at that point that Leo decided to start working on Z3.

• 16:38Speaker 05

  Leo built Z3 in order to provide a systematic way of checking that software had no bad pathways. Um, and he could kind of do it in, in the style of a mathematical proof. Like he could kind of prove with Z3 where you construct, you construct a pathway through the software as a series of variables. And you prove that those variables can never take the right combination of values that would make a statement true. And if you prove that it cannot take, the software cannot arrive at that state, that set of variables, then you just have ruled out categorically a bug, at least in this like one particular direction. Leo built Z3 as a way to automatically check different pathways through Microsoft software

• 17:22Speaker 05

  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, 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 like he and his collaborator entered it into these automated theorem prover competitions where all the ATPs from all over the world come together and they're given a bunch of problems in a set amount of time. And whichever ATP can kind of correctly prove true or false for those problems, uh, most accurately wins.

• 18:06Speaker 05

  Z3 was the world champion at. So he essentially had climbed to the top of the automated theorem prover mountain. But he also was dissatisfied with the kind of the fundamental limitations of automated theorem prover technology. Like there's just kind of a limited range of things that, uh, 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 are kind of just a wider range of truths. You can try to encode and verify and interactive in the sense that the human, a kind of a

• 18:46Speaker 05

  human user can, um, can nudge the program towards greater expressiveness. Uh, it makes it a much more powerful thing. So what my book is, is ultimately the story of how Lean, this interactive theorem prover that Demora builds to verify the correctness of software programs in a richer way than he could with Z3, gets in a sense, co-opted by mathematicians who see the potential in it. And for the first time, an ITP breaks through into a more mainstream way of working in math.

• 19:12Tim Scarfe?

  But, um, in Lean, because it uses this dependent type theory, it can be used for solving many, many other problems in abstract mathematics, which are significantly more complex. Jeremy Abigail, a mathematician and philosopher at Carnegie Mellon, has been corresponding with Leo for many years. I'm a mathematician by training, specifically a logician. Uh, and so, you know, what I like about logic is that it's somewhere between mathematics, computer science and philosophy. So here at Carnegie Mellon, my primary appointment is in the philosophy department. Proof assistants started just kind of as a hobby, just messing around with them.

• 19:47Speaker 06

  I thought they were interesting around the year 2000, so quite, quite a long time ago.

• 19:52Tim Scarfe?

  Just after midnight on the west coast, Demora sent a long email to the group, softening some of the concerns he had raised. "I apologize if I sounded too negative today. I'm still trying to understand the alternatives," he wrote. "I've been reading about all of these proof assistants and studying their implementations. When I questioned the need for dependent types or any other feature, it's because I'm really impressed with H O L Lite'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.

• 20:33Tim Scarfe?

  "I understand Jeremy's point when he says H O L Lite would be really inconvenient for doing abstract algebra. The design of Lean was being negotiated in real time."

• 20:46Speaker 03

  I want to choose higher order logic, it's a simpler foundation, much easier to implement. And for many software verification tasks, it's enough, right? But for doing abstract mathematics, it's not.

• 21:03Speaker 03

  It's important to have a good library, math library for very fine software, for example, cryptography. We need lots of math, differential privacy is another example. So having a good mathematical library is important, even if you only care about software verification. And in my point of view, you have, it's important to have users. That's what the users wanted, and I want support, I want to have Jeremy as a user. I knew others would come and pay off. I mean, many people, many of my colleagues that work on cryptography, they say, for example, one of them is a former colleague of mine, Cedric Forney, he uses Lean now.

• 21:47Speaker 03

  And he told me, "Look, the math lib, the Lean mathematical library, have the right abstractions I need for very fine cryptography." Right? Because of all the generality that having the dependence type theory provided. We have a library that's more expressive, that has the right abstractions, is cleaner. Yeah, it paid off long, in the long term, it paid off. It was a lot of extra work at the beginning, and to get it right was also a lot of work. But I think it paid off.

• 22:21Tim Scarfe?

  I suppose one of the biggest tensions and ultimately the battle that you won was that you wanted Leo to support this dependent type theory, because that was very useful for solving the types of problems that you were interested in.

• 22:33Speaker 06

  Before starting the Lean project, I had worked in 2009 and 2010. I spent a sabbatical year working on the formalization of the Pythonson theorem. And that is in a proof assistant known as Ruck, and Ruck is based on dependent type theory. Before that, I had worked with Isabel extensively, which is a proof assistant based on a simpler logical framework called simple type theory. Isabel is a wonderful system, and so for many things, it's absolute ideal. It's still, to this day, has excellent automation, automated support. So for certain types of mathematics, it was really a great system. But then for certain types of things, you hit a wall.

• 23:15Speaker 06

  So in modern mathematics, mathematicians talk about algebraic structures, you know, axiomatically characterized. They're really ubiquitous, there are these complex networks of algebraic structures. And simple type theory is just not good for that. And so after my year working with Ruck, it became clear to me that this was the framework that was capable of doing that type of mathematics. And I think other mathematicians who had experimented with Isabel and other systems were coming to similar conclusions, that to do the mathematics that they wanted to do, they needed this very expressive framework. So the thing about dependent type theory is that it's very powerful and very expressive. But I like to quote from, you know, the Spider-Man franchise, you know,

• 23:59Speaker 06

  "With great power comes great responsibility." You know, the very powerful language, it's also very hard to implement. It can be more difficult to use, there are a lot of gotchas and kind of corner cases. And so it was a more weighty and complicated and difficult framework. And when Leo first started the project, he was aiming for simplicity, you know, a very simple, formal, you know, foundation. And so he needed convincing there, that the trade-off was worth it. I think, you know, in the end, he came around, I mean, now he's one of the biggest proponents of dependent type theory. He, you know, you know, soon after, he would say that, you know, it's really beautiful. And so he recognized the benefits. But again, coming, coming from the outside and, you know, without the familiarity,

• 24:44Speaker 06

  yeah, he needed convincing at first.

• 24:45Speaker 05

  But ultimately, Leo emails Jeremy back during that summer of 2013 and tells him, "I've decided to go with dependent type theory." And Jeremy basically does a dance at home in Pittsburgh, because he just knows the seeds are there now for Lean to be useful in math and the way he's always wanted an interactive theorem improver to potentially be useful.

• 25:06Speaker 03

  It's funny, as a developer,

• 25:09Speaker 03

  when you're using the developer hats, usually you want to go to whatever is simpler to implement. And you forget that you sometimes will be the user of this tool too. I always joke, I mean, if I'm using my user hats, I want this feature. If I'm using the developer hats, I don't want it.

• 25:27Speaker 05

  Oh yeah, so Leo is like extremely self-critical. I mean, 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.

• 25:43Tim Scarfe?

  At Microsoft, Leo feared a poor annual rating would jeopardize his research. His manager never gave him one, but the fear persisted.

• 25:52Speaker 05

  Leo is just a researcher, a computer science at Microsoft Research. He's not a project manager, he's not a product manager, and 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

• 26:37Speaker 05

  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 4. But for years, you know, we were at Lean 2. And Leo saw where he wanted it to go, and he felt inhibited in his ability to actually find the time to do it because he was answering all these essentially like user support questions and queries from mathematicians. One of the earliest adopters of Lean and kind of most enthusiastic evangelists for Lean

• 27:21Speaker 05

  is a mathematician at Imperial College in London named Kevin Buzzard.

• 27:25Speaker 02

  My name is Kevin Buzzard, I'm a number theorist working at Imperial College, London. I spent some time, the beginning of this century, bringing up three kids. When that was sort of over and they were able to look after themselves a lot more, I wanted to get back into doing hard research mathematics. And I realized that there was a huge amount of material that I was going to have to sort of catch up on. I had some kind of midlife crisis around that time, because I was trying to read it, and I couldn't understand all of it. And I would find what I thought were mistakes in the literature. Then I started thinking, well, wait a minute, like, what are we, like, what, this is very abstract stuff.

• 28:09Speaker 02

  It's not immediately clear there's any sort of concrete applications. So there's nothing that we can sort of test these things on in reality. And if they're not right, then almost, you know, what is the point of this stuff at all? So I had some kind of crisis, and I started thinking, you know, would it be possible to check mathematics using machines? Because, you know, technology is moving very fast. And so I went down some kind of rabbit hole, just kind of exploring the software that was out there that was claiming, you know, that it could check mathematics at superhuman accuracy. And it absolutely could check mathematics at superhuman accuracy, but the problem was the mathematic, 99% of what it was checking was really, really basic material known hundreds or maybe even thousands of years ago.

• 28:55Speaker 02

  So that, but by that stage, I kind of 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. It's 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, it went out the window. Then I was just like, oh, this software is really great, you know, what can we actually get this software to do? And at the time, it was just like, we could barely get it to do undergraduate level mathematics, but because it was great fun using it, you know, that was how I ended up switching.

• 29:34Tim Scarfe?

  By 2016, Kevin Buzzard had time to return to the P. Attic Landlands program. A young talent named Peter Schultz 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 Schultz'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.

• 30:19Tim Scarfe?

  His critique was not of Schultz'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.

• 30:54Speaker 05

  So to him, that was the draw of Lean, was he wanted to take these papers that had developed in his field, formalize them, like convert them into this computer programming language, determine with complete certainty whether they were correct, and if they weren't, fix them. But if they were, then it would just kind of give him renewed confidence to kind of proceed in research in this area.

• 31:15Tim Scarfe?

  So here's a small example, the ring. Contact it constructs a proof of this algebraic identity using machinery from MathLib. Lean then checks the proof and it says no goals, which means the task is complete.

• 31:29Speaker 05

  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 kind of just like some understanding of mathematical logic. So what you need to do is equip it with a library of definitions. And this is the parallel story in my book. There are kind of two key stories, two dreams almost, that are very dependent on each other, sometimes in tension with each other. So one is Leo's vision for Lean, the software he wants to build. The other is the development of what comes to be called MathLib, a library of digital mathematics, which is spearheaded by several of the main characters in the book. People like Kevin Buzzard, Johan Kamelin, Patrick Masso, Jeremy Avogad is very involved. Mario Carnero is another figure who's very important

• 32:14Speaker 05

  in the development of MathLib. The vision for that is it will be a crowdsourced effort to define in Lean language, basic concepts in math from the ground up. So starting with even just like high school level math to college level math, so that you have the ingredients to then later encode more sophisticated forms of math. That's kind of the, that's how Lean breaks beyond just these combinatorial results like the four color theorem and Kepler's conjecture and becomes a place where you can express very deep kind of frontier level abstract math. It's through the development of MathLib. And actually, I got interested in this story back in 2020, when I was assigned an article for Quantum Magazine

• 32:56Speaker 05

  on the development of MathLib, when it was still quite early days. In that article, I say, I said that MathLib had the spirit of a barn raising. It was just like this like community effort to get this massive thing done without any central authority, no central resources. And so slowly, this library of digital mathematics is created.

• 33:15Speaker 02

  MathLib is Lean's mathematics library. So it was born about the same time that I started working in the field. It was 30,000 lines of code containing a bunch of completely basic theorems about finite sets and some very basic undergraduate level mathematical definitions. And that was it. It didn't even have a definition of the real numbers when I started. Or it just got this concept of the real numbers, which is something known to, you know, known to the ancient Greeks and the Babylonians, you know, there's thousands of years old. And it didn't have the complex numbers, which I guess from about 500 years ago. So there was clearly a lot of work needed doing.

• 34:00Speaker 02

  Yeah, I spent a lot of time teaching, right? That's part of my job. I teach these undergraduates, they come in. And the way it works at university in a mathematics department is you kind of say, okay, you learn all this stuff at school, but actually we're going to start again from the basics and just work through everything quite quickly. And one of the things we teach them is how to define the complex numbers, which are this basic number system that goes back to Descartes. So I kind of thought, oh, this thing doesn't have the complex numbers. Let's teach it the complex numbers. So there we go. We define the complex numbers, prove basic things about it. And it was great. And I made a pull request. You know, this is a free open source math library. So I made a pull request to this math library and then it got merged into the main branch.

• 34:43Speaker 02

  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 I'm now I'm thinking, you know, what, 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 roped the undergraduates in. It was absolutely critical. We just got to the point where all my kids could make their way to school by themselves. They can make their way to and from school. You could leave them in the house and they were unlikely to, you know, set anything on fire or, you know, it'd be illegal. So, so I could stay late at work, like one evening a week, I'd stay late at work and just let the kids muddle on by themselves.

• 35:27Speaker 02

  And, and I would teach undergraduates how to use this software. And then I would get them to start, you know, transcribing what they were learning in their, in their undergraduate degree, just, just teaching it to this machine. So the library just like, I mean, there was lots of other people around the world, well, not lots, but there were plenty of other people around the world doing the same thing. You know, I was treating this thing as an undergraduate at the time. So it's 2017 and the question was, you know, let's just imagine you've enrolled on our degree. You know, can we, can we actually teach you at the same rate as we teach the undergraduates? And it was, it was just about possible. You know, the, the thing was learning at the same rate as other students at the time. But, you know, three years later, we could sort of step back and say,

• 36:11Speaker 02

  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. Because I wanted to teach it.

• 36:19Tim Scarfe?

  But when is a new mathematical idea ready to become part of the library?

• 36:25Speaker 02

  Mathematics is, is an interesting object. It's this gigantic abstract object that humans have created. And at the boundary, there are things that haven't, you know, they're not quite fully formed. There are ideas which sort of sort of work or work in some cases. And, you know, we need to think about how these ideas should mature, what they should really look like. So mathematics needs to mature. Sometimes at the boundary, it's, it's not material that's ideal for the library. You know, what we want in the library is ideas which are really well understood and there's a, exist in the correct generality. You know, we want polished, we want polished mathematics, stuff which is still a bit chaotic.

• 37:08Speaker 02

  You know, one can attempt to teach it to the machine. You know, we can teach it to the software, but we don't necessarily want to add it to the library. The library wants to take sort of fully formed, well thought out, you know, beautiful conceptual ideas, which sort of know their place. Essentially, all of the library now is a, is, is well thought out, beautiful ideas. Some of the things in the library are actually stuff that happened in the last few years. But a lot of it is much more basic stuff that we feel like we understand well. Because that's, you know, that's when you want to commit, right? This is part of the work of our community, trying to understand what humans have done and to get it into the correct, you know, most abstract,

• 37:51Speaker 02

  most useful form for future work. Because you don't really want to put some concept in the library and then it gets generalized and simplified a bit. And then somehow you need to rework the entire thing. This, we try and avoid this. We, we like to get things right first time. Occasionally, we have had to go through and change a fundamental definition. This can be a huge amount of work because then, you know, many thousands of files then break and need to be fixed.

• 38:17Speaker 05

  Kevin Buzzard has like the instincts of a showman. He's like a natural marketer and he comes up with a couple, essentially schemes or stunts for doing this. And one of them actually is to formalize a mathematical object called schemes, which is in algebraic geometry. It 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, type of like frontier math that they themselves care about. He does it and he's met with like a collective yawn because people tell him, Kevin, schemes are old math, right? It's 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.

• 39:02Speaker 05

  What is frontier math? And in this period, around 2018, frontier math is this object called perfectoid spaces, which is something that was created by a German mathematician named Peter Scholze, who is today and then as well considered maybe the greatest living mathematician. Perfectoid spaces are truly state of the art objects in, in math. And Kevin says, all right, if we can formalize them, if we can show Lean is capable, capable of expressing perfectoid spaces, we'll have indisputable proof that it can do anything. And so he and Masso and Kamelin start this effort, just the three of them, to create a blueprint, essentially a kind of a guide to the things

• 39:44Speaker 05

  that we need to define in Lean in order to be able to, in order, in order to be able to write the definition of a perfectoid space. So it's essentially a punch list, like a construction project. You know, we would need to define this and then this and this and this, and ultimately we'd get perfectoid spaces. They succeed at that. And what that, I think, kind of an important point to emphasize is MathLib is all of the math that anyone working in Lean can draw on. At the moment, it's essentially maybe first year graduate level math. They have all of undergraduate math, modulo a few things here and there. They have all of first year graduate level math. Then there are these extreme spikes from grad math to the far frontier of the field, which is like extremely far

• 40:28Speaker 05

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

• 40:59Speaker 02

  So I was just beginning, this was back, back. So back in 2017, I was having this midlife crisis and trying to work out what was going on in the area of computers proving theorems. And I discovered to my amusement that there was a big conference in the area that I was far too late to register for in Cambridge, taking place in two years' time. But this was at the Newton Institute in Cambridge and they were ahead of the game. This is pre-COVID, but they were already recording and live streaming their talks on the internet. So even though I couldn't go to the conference, I could still watch the talks.

• 41:42Speaker 02

  And the first talk was given by Tom and I imagined that he would be by Tom Hales. And I imagined that he would be talking about his proof of the Kepler 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

• 42:27Speaker 02

  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. You see, in reality, you would imagine that maths was this sort of perfect language where everything can be expressed in a completely unambiguous way. But in practice, this is not, this is not what happens. In practice, you read, you read section three of the paper and section three, it says,

• 43:10Speaker 02

  "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, you know, 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.

• 43:54Speaker 02

  Trying to, trying to translate all the, I was two weeks in and I'd realized that the systems knew nothing. But somehow the idea of teaching the system's basic mathematical definitions seemed to be much more viable than teaching it 100-page-long proofs of theorems. Because many mathematical definitions are quite short. In fact, that was what the library looked like in 2017. It contained some definitions that undergraduates find quite difficult. Second year and third year fancy things like topological spaces and Noetherian rings and things like this. But actually, just writing the definition down is only a few lines of code in the computer.

• 44:37Speaker 02

  It's proving all the theorems about it where all the work is. So if you can just write down the definitions, then we can start stating the theorems. And this just seemed to me like a viable way to move forwards whilst engaging with interesting material. So it was just a completely, my idea was just like, let's check these modern papers, remark that's completely impossible. Whereas Hales' idea was viable. In fact, it was somehow not quite viable at that moment. Hales pushed for, 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,

• 45:21Speaker 02

  just to do the same thing. And, and we've spent a year working on this now and it now is sort of, it's becoming viable. We're taking theorems published in the top pure maths journal this decade and we're trying to translate just the statements of the theorems into the language of the software. And yeah, we're 20% through. So that's some indication that at least this dream is slowly becoming a reality. And I would imagine that in a year's time, we're going to be far more than 20% through. So Hales had these ideas which have taken years to become real, but now, you know, now they are becoming.

• 46:04Speaker 02

  So yeah, I would say that Hales was really, you know, this was a visionary talk and now his vision is coming to fruition.

• 46:12Speaker 05

  Formalizing a proof or writing math in this formal language is very kind of tedious. You have to spell out every little detail. Even things that are kind of trivial or obvious to mathematicians, you need to kind of convince the computer of their correctness. There are a few moments in the book where a mathematician is reading a proof, like it's written in formally on a PDF and they want to formalize it, incorporate it, write, they want to formalize it in Lean. And what they discover is often it's the most trivial statements that are most obviously true to humans are the hardest to convince Lean are correct. Things like 1 plus 1 is 2. 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 1 plus 1 is 2.

• 46:57Speaker 05

  That is a hard thing to do. Like, how would you convince me 1 plus 1 is 2? It's like, you know, it's, we all know it's correct, but once you actually start to think about how you would, you know, impress someone who's not, not, it's hard. Terry Tao, much later, when he is formalizing some of his own work in Lean, he confronts a similarly elementary fact that is just, you know, obvious on its surface to mathematicians, but convincing Lean it's correct is difficult. So the point is, there's, there are lots of, lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora's ideas for Lean is it would have these little helper programs called tactics, which will automate some of those repeated steps, those kind of things, steps that happen regularly in proofs.

• 47:42Speaker 05

  Instead of having to explain to Lean why 1 plus 1 is 2, you can invoke a certain tactic that just does those type of arithmetic guarantees that kind of proves equalities, numerical equalities, and then you don't have to do it yourself. So Leo builds out the capability, he writes some specific tactics that are useful for Lean, but he also builds out the capability for people in the community, Lean users, to write their own tactics. That becomes one way in which Lean becomes much more powerful and this pain of writing proofs in Lean starts to diminish.

• 48:12Tim Scarfe?

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

• 48:18Speaker 02

  So in, in November 2020, I was contacted by the Fields Medalist Peter Scholzser. This was back when the library had just basically graduated in some sense. We had sort of, it knew a lot of undergraduate-level mathematics, but not too much else. And Scholzser asked me if I'd read, I'd carefully read his latest pre-print. And the answer to this was, well, absolutely. You know, we'd had a study group on it at my university, a London-wide study group. There were people from other universities in London. We would meet every week and we would read another section from this, spend two hours reading another section from this paper. And during the term, we'd read the entire, we'd read the entire paper.

• 49:01Speaker 02

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

• 49:45Speaker 02

  You know, you get the hang of the general idea of what's going on. So we had not read the details at all. So I emailed him back, said, you know, we looked at it, we didn't read the details. And he said, that's what everybody says. And he'd asked people at 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, but, and of course, the devil is in the details in mathematics. So he said, at the end of the day, this material is, it sort of looks technical, but at the end of the day, a lot of it is undergraduate-level material.

• 50:26Speaker 02

  So maybe it would be possible for your system to check this material. And I thought, that would be a great test, because this is interesting. All we have is undergraduate-level stuff. And all of a sudden, I've got this Fields Medalist suggesting that we could check part of his most recent paper. And, and I was just, you know, part of, at the time, nobody was taking this software seriously. Maybe people were just beginning to take it seriously. The year before, we'd, 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.

• 51:08Speaker 02

  You know, in, people are beginning to notice that the software was able to do more complex material. But this is, you know, this was a complex proof of a complex theorem. It was only, it was only six pages long. But the community at that time was small. So we did wonder.

• 51:28Speaker 02

  We did wonder whether it would be feasible to actually plow through these six pages. And I asked various people and they were just like, well, could we make this email public? So I asked Peter if he would write a blog post for my blog. I'd started a blog that was sort of promoting the software. So Peter wrote a blog post on my blog, putting this as a challenge. And then people started popping up in the community, saying, actually, I'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.

• 52:12Speaker 02

  And we started going through it with a fine tooth comb and we found a simplification. Johann Komolin in particular, found a simplification. And so that cut the time down by a factor of two. And six months later, we'd check the key thing that Peter was, you know, Peter was worried that the thing was wrong. And Peter's like, I think it's right. My co-author thinks it's right, Dustin Claussen. No one else has read it, maybe it's wrong. So six months later, we'd read it through and it was like, it's okay, it's right. The machine says it's right. And Peter got very excited, which is like, okay, so these systems are actually useful. Because they've taught me something about how the proof works. You know, we've, we've found a more conceptual argument of part of it. And, and something has now actually finally read it.

• 52:57Speaker 02

  So we got excited and wrote a second blog post, which then, which then went viral in the community. And the next thing we know, you know, Quanta was on the, you know, and, and nature was calling me up. And so at this point, I realized that we'd arrived. Now the, you know, now the sort of the big league people were taking an interest. And, and then it sort of, you know, it went on from there. Then of course, once, you know, once we had 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, you know, the basics in your area. And so here's where to start. And so the library started growing much more quickly then.

• 53:41Speaker 02

  The other thing, of course, that happened around that time was COVID. So people were sort of stuck at home and playing computer games was sort of an appealing way. You know, playing computer games while simultaneously engaging with interesting mathematics. Was some mathematicians found that a very appealing way to spend their time. So there was a sort of a, a big sort of jump in the, the rate of growth of the library.

• 54:04Speaker 05

  When you have a mathematical proof in Lean, fully spelled out, you can kind of click into elements of it, investigate and see how different parts of an argument really relate to each other. This ability to interact with the proof is something that Lean provides that a static PDF does not.

• 54:21Tim Scarfe?

  And could that same machinery teach an AI to find proofs?

• 54:25Speaker 05

  So I was recently talking with some mathematicians at a book launch party for the proof in the code. And kind of late into the evening, we start talking about whether you could apply the alpha zero approach, the zero knowledge approach to like having an LLM recreate mathematics. If you just give it kind of the basic axioms. Question we were talking about was would an LLM rediscover essentially kind of human mathematics? Or how far along would it get? And there was a, the kind of the consensus among these three mathematicians I was talking with, was that it would not necessarily discover more than the rational numbers. If you were kind of advancing along the kind of the human understanding of math, starting at the rational. It's almost at the very, very beginning. They expected computer math would diverge from kind of what has become, you know, human discovered math.

• 55:09Speaker 05

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

• 55:44Speaker 04

  If you're working on a, on a proof, say, there are a lot of intermediate phases where you go and look at the whole thing. And you're just like, oh, this is wrong, but it felt right. Like, I don't think that's just like a weird artifact of like the reasoning about mathematics process. The idea that it felt right, I think that's probably native to, to cognition.

• 56:01Tim Scarfe?

  So in your book, you, you told the story of Alpha proof. So this was back in 2024 and they actually used Lean as part of that architecture. And it's very interesting in context as well, because the newer versions don't, don't use Lean, possibly not yet. But tell, tell us the story of Alpha proof.

• 56:18Speaker 05

  Very early on, there's this interest in using AI to do mathematics. Can AI solve math problems? It's, it's both kind of just like an obvious like test, because math is, you know, the pinnacle of human thought. If AI can do that, perhaps it can do almost anything. Also, math is a very effective training environment for AI, because you get a clear reward signal at the end. Has it done the problem correctly or not? That enables reinforcement learning, where you can have an AI system solve a problem, receive signal that 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.

• 57:02Speaker 05

  It's the premier pre-college math competition in the world. These are high school age students doing things that only require high school math. Those are the, the problems on the competition, but extraordinarily sophisticated versions of those questions. So early on, it set out, can AI achieve a gold medal level score on the International Math Olympiad? Google DeepMind picks up this quest themselves. In the book, I talk about the 2024 IMO, which is where Google DeepMind designs a system called Alpha proof, 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.

• 57:46Speaker 05

  They do reinforcement learning to like slowly reward climb until it is within range of IMO level problems. And then they essentially administer the 2024 exam to Alpha proof. They receive the questions after the competitors have finished their work to, there's a kind of concern about the machine upstaging the human participants. So it receives the questions after the, the human competitors complete their work. It has more time than the human competitors. It has massive amounts of compute. Ultimately, it gets a silver medal level score. And the way in which it, it solves the problems is by outputting Lean proofs and then using Lean to verify them. DeepMind used Lean in both the, the reinforcement learning stages

• 58:29Speaker 05

  and then the actual problem solving in the competition stages of, for the IMO.

• 58:33Tim Scarfe?

  Alpha proof could not read the problems it was meant to solve. It took statements expressed in Lean and devised proofs in Lean. But competition problems arrive in natural language. DeepMind needed potentially millions of training problems. Formalizing each one by hand would create an impossible bottleneck. So the team had to find a way to translate competition mathematics into Lean automatically. The translation itself had structure. Algebra and number theory were easier because their natural language statements already contained equations and notation. DeepMind eventually auto-formalized about 80% of questions in those areas nearly perfectly. Combinatorics was harder.

• 59:19Tim Scarfe?

  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 Alpha proof's proof search begin. By September 2026, AI systems were tackling open research problems. In Epoch AI's fixed budget test, a pre-release OpenAI model proved Erdos problem 126 and disproved problem 74 by finding a counter example. Both results were checked in Lean.

• 1:00:03Tim Scarfe?

  It resolved two of 68 problems. The other four models resolved none. And on September the 8th, OpenAI also published a claimed resolution of the Navier-Stokes millennium problem alongside a Lean formalization. But unfortunately, not under the best circumstances. But that's outside the scope of this particular video. Back in September 2024, Terence Tao launched Equivalent Theories, an open collaboration mapping which algebraic laws imply others, with Lean checking the results. Within a month, the Equivalent Theories group had narrowed 22 million questions down to 238. By late November, they were down to 138.

• 1:00:49Tim Scarfe?

  By the end of March, they'd been stuck for several weeks on just four. But settling every implication had never really been the goal. Tao viewed Equivalent 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.

• 1:01:33Tim Scarfe?

  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.

• 1:01:46Tim Scarfe?

  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 Tao, that was exactly the point. The project had demonstrated the efficacy of a new kind of mathematical machine. In July 2025, Google DeepMind and OpenAI reported gold-level scores on the International Mathematical Olympiad using natural language proofs. Google's result was officially graded by the IMO, and OpenAI's was separately evaluated.

• 1:02:31Tim Scarfe?

  Neither relied on Lean to verify those competition answers. Does that in any way negate the need for this kind of verification when we now have proofs that are just written in natural language?

• 1:02:44Speaker 05

  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 to be essential for model training. I think it's also extremely useful for exploring a wide variety of possible proofs. I mean, that's kind of the value of an LLM, that it can output millions of potential proofs, but you need to then quickly sort among them to the ones that are plausible or correct. Lean can tell you which ones those are. 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.

• 1:03:19Speaker 02

  So the philosophy of the library has always been find the right abstraction and develop everything in that correct generality. And the advent of AI has been quite interesting because we always firmly believed that finding the right abstraction would just make our lives easier later. And what seems to be happening now is you can have an AI tool which just sees something in a book, doesn't think about it at all, just blindly translates that human-written mathematics into Lean, the language that the software uses,

• 1:04:04Speaker 02

  and doesn't really care about making things easy. If now it becomes kind of grueling to just bash through this stuff in not really the generality it should be working in. Things are much more complicated. And as humans, you don't want to plow through stuff when you kind of, "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. So as an example, if we did want to change a fundamental definition in the library now, AI would be great at that. AI would just fiddle around the roots, break everything, and then it would just plow through and fix everything.

• 1:04:49Speaker 02

  And so now we have these new tools. One can now question this fundamental design principle. Do we have to find the right level of generality? The MATLAB maintainers, this fundamental math library which everything is building on, we are still absolutely of the opinion that to get into our library, it needs to be conceptually the right way of doing things. But there are of course plenty of other developments 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.

• 1:05:34Speaker 02

  But in a year's time, there will be AI-developed libraries that will be much more poorly thought out in those terms because somehow trying to make it easy seems to be less of an issue. If you're prepared to just pour tokens into the problem, then we don't necessarily need to find the correct conceptual way of thinking about these things. We can 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.

• 1:06:20Tim Scarfe?

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

• 1:06:32Speaker 05

  It's in two ways. A, I mentioned that writing the fiddly Lean syntax is a real barrier to entry for mathematicians. Obviously, with agentic coding, you don't need to learn all that Lean. You can just 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, MATLAB. 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.

• 1:07:15Speaker 05

  There is hope in May of 2025 that auto-formalization will dramatically accelerate the rate at which new math is added to MATLAB. 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 MATLAB 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

• 1:08:00Speaker 05

  that is not always defined with exactly the precision, the economy with which you want these canonical objects in MATLAB to be expressed. And so they're kind of confronting in a certain way the same challenge that the rest of the world is confronting everywhere, which is the volume of AI-generated everything. In this case, Lean code, you might admit to MATLAB, 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.

• 1:08:26Tim Scarfe?

  So we have a real serious problem now with the spaghetti monster. 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.

• 1:09:09Speaker 02

  Mathematics is a well-specified formal language. And that's exactly why we can write computer programs that understand what humans mean when they speak in mathematical terms. So mathematics should contain no ambiguities at all.

• 1:09:32Speaker 02

  So in theory, mathematics is completely well-specified and thus perfect for this kind of game, writing it down in a formal system using a computer program. But in practice, reading recent mathematical papers, we do see that there's a certain amount

• 1:09:55Speaker 02

  of people speaking to other experts and just knowing, experts sort of know what humans mean when they say things. So sometimes what ends up on paper is sort of 99%, but not 100% representative of what humans mean by mathematics. And a few years ago, I would not have said that. A few years ago, I would have said, "Humans are excellent, humans are perfect." The experts, they write down 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 story that's not been made public yet, but I'll tell you a story.

• 1:10:37Speaker 02

  So we wrote down the statements of 50 theorems from this top pure maths journal, The Annals of Mathematics. And we're going to make them public this week. But before we made them public, we ran them through an AI and asked an AI to check them. And the AI found errors. And the errors were of two forms. There were errors that my team had made. We had 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.

• 1:11:22Speaker 02

  The humans hadn't bothered to mention that obviously n had to be at least three, or obviously this set should be non-empty. There were things that... And this was Fields Medalists. 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. Strictly speaking, what they've written is false. And it's obviously not true, in fact. If you're an expert in the area, you would say, "Well, obviously, they mean this." So the process of... I think this is quite humbling.

• 1:12:04Speaker 02

  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 which you've written, it isn't actually true, is it?" And then the human will go, "Well, obviously not. Everybody knows that we mean this. But why don't we just write that down now?" So this is one of the ways in which the software is making mathematics better. 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 assistance, like I said...

• 1:12:49Speaker 06

  The arguments that we need these because they're going to 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, isn't about axioms and rules. It's not about checking the details. It's about the ideas. It's about the understanding. And you know, you come up with ideas, you know, when you go to formalize a proof, that's where the mathematics is just dying. I mean, it's just, you gotta do it. You gotta check, you know, you gotta check carefully, but that's not what we really care about. We care about the ideas. And often the ideas, they are about coming up with a new representations, ways of thinking about things that will let you solve harder problems and get further.

• 1:13:27Speaker 06

  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 a proof is correct or not. And that's a matter of checking the details and the rules at the bottom. So, you know, the way I like to think about it is mathematics and that level of precision and rigor, that's the medium. That's the language, 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 this framework where we can be very precise.

• 1:14:08Tim Scarfe?

  I suppose after formalism, what exactly do you know more of? And who knows it?

• 1:14:14Speaker 06

  Just arguing for formalization in terms of checking correctness didn't get a lot of mathematicians interested.

• 1:14:22Speaker 06

  To my surprise, you know, around 2000, after, you know, 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. 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, you want them to interact. You start thinking about them in terms of what computer scientists call the APIs, right?

• 1:15:06Speaker 06

  You know, you have information and you, you encapsulate things and you expose things. And what, you know, what kind of information you're kind of making public for other people using it? What's the kind of the internals? And so I think mathematicians found it useful to think about mathematics in this kind of software engineering, you know, kind of way of thinking about, okay, you know, what are the different modules? What are the pieces? How do they interact? What are the, the interfaces? I think that they found that this gave them a way of coming back and understanding, you know, the mathematics in new and interesting ways. So it's really just, yeah, exploring the, the structure of mathematics and how the pieces get put together. I mean, we built up these, these, these very complex edifices on top of these, you know, kind of very, very precise rules.

• 1:15:50Speaker 06

  And understanding how you get that level of complexity, you know, down to the, the very simple rules at the bottom is really remarkable.

• 1:15:57Tim Scarfe?

  Alongside concrete tactical discussions about the project, Komele and Schultz debated philosophical aspects of formalization. Komele saw Lean as a better way to work. Schultz did not. These different orientations came through in Komele and Schultz's Zulip exchanges about what it meant to write definitions in math. How do you know that a definition written in Lean is faithful to the definition of an object as mathematicians conventionally understand it? In many ways, coming up with the right definition for an object is the whole game in mathematics. When mathematicians define new objects or new frameworks and abstractions,

• 1:16:41Tim Scarfe?

  they are equipping the field with new tools and perspectives. And Schultz worried that if the definitions were wrong in Lean, nobody could tell. Lean might verify the proof as 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 Komele and Topaz looked for another form of reassurance.

• 1:17:25Tim Scarfe?

  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 Komele 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.

• 1:18:08Tim Scarfe?

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

• 1:18:33Speaker 03

  I was trying to build something that works. Some people were there in this like channel having fun, throwing ideas on the wall, right? I mean, it's cheap. I mean, you can throw ideas on the wall and the other side has to keep telling you, no, this doesn't work.

• 1:18:50Speaker 03

  Something that's, for me, one frustrating scenario. You throw an idea, you didn't spend five minutes thinking about it. Then I find a hole, I send back to you. Then you polish a little bit, send back. Now it takes 10 minutes to find the hole, the next hole. It keeps taking exponentially longer to find the holes on the half-baked idea.

• 1:19:16Speaker 03

  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. You spend time telling people why this is not a good idea, why it's not the time to do it.

• 1:19:31Tim Scarfe?

  So we should come up with a concrete example here. So apparently Kim Morrison used a Claude agent to produce a Lean implementation of the compression format Z Lib and, and prove some specific properties of it. So what exactly did they manage to prove?

• 1:19:46Speaker 03

  But they, I managed to translate from C to Lean, the code. Then managed to keep fixing the Lean implementation to its passage that has suites that comes with the C version. And then it proves that for any compression level, for any data, if you compress the data and then decompress, you get the original data back.

• 1:20:10Tim Scarfe?

  I liken it to the blind men and the elephant, which is that you have all of these blind men feeling different parts of the elephant. And they, they understand parts of the elephant, but they don't understand the whole. And I don't know whether it's a similar thing with this Z Lib, whether it actually encompassed the whole or just some perspective of it. But I suppose the problem, when you only have a perspective of a bigger, complex whole, you, you get problems in terms of, you know, we're talking about reward hacking and, and, you know, like good hearts law and, and all kinds of, you know, degenerate behavior can happen if you optimize only part of a system. So is that, is that part of the story here? Was it actually encompassing the whole Z Lib algorithm?

• 1:20:47Speaker 03

  Yes, yes. For example, one way to do reward hacking, this compression, decompression. So that's, that was the only property we asked the, the AI to show, to demonstrate to us that was achieved. The AI could hack by saying, compression, you just return the data. It's the identity function, you just return. Decompression, you return it back. You proved the property, right? But then you can put more properties, like saying 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 rest implementation in the test suite.

• 1:21:31Speaker 03

  But you're completely right. It's really easy to give properties that do not cover the whole thing, right?

• 1:21:39Speaker 03

  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 code, I, I think this is not super concerning, this problem you raised, but if you want to let the AI go wild and you don't even want to look at the code, it's really important to cover all aspects, right? So otherwise, you can have implementation that satisfies all your properties, but you do not fully specify what you wanted, you're not really getting what you want.

• 1:22:15Speaker 05

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

• 1:22:31Tim Scarfe?

  And how do you see this panning out in the future with agentic engineering? So do you think we will come up with some kind of, yeah, specification, systems of constraints, new ways of working, new ways of engineering to essentially solve this divergence problem? I guess you could call it understanding debt, right? There's this problem of we're building things we no longer understand, we can't verify them. Like practically, how do you think we can engineer this problem away?

• 1:22:56Speaker 05

  The utility of agentic coding is completely bottlenecked right now on this review and verification phase. I think that AI itself makes software verification kind of much more powerful because you can use AI to write these specifications themselves, they don't have to be written by hand. But I think kind of formal verification of software programs will like increasingly have a role to play in the new AI-powered software development lifecycle. There are places like Harmonic, which believe that if you can train an AI model to write math proofs, that same intelligence will be useful for writing proofs about software, for verifying the output of LLMs. So I don't know, that kind of bet is underway. Whether or not it pans out, I don't know.

• 1:23:39Tim Scarfe?

  So underneath all of this software was a very human story of fractious 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.

• 1:24:01Speaker 02

  So AI is coming from mathematics, this is absolutely clear. And what it's going to do to it, nobody really knows. All that we know is it's getting really good really quickly and no one has any understanding of how much better it's going to get. So mathematicians have had various different reactions to this, ranging from, you know, what could only be described as grief, that the subject is changing and that they're going to have to adapt or die. So ranging from grief to excitement, and I'm very much at the excitement end of the scale. I think mathematics is going to be hugely accelerated by this software

• 1:24:44Speaker 02

  because remember, it's already doing interesting things. And the thing you have to remember is it's at its worst, you know, today is the worst it will be, right? 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. So I think AI opens up huge new possibilities for mathematics. It will change many things about it, but at the end of the day, we're going to end up with more understanding, we're going to end up with more theorems proved, and we're going to end up, you know, with just a better overview of what mathematics is and great tools where we can explore new dark corners and enlighten them and enlighten our community.

• 1:25:28Speaker 02

  So going forward, things are very exciting.

• 1:25:30Speaker 06

  What makes our goals special is that they're ours. They're our goals. I mean, you and I are having this conversation, right? And the conversation is what should we do? What should we make of AI and how should we respond to AI and what should we do with AI? Right? We're having this conversation. 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 going to interact with it? So, yeah, it's not that, I don't know, it's, again, the questions I think that we should be interested in are

• 1:26:11Speaker 06

  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 think we should be at the center of the debate just because we're the ones having the debate. If it's our, insofar as it's our debate, we can't help it, make it about, help but make it about what, you know, what we want.

• 1:26:36Speaker 05

  Once I started writing the book, I spent a lot of time with Leo Demora, and that was actually kind of the first moment in which I understood in a certain way the significance of what I was doing. Not like for the world, but just like as a kind of an ethical contract almost between me and the sources, which is this was Leo's life work and he cared a tremendous amount about it. And my book was likely to be the only kind of start to finish story of the development of Lean and just started to feel extremely important to tell the story well.

• 1:27:03Speaker 02

  And I was contacted by a guy called Kevin Hartnett, who at the time worked for Quantum Magazine and wanted to run a piece on Lean and its mathematics library for Quantum. So I ran into Kevin around then and, you know, we became friends and, and he interviewed me several times about several things. And then later on decided that this was such an interesting story that it was sort of worth writing a book on. You know, a decision which I thought was quite an interesting one, but he, he went for it. And during that time, he interviewed me many more times and tried to get some kind of idea as to

• 1:27:47Speaker 02

  sort of how it happened. You know, he wanted to put together, you know, the people behind the story and what was going on. And so my midlife crisis, where I started worrying about human-generated mathematics and asking whether machines could do it better, somehow played a role in Kevin's, in the story that Kevin decided to tell.

• 1:28:06Speaker 05

  As I met more, more figures in the book, more mathematicians, I similarly understood how important it was to them. I spent a lot of time with the six or seven key core sources for the book. It was also very useful to me that this group of people left a tremendous digital record of all of their work. They were initially very active over email and they shared a large, a large number of their private emails with me. They also then later migrated to this chat platform called Zulip, where they conducted a lot of their work in these public threads and then also in private DMs, which they shared with me. And so I was able to kind of reconstruct a lot of the work as if I was like there observing it and in the moment it was taking place. So that was like a tremendous benefit to writing the book.

• 1:28:51Tim Scarfe?

  Yeah. 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?

• 1:28:59Speaker 06

  You know, you don't want to air your dirty laundry, you know, in, in public. I mean, the, the thing about the people working on Lean, it's just a wonder, it's like family, you know, it's just a wonderful community of, of good friends and everybody working on the project was kind of young and idealistic and excited about it. 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 bumpy spots along the way and there were the, you know, there were these tensions and, but we don't want

• 1:29:42Speaker 06

  to dwell on them, right? And so an outside reporter, you know, journalist comes in. And so we were very guarded at first, but I think we, 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, 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.

• 1:30:19Speaker 06

  You know, making it come across that again, it wasn't a matter of good guys and bad guys, but just people looking for different things.

• 1:30:27Speaker 05

  There was this experience I had reporting it where for a period around 2018, Leo goes off and builds Lean4 and simultaneously all the math activity in MATLAB is still continuing at pace. And it just never felt like, kind of like I understood what was going on in those years. It was very not clear to me if Leo was talking to the mathematicians or not. It was kind of a situation where if 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. And they kind of, they kind of actually, they get the message. They're a little wary of like angering this guy who they admire and is so important to them.

• 1:31:11Speaker 05

  There's some particular personality conflicts that I talk about in the book between Leo and this guy Mario Carnero, who both are, just have strong visions for what they want this kind of emerging world to look like. Mario's vision is what he wants MATLAB to look like. He's very much a big open source believer. Leo's vision is for like Lean. The two of them clash quite a lot. And in certain ways, kind of that friction pushes Leo away from the mathematicians in this way, in this 2018 to 2022 period. Anyway, what was interesting for me though, was realizing I'd been like hearing this story. It didn't quite make sense to me. I didn't quite know why. And then almost in like in a rush, the various figures, the sources I was working with, kind of said, oh, this in fact is what's going on. Leo was mad and kind of had left, left this sphere for a little while.

• 1:31:56Speaker 05

  And of course, once, once you get one person to, to explain their side of the story, others are kind of more forthcoming about theirs as well. So I think that's how I felt like by the end, I had understood at least kind of interpersonally fully what was going on with Lean.

• 1:32:11Speaker 06

  Oh, so, so, so 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 Lean4, he kind of held off and, you know, he kind of needed his distance.

• 1:32:27Speaker 06

  And, you know, every once in a while I'd send him an email and get a quick response, but it was clear that he, he wanted some distance. And that was hard, you know, I missed him because he's, he's a very good friend and, 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, so Leo arranged the dinner. It was, other people were in town for the conference. He decided to take the opportunity to bring together advisors for the Lean 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,

• 1:33:12Speaker 06

  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, at Pike's place and we just kind of just walked and just walked and walked.

• 1:33:37Speaker 06

  And yeah, it was, it was just, I don't know, it was just, it was great talking to him again. You know, we talked about Lean, but we talked about things that were not Lean.

• 1:33:46Speaker 06

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

• 1:34:07Tim Scarfe?

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

• 1:34:34Tim Scarfe?

  Now for a quick message from Anthropic, the team behind Claude, the AI built for businesses. Imagination doesn't need permission, just room to play. Claude is an AI that works alongside you to give your ideas the space they need to grow. And then it helps you make them real and ready to ship. Discover more with Claude at claude.ai/span.

• 1:35:03Speaker 01

  Hey, listen. Power up your play with Nintendo Switch 2 and experience Link's legendary adventure, now reborn in vibrant detail on our fastest and most powerful system yet.

• 1:35:16Speaker 01

  And harness the power of the Ocarina with the built-in microphone.

• 1:35:25Speaker 01

  The Legend of Zelda: Ocarina of Time, a Nintendo Switch 2 exclusive. Game and system sold separately. Game rated everyone 10 and up.