Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura

0:00LLMs paired with the Lean Proof Assistant have led to breakthroughs in competition math and more recently the verification of frontier math results. Lean is a critical part of this process because it helps validate the candidate proofs the LLM spits out. In this conversation, I asked the creator of Lean about how it works and how it will affect the future of math and software verification. Could that be the end of handwritten math? Here's the full episode.

0:32There's this famous Dykstra quote I want to start the conversation with. It's that program testing can be used to show the presence of bugs, but never to show their absence. And my understanding is that lean and formalizing proofs can be used to show the absence of bugs. And so in your words, what is lean and how do people use it to show bugs can't occur in programs? Lean is a programming language. You can write code, but you can also write proofs. You can reason about your code. You can write state properties about your code and prove them. Lean gives you machine-checkable proofs. You can check your proofs and get absolute assurance they are correct.

1:16You have many independent checkers. But you should view Lean as a platform. You can write code, you can write properties about your codes, and you can prove them. So could you give a concrete example? Because when I think of a proof, I think of what I learned in math. But then how do you couple that with the software that we write? Yeah, it's a great question. It's not that different from math proof. Lean is actually very popular for math. But for software verification, right, there are two very different use cases. You can reason about Lean programs. Lean is a programming language. You can write programs in Lean itself.

2:04Then a Lean program is not that different from a definition you have in math. The techniques are very similar. But if you want to verify programs written in a different programming language that basically two different approaches. One of them, they translate, it's called shallow embedding. They translate for Rust. This happens today. We have a tool called Aeneas that maps Rust into Lean. And you can verify the Lean translation. And there's another technique called deep embedding where you have the semantics. You write a semantics of the programming language of C in Lean. And now you have a data structure that represents a C program.

2:49And you can state properties about it. It's almost like your programs become Lean objects that you can reason about. To make it really concrete, to give someone a sense of, you know, here's this thing I want to prove about a simple C program. Maybe like no buffer overrun or something like that. What's the step-by-step where we could use Lean to prove that? Yeah, yeah. Let's get array, you're trying to access an array in C, you want to make sure the index is in bounds, you're not accessing elements that your array, for example, has 10 elements, you're not trying to access elements 11, right? Basically, you can write that.

3:33You can write in Lean that the value of i at this point in your program is going to be greater than or equal to zero and less than 10. You can write that as a mathematical statement. Another way to view is that if you can express in math what you care about your program, you can verify using Lean. that's another way to view it. So I have my C source files and then somehow there's an equivalent Lean proof that's almost like metadata on top of the C program. Yes. And that's a line-by-line proof and Lean will go and check. Exactly. People will build automation for automating the process. They're going to use techniques like hard triples that says like we have a precondition, some mathematical facts that should be true before executing that statement, the statement, and what is true after.

4:37And we will have a lot of automation to process. Makes your proof modular. Complexity is a challenge in software verification. Handling the complexity is a big deal. And all these frameworks for verifying programs, they are trying to manage the complexity, to make your proofs modular. Even with AI now, AI can prove things automatically for us, but they have to be modular to the proofs if you want them to scale. And what you're saying sounds similar to in software, where you have to write it cleanly, it needs to be easy to edit and reason about. So it's almost like a second software layer on top of the software.

5:20Yes, yes, you can feel this way. You can also flip and imagine a future where you're writing what you want mathematically, precisely, and AI synthesizing the codes and a proof that's the code that was synthesized meets your specification. Oh, interesting. So you could start by writing what you want to be true. Yes. And then... Ask the AI, please. And AI is going to just go and hammer at it until the lean proof says you're good. Yes. It feels like science fiction. Six months ago, I would say this is science fiction. But, for example, now a colleague of mine, Kim Morrison, a few months ago she started a project.

6:09I thought it was six months ago I would say it's not possible at all. She said, we have Zlib, this compression library written in C. And she said, she creates a very complicated prompt for AI saying, I want you to translate to Lean, ensure the Lean version passes the test suite for Zlib. Then I want you to prove that if you compress data and you decompress, you get the original data back. It's a really strong property, right? and believe it or not after one week succeeded doing the whole thing and now it's just asking to optimize the code but you cannot break the proofs I mean you have to keep still proof all the properties you care about I mean compressing and decompressing getting the data back is a really important property for a compression engine yeah this is enrich I mean, it's real.

7:16I mean, it's crazy. And I hear in the industry, a lot of people, they use a really comprehensive test suite coupled with AI to do some really amazing rewrites. Because they have some more confidence that the rewrite is accurate and the AI can check itself. and it sounds like a specification is even better than a comprehensive test suite. Yes, yes, because, well, your quote from Dijkstra captures perfectly, right? With a test suite, you can show the presence of bugs, but not the absence. It's almost like with a good test suite, you may say, well, probably there are no bugs here, but you may have a really corner case that's not covered by your test suites but with a proof you're covering all possible cases.

8:14And it connects. So property-based testing is really popular now. People are writing properties they want to ensure they are true but they are checking with testing, right? But now we can prove them and you say, look, There's no point testing anymore. I prove it. It seems like having a well-written specification is a superset of a test suite. But in terms of the human labor required to create a reasonable test suite versus a reasonable specification, how much more work is it to come up with a great specification? There is a lot. I mean, the programs, in many cases, it's not uncommon for someone to start developing a piece of software and they don't know exactly what the spec is, right?

9:13But you know properties. Usually, their properties are very clear in your mind. Another thing that I tell people to keep in mind is that an inefficient program can be viewed as a specification. Usually, writing an inefficient program is way easier than writing the super efficient one that has many clever tricks. You can write a very, this is what I want, in a very naive way. And you ask the AI, look, generate the efficient version and optimize and prove that's equivalent to my inefficient one. There are many scenarios. I mean, I will not say this. Specifications are always easy to come up with.

9:57But properties, usually the developers have good ideas about properties they care about. As inefficient programming is a spec, right? You can do a specification. And the technology, formal verification complements testing, right? I think your code from Dextra captures perfectly. And I think I saw this on Twitter because Jane Street was more heavily investing in formal verification. And I read their post and they talked about this. I think it was a cell for some software that was entirely formally verified. Yes. And the main drawback to why it wasn't, you know, how much more time would it take writing a program versus verifying it?

10:47Your example, Cell 4, is a great example. This was a major milestone. It's a microkernel they verified. Done manually was before AI. This project was done before AI. It was a big deal. And it's a lot. The cost is super expensive, right? At AWS, we have been using formal verification for a decade, but only for the super safety critical components because it's expensive until now, right? with AI, it changes the game. You have to come up with a spec, but this is not the most painful part. The most painful part is to develop the proofs manually, if you have to, before AI, and maintain the proofs as you change the codes.

11:35Imagine, you know, I've seen people complaining that, oh, I changed the program right now. I have a bunch of failures in my test suite, and I have to patch, go one by one. Imagine if proofs, it's the same process. You have to fix the proofs. Sometimes you don't remember anymore why the proof, what's the story behind this proof. It's a lot, but AI is extremely good at proving, writing formal proofs, maintaining formal proofs. for example yesterday i was changing something in linia i want to modify some proofs for technical reasons i didn't even know what the proofs were about someone else wrote then i said look i want you to i asked the i he write these proofs without using this feature because i'm going to change it i don't want to break the libraries it's instantaneous it came up with the new proofs for me, I mean, it's really good.

12:39And this is crucial for making formal verification mainstream, because otherwise maintaining the proofs was almost like if your program took X amount of time to do the formal verification in the past, it would take 10X, that would be normal. But imagine if your program is changing, that's something that's really common. Now you have to keep maintaining the proofs too. It's a lot of work. But AI eliminates this pain for us. You mentioned that Lean is, because I hear it as a proof assistant, and then you also said it's a programming language. Is that typical for proof assistants to be both a programming language and a proof assistant?

13:30Some of them, especially the ones that are based on dependence type theory, they are like rock and lean are programming languages in proof assistance right you can write definitions like when you're defining concepts in math but some of these definitions can be programs I mean and you have types you have structures it is a programming language but is in that the family of called functional programming language I mean is a specific kind of programming language. For people that are familiar with programming languages like Haskell, Lean is close to Haskell. But with the support for proofs, that's a way to view Lean.

14:15Are there major use cases where people use it as programming language but not as a proof assistant? Well, the first big use case is Lean. It's implemented in Lean. We have many of our tooling is implemented in Lean, like the documentation authoring system called Verso is implemented in Lean. The build system that's called Lake, it's like Lean Make. Lake is implemented in Lean. At AWS, we have a compiler for AI accelerators. It's half a million lines of Lean. And it's using Lean as a programming language. They're proving some properties about the program using Lean. But the main goal is to use Lean as a programming language in this project.

14:59The proofs are like a bonus, right? That you can get the proofs and find problems in the design. I think most people are familiar with programming languages and the tool chains they have. But what are all the major components that you would need for a proof assistant? It's not that different. I mean, if I use modern programming language like Rust, the tooling, for example, Lake is our cargo, right? I mean, you're going to open Visual Studio Code, same way. And I'm going to get all the IntelliSense. One big difference is that we have something called the info view in Lean. Your screen is usually going to be split in two.

15:44You have your file on the right-hand side. You have the info view that tells you information about your proofs, about your codes. is giving you constant feedback about your development. That's basically the main difference. But the tooling, VS code, everything works the same way. It seems like a programming language is the fundamental layer, and then there's some additional layer on top that keeps track of that stuff. Good question. In Lean, you have definitions that show your program, but you have theorems, statements. You're going to say, for example, factorial is always greater than or equal to zero or something like that.

16:29Or if you add two even numbers, you get an even number. You can write statements like that. And immediately you can write actually a program that's the proof. But most people don't do that. They go into something called tactic modes. You can view it as a domain-specific language for writing proofs. In Lean, when you write by, it switches to this domain-specific language. And you have steps like simplify my goal, the state of my proof. You can say, oh, apply this rewriting step. Apply, for example, we know that x plus 0 equals x. You can ask Lean, apply this rewriting. And you're going to see in the info view the state of the proof changing.

17:17You get immediate feedback and you get this feeling that you said you keep telling, applying transformations to your proof. Step by step, you can see what's happening until you get no goals left. You are done. The proof is complete. And some people view this process as a game. I have users that told me, you built my favorite computer game. That's funny. Is Lean itself verified in Lean? Lean is a massive program. You only have to trust the kernel. The kernel is where the proofs are checked. Lean itself is the kind of program that, because there are so many new things we are adding, it's not even clear what is the specification.

18:04For example, what is the specification of a simplifier. You can write general ideas, but users, they want to be able to customize the behavior. They keep asking, they keep changing the specification all the time. I want this, I want that. No, add this knob here. It's really hard to have a full specification of Lean, but the kernel is possible to have a specification. We have a kernel. The kernel that comes with Lean is not verified, but there are other kernels that you can use One of them is implemented by Mario Carneiro. It's called Lean for Lean. And it's implemented in Lean, and he's verifying.

18:46It's proving that this kernel has been verified with respect to the semantics of Lean. This is a cool project. But for us, having multiple kernels is the best way to ensure that your results are correct. I mean, some users implement their own kernels. We have kernels implemented in Rust, in different programming languages. And when you say kernel, what's the responsibility or what's the inputs and outputs of that portion? Yes. And lean proof checking is type checking. These kernels, they are type checking your programs. Basically, you can export your lean developments. you got a big blob and you read this blob and they're going to check if when you say we have a proof in Lean basically we have a term that has a type and you're checking if the type of this term matches the type that you claim it has for example the example of the even numbers this is a type in Lean saying that the sum of two even numbers is an even number you can write you can do that it is exactly a type and the proof what the kernel is checking is whether the type of the proof matches the type you claim this term has and the kernel will check you'll do this type checking the kernels vary between a high performance kernel it's like 5000 lines of code I mean the goal of the kernel should be something you can write yourself of course sometimes people put bells and whistles like one concern people have is like okay but how do I know suppose I wrote Fermat's last theorem in Lean, how do you know that when you export it's really Fermat's last theorem it's not 2 plus 2 equals 4 I mean and people, some external kernels they write print printers.

20:55I mean, it will print the statements that has been proven, all the dependencies. You can have all these fancy tools to make sure you're not being misled. Lean, obviously, it's so powerful. And I see on social media all these amazing results from formal verification. I want to know what are the top ones that you think of or top examples more recently that have impressed you that Lean was able to accomplish? Well, there are so many, I mean, that I thought it was impossible. For example, getting a gold medal in the International Mathematical Olympiad. A few years ago, everybody thought it was impossible.

21:38Now everybody, they use it as a benchmark of an easy problem. They say, oh, this is like an IMO problem. I mean, this is easy. But it's not. I mean, these are really challenging problems. the others conjectures that people close using lean ai with lean also impressed me there's this unit distance conjecture for others first open ai proved using formal right was not formal and we have a system now in lean it's a website where we call lean eval where we collect challenges. The same Kim Morrison saw this proof of OpenAI and she puts on LeanVal as a challenge. Say, okay, I want to see someone formalizing.

22:31We knew it was huge to formalize. It's serious math. It depends on. And Boris Alexei from OpenAI, he did. He submits a one million line proof for whole proofing lean for this conjecture. We estimate, I mean, the ground math that is needed for the proof, we knew it would take months, I mean, for experts to do by hand. How long did it take in that case? Like the time from when the proof came out to when the challenge was solved on the lean? I think it was one month. yeah and after kim was a few i think less than two weeks after kim puts as a challenge on lean i took i think two weeks to get the or less i mean that's that's insane yes yeah we talked about verifying programs but also there's using it just directly for mathematics like in this case how popular is lean in terms of when you look at the users of lean what percent are using it for software engineering what percent are using it more for just direct math well historically lean got popular first with math right i mean no with the beginning of the lean mathematical library in 2017.

23:56We had like a big project called Liquid Stencil Experiments. It started beginning of 2020. It was a big deal because it was to verify a result from a field medalist. Peter shows it. It's a result he was unsure about. He has not published it. He felt like this was one of the most important results in his career. here, he wants to be sure it was correct. It was done manually, the verification. It was a big deal because the team that formalized it led by Johan Komelin, they not only formalized the results without fully understanding it, they do not fully understand the proof, but having this info view helped them, guide them step by step.

24:47they formalized and simplified the proof without fully understanding the proof. It's mind-boggling, right? I mean, how can you simplify a proof from one of the greatest living mathematicians without fully understanding it? I mean, but they managed to simplify. It's almost like when people do refactoring codes and you start changing the codes. It's faster now, but the programmer doesn't really know why. I mean, it felt like that. It's like you have a gut feeling, I mean, that you're going in the right direction. And this, for us at the time, lots of people got excited about the math community because of this project.

25:28It's like it's shown that's not about verifying, but enabling people to work together in large numbers. Because you can trust, you don't need to trust someone else's proof, right? They can fill holes for you. this was I mean what attracts a lot of attention from the math community then came Terence Tao he starts using after this project he has really cool projects with and without AI and he got addicted actually I think the first time he used it he said I don't think I'm going to do it again the formal proof one week later he had another project using Ling and he did a new result he had. When you say addicted, you mean because that game, that completion engine.

26:17Yeah, some people, we feel like when I talk to professors that use Lean for teaching, they tell me that the class is going to split. Some people love it. Some people don't like. But people that like problem solving, people that get medals in the IMO, they love lean because you get this excitement of solving is like solving millions of really hard sudoku problems right and you can keep solving one and it's easy to get i mean i'm a lean developer not a lean user but when you're developing lean i'm coding in lean and sometimes i have proved things it's really easy to get addicted and get lost proving things you get this bus every time you prove something.

27:07You mentioned the IOI gold medals. How is Lean used in that kind of I think maybe you're referring to Alpha Proof by DeepMind or maybe something else? Yes. DeepMind was, they got in 2024, was a big surprise in 2024, they got a silver medal. And now we have gold medals from startups like Harmonic. By Dance got a medal. I never I never imagined by dancing, they're behind TikTok, right? I didn't even know they care about formal math, but they have a formal math team. They got medals also. The approver is really good. So how's it work? Let's say, I mean, there's a series of math problems. Lean is just used for verification, right?

27:55So I imagine there's other components there. Yeah, there's the AI. You can view it like we have Go that was very popular with AI. The AI is playing the game. I told you that many people see Linhaza game. It's the same. I mean, the AI is viewing Linhaza game. They have the statements of what you want to prove. You have the buy keywords. Now you have a blank field. Make sure that you have no goals left, right? It keeps applying steps in this game. And seeing the state of the boards, right? That's the info view changing. and the AI, they use reinforcement learning for trying to get to no goals left.

28:40It's a single player game. Some people play together these days, but the AI is learning to play the game. So before we were talking about that game, it kind of starts with the specification. So in that case, then the problem is kind of the specification and then it hammers away. You have basically for each problem in the International Mathematical Olympiad, someone translates to Lean the statements. It's super important to have the mathematical library because you want to be able to talk about the problems, right? For example, support the problems uses the real numbers. You need a definition in Lean.

29:18And we have it inside of Mathlib, the Lean Mathematical Library. The first thing you have to be able to write the problems in Lean. and this now because of mathlib it's easy part and after that you have to provide the proofs sometimes some problems you have to come up with a definition to some objects you have to create that has some property but that's how it is I remember you said one of the first use cases of Lean was this fields medalist had this novel mathematics and then we use Lean to verify it. But can Lean be used with LMs to generate novel mathematics or just verify existing? It's a good question.

30:09I mean, we don't see lots of evidence. We see now evidence it can find novel proofs, right? But coming up with new mathematical concepts is still at the limits, right? I mean, right now, in this lean of all, we have challenges where the AI has to come up with the objects themselves, right? I mean, but these people will keep investing in this area. I would not bet against AI here. I mean, but right now we don't have evidence they can come up with new math. OpenAI, Anthropic, Cursor, and Vercel all use this product to make their lives better. And the problem it solves is when you're building SaaS or an AI product and you want to sell to other companies, there's all these requirements you need to meet.

31:02There's SSO, there's SCIM, there's RBAC, there's audit logs. These are all things that take time to integrate but aren't the main focus of your app. WorkOS is an API layer that lets you meet all of these requirements in just a few lines of code. So let's say you have a new SaaS product and you want to sell to other companies. WorkOS will solve all of these critical feature gaps for you. You can check them out at workos.com to learn more and get started. And I appreciate them for supporting my work and sponsoring this podcast. When I see on Twitter this major conjecture, they made headway on it.

31:38It's that they made headway on confirming something. Or just proving. They also have these one million lines. They've shown the conjecture was false. They have a proof showing that it's false. But it's a formal proof. They did not come up with a new theory or anything like that. They are coming up with a proof. At what points would you say someone should evaluate formalizing something in Lean? I think if it's safety critical or if you don't understand really well, I mean, this is important part. I don't really understand. Anybody that went through the process of formalizing something understands the subject way better after that.

32:30I almost feel like I remember when I was in college, people would say, well, after I implemented this algorithm, now I understand it's much better. the next level is that you implement the algorithm, you prove the properties you expect. Your level of understanding grows, right? I mean, another cool thing is that it enables you to be much more bold on your optimizations. Because sometimes, I've seen that all the time, people fear implementing optimization because they don't really understand why the piece of software works. They feel like if I do that, it still works and is faster, but they are not confident.

33:17With proofs, you eliminate discomfort. You can prove it again, or the AI can prove for you or find a counter example. They are good at both things. But if you were to speculate or draw into the future, maybe three to five years from now, if the cost of formalizing things goes down? How does that change software? How does that change, you know, handwritten math? Oh, I think it will change dramatically, right? We have to keep in mind the big labs, they only start training for formal verification very recently, right? Seriously. Before that was like, oh, it's in the data sets. I mean, you don't really have the reinforcement learning.