The Peterman Pod - Creator of Lean: Handwritten Math Will Change Dramatically | Leonardo de Moura

Episode Date: August 10, 2026

Leonardo de Moura is the creator of Lean and the Z3 theorem prover. I talked with him about how Lean works and why LLMs plus Lean will fundamentally change how we write software and do math.• My ergonomic keyboard project I mentioned, you can follow along here: https://read.compose.llc/• The Kickstarter page for it: https://www.kickstarter.com/projects/ryanlpeterman/compose-simple-ergonomics-beautifully-donePodcast links:• YouTube: https://youtu.be/KzdYKeAqWhY• Apple: https://podcasts.apple.com/us/podcast/the-peterman-pod/id1777363835• Transcript: https://www.developing.dev/p/creator-of-lean-the-end-of-handwrittenThank you to this episode's sponsor for supporting my work:• WorkOS: makes your app Enterprise Ready with easy to use APIs to add SSO, SCIM, RBAC, and more in just a few lines of code, check them out at https://workos.com/Timestamps:(00:00) Intro(00:28) How formal verification works(05:21) A new way of writing software(13:15) Proof assistants vs programming languages(21:06) How Lean has assisted in mathematical breakthroughs(32:03) When is it worth formalizing software(33:29) How Lean will impact handwritten math(38:55) The Z3 theorem prover project he started(45:44) The most technically challenging work of his career(51:10) Lean vs its competitors(01:00:37) The future of Lean(01:04:10) Technical book recommendations(01:06:15) Advice for his younger self(01:07:10) OutroWhere to find Leonardo:• Wikipedia: https://en.wikipedia.org/wiki/Leonardo_de_Moura• Website: https://leodemoura.github.io/• GitHub: https://github.com/leodemoura• LinkedIn: https://www.linkedin.com/in/leonardo-de-moura-26a27b5/• X/Twitter: https://x.com/Leonard41111588Where to find Ryan:• Newsletter: https://www.developing.dev/• X/Twitter: https://x.com/ryanlpeterman• LinkedIn: https://www.linkedin.com/in/ryanlpeterman/• Threads: https://www.threads.com/@ryanlpeterman• Instagram: https://www.instagram.com/ryanlpeterman• TikTok: https://www.tiktok.com/@ryanlpetermanReferenced in this episode:• Lean 4: https://github.com/leanprover/lean4• Mathlib: Lean Mathematical Library: https://github.com/leanprover-community/mathlib4• Lean4Lean: https://github.com/digama0/lean4lean• Liquid Tensor Experiment: https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/• Veil protocol verification language: https://veil.dev/• Z3 theorem prover: https://github.com/Z3Prover/z3• seL4 formally verified microkernel: https://github.com/seL4/seL4

LLMs 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. There'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? LIN 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.

You have many checkers, independent checkers. But you should view LIN 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 difference from math proof. Lean is actually very popular for math. But for software verification rights, there are two very different use cases. reason about lean programs, LIN is a programming language. You can write programs in LIN itself. Then a LIN 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 what this happens today. We have a tool called the Enneas that map rust into Lean and you can verify the Lean translation, right? And there's a lot of technique called Jeep 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. And you can state properties about it.

It's almost like your programs become lean objects, right, 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 a step by step where we could use lean to prove that? Yeah, yeah. Let's get an 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. You can write in line that the value of I at this point in your program is going to be greater than equal to zero and less than 10, right? You can write that as a mathematical statement. Another way to view is that if you can express in math, what you care about, you? 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 Hort 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. And they will have a lot of automation to process. Makes your proof modular, right? I mean, complexity is a challenging software verification. Handling the complexity is a big deal. And all these frameworks for refining programs, they are trying to manage the complexity. complexity, make your proofs modular. Even if 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. Yes, yes, you can view this way. You can also flip and imagine a few. future where you're writing what you want mathematically, precisely, and AI synthesizing the codes and a proof.

That's the code that you synthesize it meets your specification, right? Oh, interesting. So you could start by writing what you want to be true and then ask the AI, please. And AI is gonna just go and hammer out 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, King Morrison, a few months ago she started a project I thought was six months ago, I would say it's not possible at all. She said, we have Z-lib, this decompression library written in C. And she said, she created 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 codes. But you cannot break the proofs. I mean, you have to keep still proved all the properties you care about. I mean, compressing and decompressing, getting the data back is a really important property for a compression engine, right? Yeah, this is in rich now. I mean, it's real. I 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 with, well, your quote from Dykstra captures perfectly right. With a test suites, 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 suite,

but with a proof, you're covering all possible cases. And 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? Various a lot. The programs, in many cases, it's not uncommon for someone to start developing a piece of software. They don't know exactly what the spec is, right? But you know properties.

Usually their properties are vaguely in your minds. Another thing that I tell people to keep in mind, that an inefficient program can give you this specification. Usually, writing an inefficient program is way easier than writing the super-efficient one that does, 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 equivalent to my inefficient one.

There are many scenarios. I mean, I would not say these specifications are always easy to come up with, but properties, usually the developers have good ideas about properties they care about. As inefficient program is a spec, right, so you can view as a specification. And the technology, formal verification, complements testing, right? I think your code from Extra 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. Your example cell 4 is a great example. This was a major milestone. It's a microcernel they verified. Done manually was before AI. This project was done before AI was a big deal. It's a lot. The cost is super expensive, right? At say, AWS, we have been using formal verification for a decade, but only for the super safe, it's critical components, because it's expensive until now.

Right? So if AI, it changes the game. You have to come up with the spec, but this is not the most painful part. The most painful part is to develop the proofs manually, if you have two, before AI, and maintain the proofs as you change the code. I've seen people complaining that, oh, I change the program right now. I have a bunch of failures in my test suites. And I have to patch, go one by one. Imagine with 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 is a lot. But AI is extremely good as proving, writing formal proofs, maintaining formal proofs. For example, yesterday I was changing something in Linia. to modify some proofs for technical reasons.

And I didn't even know what the proofs were about. Someone else wrote them. I said, look, I want you to, I asked AI, he write these proofs without using this feature because I'm going to change it. I don't want to break the libraries. Instantaneous, it came up with the new proofs for me. I mean, it's really good. And this is crucial for making formal verification mainstream

because otherwise maintaining the proofs. the proofs. It was almost like if your program took X amount of time to do the form of verification in the past, you 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 that Lean is, because I hear it as a proof assistant, but and then you also said it's a programming language. Is that typical for proof assistance to be both a programming language and a proof assistant? Some of them, especially the ones that are based on dependence type theory, they are like

rock and lean are programming languages and proof assistance, right? You can write definitions like when we're defining concepts in math, but some of these definitions can be programs. I mean, and you have types, you have structures. It's a programming language, but isn't 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,

Lynn is close to Haskell, I mean, but with the support for proofs. That's a way to view. Are there major use cases or people use it as programming language but not as a proof assistant? Well, the first big use case is LIN is implemented in LIN. We have many of our tooling is implemented in LIN, like the documentation authoring system called VERSO is implemented in LIN.

The build system that's called Lake is like LIM make, lake is implemented in LIN. At AWS we have a compiler for AI accelerators. It's half million lines of LINN. And it's using LIN as a programming language. They're proving some properties about the program using LIN. But the main goal is to use LIN as a programming language in these projects. The 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? components that you would need for a proof assistant. It's not that difference. I mean, if I use to modern programming language like Rust, the tooling, for example, Lake is our cargo, right? You're going to open Visual Studio codes, same way. And I'm going to get all the Intellisense. One big difference is that we have something called the InfoVue in Lin. Your screen is usually going to be split in two.

You have your file on the right-hand side. You have the info view that tells you information about your proofs, about your codes. It's giving you constant feedback about your development. That's basically the main difference. But the tooling, VES 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. Good question.

In Lean, you have definitions that are your program, but you have theorems, statements. You're going to say, for example, factorial is always greater than equal to zero or something like that. Or if you add to even numbers, you get an even number. You can write statements like that. And immediately, you can write actually a program that is the proof. But most people don't do that. go into something called tactic modes.

You can view as a domain-specific language for writing proofs. In Lin, when you write by, it switches to this domain-specific language. And you can, you have steps like simplify my goal, the state of my proof. You can say, oh, apply this herewriting step. Apply, for example, we know that x plus zero equals x. You can ask Lin, apply this rewriting. And you're going to see in the info view. the state of the proof changing, you 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.

For 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 changing the specification all the time. I want this, I want that. No, add this knob here. So it's really hard to have a full specification of Lin. But the kernel is possible to have a specification.

We have a kernel. The kernel that comes with Lin is not verified. But there are other kernels that you can use. One of them is implemented by a Mario Carnado. It's called Lean for Lin. And it's implemented in Lin and he's very fine. It's proving that this kernel has been verified with respect to the semantics of Lin. 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 implemented their own kernels. We have kernels implemented in Rusts in different programming languages. And when you say kernel, what's the response? 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 read this blob and they're going to check if... When you say we have a proof in lien, basically we have a term that has a type, and you're checking if the type of this type matches the type of the type that you claim it has. For example, the example of the even numbers. This is a type in link saying that the sum of two even numbers is an even number. You can write, you can do that.

It is exactly a type in line. And the proof, what the kernel is checking is whether the type of the proof matches the type you claim this term has. I mean, the concerns will check, you'll do this type checking. The kernel's very between high-performance kernel to like 5,000 lines of codes. I mean, the goal of the country should be something you can write yourself. Of course, sometimes people put bells and whistles, like one thing concerns people have is like, okay, but how do I know? As I put that I wrote Fermat's last term in Ling.

How do you know that when you exported, it's really for my last theorem. It's not two plus three equals four. I mean, and people, some external kernels, they write print printers. I mean, it will print the statements that has been proved, 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 now everybody They use it as a benchmark of an easy problem.

They say, oh, this is like an IMO problem. I mean, it's easy. But it's not. I mean, these are really challenging problems. The other conjectures that people close using LIN, AI with LIN also impressed me. There's this unit distance conjecture for others. First, open AI proved using informal, right?

was not formal. And we have a system now in Ling. It's a website where we call Lean Eval, where we collect challenges. The same King Morrison saw this proof of OpenAI, and she puts on Linerval as a challenge. Say, okay, I want to see someone formalizing. We knew it was huge to formalize it.

It's serious math. It depends on. And Boris Alexi from Open AI, he did, he submits a one million line proof for formal proof in lien for this conjecture. We estimate, I mean, the ground math that is needed for the proof, we knew to take months, I mean, for experts to do by hands. 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 lien? I think it was one month. And after Kim was a few, I think less than two weeks after Kim puts as a challenge only in Val, I took, I think, two weeks to get the, or less.

That's insane. Yes, yeah, yeah. We talked about verifying programs, but also there's using it 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 became got popular first with math right i mean no with the beginning of the lean mathematical library in 2017 we had like a big project called liquid stensual

experiments uh it started beginning of 2020 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. He felt like this was one of the most important results in his career. He wanted to be sure it was correct. It was done manually, the verification.

It was a big deal because the team that formalizes led by Johann Komelin, they not only formalizes the results, the results without fully understanding. They do not fully understand the proof. But having this info view helped them guide them step by step. They formalize and simplify the proof without fully understanding the proof. It's mind-boggling, right? How can you simplify a proof from one of the greatest living mathematicians without fully

understanding it? I mean, but they manage 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. It felt like that. It's like you have a gut feeling. I mean, that you're going the right direction.

And this for us at the time, lots of people got excited about lean the math community because of this project. It's shown that's not about very fine, 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 feel holes for you. This was, I mean, what attracts a lot of attention from the math community. Then came Terran Stahl. He starts using after this project.

He has really cool projects with and without AI. 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 Yeah some people I feel like when I talk to professors that use Lin for teaching They tell me the class is quite split some people love it Some people don't like But people that's like

Problem solving people that's like problem solving People that get medals in the IMO, they love Lien because you get these excitement of solving. It's like solving millions of really hard Sudoku problems. 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 LIN, 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. You mentioned the I-O-I 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 the got in 2024. It was a big surprise. In 2004, they got a silver medal.

And now we have gold medals from startups like Harmonic, By then's got a medal. I never imagined by then they're behind TikTok, right? I just even know they care about formal math, but they have a formal math team. They got

medals also. Their approval 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? So I imagine there's other components there. Yeah, there's the AI. You can view it's like

We have Go that was very popular with AI. The AI is playing the game. I told you that many people see Linus again. It's the same. I mean, the AI is viewing Linens again. They have the statements of what you want to prove. You have the buy keywords. Now you have a blank feel.

Make sure that you have no goals left. It keeps applying steps in this game. And seeing the state of the board. That's the info view. changing. And they they use reinforcement learning for trying to get to

no goals left. It's a single player game. Some people play together these days, but yeah, 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. The problem, yeah. You have basically for each problem in the international mathematical Olympiad, someone translates to Linh 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, suppose the problems uses the real numbers. You need a definition in Lin, and we have it inside of Mathlib, the Lean Mathematical library. The first thing you have to be able to write the problems in Lin. And this is now because of

math lead, it's easy part. And after that, you have to provide the proofs. I mean, sometimes some problems you have to come up with a definition to some objects. You have to create that has some property. But yeah, 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 used Lean to verify it. But can Lean be used with LMs to generate novel mathematics or just verify existing? It's a good question. I 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 linear value, 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 batch against AI here. I mean, but right now we don't have evidence they can come up with new math. Open AI, Anthropic, Cursor, and Versal

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. There's SSO, there's Skim, there's Rback, 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, it's that they made headway on confirming something. Or just proving. They also have these one million lines, they shown the conjecture was false. They have a proof showing that it's false. But it's a formal proof.

They did not came up with a new theory. or anything like that. They are coming up with a proof, right? At what points would you say someone should evaluate formalizing something in lean? I think if it's safe 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. I 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 opportunity. 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 still works and is faster, but they are not confident. With proofs, you eliminate discomforts, right? 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 you'll change dramatically, right? We have to keep in mind the big labs, they almost start training for formal verification, Lean very recently, seriously. Before that was like, oh, it's in the data sets. I mean, you don't really have the reinforcement learning pipelines to optimize. The behavior we see today that is already amazing will get way better in the future.

The costs will reduce programming languages like Lean and Rock will become more mainstream because of that. Many people are not so, in the past people would say, oh, functional programming, I don't like it. But if I'm not the one that's writing most of the codes anyway, it doesn't really matter. What matters is the specification level, right? It doesn't really matter how the code has been written. Yeah, I think you'll change a lot because of that.

At least that's the direction we are pushing me into. What about, let's say, you know, 10 years from now, Lean is everything's going really well with Lean. Is that the, could that be the end of handwritten math or handwritten proofs? I think there will be always an aspect that is handwritten. Some people like to make a proof look. They want to use the proof as an artifact that you communicate. ideas to others. I can't imagine there will always be people polishing, making them super easy to understand, for another human, to communicate ideas to other people. There will always be people like that. The same way today we have people that, we have machines that build furniture, but people they like to create them by hands and polish them, make them perfect.

This will always exist, but it will be a mixture. I will be surprised as if there is someone that is completely AI's not in their workflow somehow, right? You'll be hybrids, many hybrids. Some people don't like feel uncomfortable about this future. But for me, it's super exciting because I view developing software a super painful process. And with AI, it's crazy how it brings you our runners of how many steps are just repetitive and there's no creativity or just patching things. AI automates removes lots of this pain. I mean, I cannot go back to.

I'm looking forward to this future you described. Yeah, I guess the thing that gives people, I'm guessing, the discomfort is the worry that if it kept going, then, you know, we need less mathematicians or less computer scientists or something like that. People don't see that AI can bring more people. There's also the specification. I mean, I see people saying, oh, we're going to leave AI. we'll come up with new math. But if there's no connection to our world, this is some alien thing that's going by itself.

You need an interface. For example, we want to build programs because you want to accomplish something. This something, whatever it is, has a specification. There will be always humans in the loop saying, this is what we need, this is what we want. writing this interface, interacting with the AI. The AI will have math libraries and everything to prove things about these

these programs we are writing, these artifacts, whatever we are trying to build. But we have to be able to interact these libraries. We have to understand the abstractions that are there. I don't see humans being limited. We are always going to be there. We're in the interface. We are telling them what we want.

Specifications will be there. I can see people always writing codes. Another thing, a lot of people like to write, they say I love coding. My interpretation is they love to write prototypes. This is fun. This is the fun part to try a new idea, but to transform it into our own.

products is never fun. I can tell you, it's never fun. And I can take over these parts. And nobody really likes doing. Outside of Lean, I know you worked on the Z3 SMT solver. And that sounds like a really difficult thing to build. So first, what is that solver in your words? And yeah, how does it differ from a SAT solver? Yeah, I saw this is really long. It's going to be, yeah, 20 years ago I started this tree. I mean, when I joined Microsoft Research. Yeah, Zs3S70 software. It's like a set software, but you have backgrounds theories,

like you have support for arithmetic, for arrays. These are not random choices, right? This is because you use for doing test-key generation software, for doing software verification. Lines fully automated, is a push button. Although Lean Z tree are called term Provers, there are completely different

beasts. Zetree is fully automatic. Lean is interactive. It has automation, but it's interactive. The tree is not a programming language. It's more like a constraint solver. It turns out you can prove simple things

about it. You cannot do advanced math with abstract math. You can solve constraints with you. with Z3. What's an example of the inputs to this SMT solver and what you get out from it? Oh, I can give you one. I mean, that's even in the Z3 manual. You can encode a Sudoku problem as a set of constraints, and you can ask Z3 to solve, and you will give you back the answer instantaneously. For real applications, Z3 was used very successfully for finding bugs in software.

people would convert, for example, suppose that you have a path in your code, you know that has a security vulnerability. But you don't know which inputs to the program allow you to execute this path. You can convert that into a set of constraints that you send to Z3 and it will say unsatisfiable. It means it's impossible to execute this path and you are happy or it gives you back an example saying, With these inputs, you're going to be able to do it. And people use ZE3 for doing software verification. But because the problem becomes undecidable, at that level, you have many universal quantifiers for stating properties about your program,

your pre-imposed conditions. The silver has heuristics. And it just was all before AI. The heuristics were hand-coded. They will always fail. And for simple things, people would be very happy with the fact that Z3's push button. But when the property is not trivial, they would come back saying, come on, I know the proof. I mean, why Z3 can't find it.

That's why I leaned started. I started to make sure that we would have a system that's really good for software verification. Right. Z3 was successful for finding bugs, but not so much. much for software, for proving the absence of bugs. It was never super successful there. But Linth was born to fill this gap. You said undecidable, but in practice in the real world,

if you run it, does it typically terminate? Yeah, great question. The three goes the whole complexity ladder, right? So you have sets, you have NP complex. complete, P space complete, XP, you have the whole, too undecidable, right? I mean, surprisingly, even for sets, you can write really time set problems that are really hard to solve. No set server will solve them. But in practice, the problems we get for hardware verification, especially if you bound everything, say, oh, I'm trying to look for a bug in the first 10 stack.

apps, right? Everything's bounded. You're not trying to prove, but you're trying to capture a class, like a space of scenarios, right? They are very effective there. I mean, I think the lesson there is that programs and hardware, they're not correct by esoteric reasons, right? They are correct because for very simple reasons. I mean, that's why these tools are super effective. effective there. Yeah, but when you get too undecidable, when you're trying to prove even if the property is not trivial there, I mean, it runs out of steam. I mean, and they time out frequently. And sometimes there is a here, a colleague of mine here at Amazon and Minator like chooses the name, proof instability. because sometimes if you change the problem, you just flip.

You have A and B, you write B and A, where B and A are complicated formulas. You may fail to prove. When she was just trying to maintain things, proofs would break if using this kind of technology. But with Lean, she switches

to Lean and is super smooth, because you're controlling the proof. In the Lean case, Why is it so much more efficient? Your proof is basically you can view the sequence of steps for solving the problem. In Z3, you can view that you have only one proof step, solve.

Right? I mean, you have options to solve, flags, but you have very, you cannot influence what Z3 is going to do. It's much harder to influence this kind of series. In Lin, if you want to give a super detailed step-by-step proof, you can. You can use proof automation like it's available in Z3, but you can also break it down step-by-step. And the fact you can do that, humans can do it, but the happy surprise is that AI can do it, because now you can say step-by-step why something is true, the AI can convince Lin that it's

it can provide a proof. When you were working on Z3 and Lean, what was the most technically challenging part that you had to build for either project? I underestimated how much harder Ling is in comparison of Z3. It's always of a magnitude harder. I mean, I talked to many colleagues about that, why I felt like

this line was so much harder. I think it's the surface, the interface with humans is way... For ZE3, you have a defining language for... It's called SMT-Lib It's a very simple language.

It's not meant for humans. It's meant for tools. It means Zetri is used as the back ends of many different tools. Some program is generating input for Zetree. And people expect a counter example or saying it's impossible, it's unsatisfiable to come up for the country example. The interface is really, really simple, right?

You can use this tree as a command line tool that you pass this file on this very low-level language that's super easy to parse. And you come back if you as or no. And Ling, you have, it's a programming language, you have libraries, you have matches, you have mechanisms, you have interactivity, you have user interface, you have LSP, you have build system, you have G, you have that. It's so vast. That's another challenging part for me. As I mentioned, Z3 was a back end. The Z3 users are very sophisticated software developers.

People that speak the same language I speak. It's way easier to talk to people that speak the same language. With Lean is completely different, right? The first users are all math people. They have a completely different background, different expectations, different everything, and different community. And then you have people that you want to use Lean as a programming language.

I'm not a programming language person. My backgrounds automated reasoning. And yeah, it's different language, different expectations. Was there like a singular component that was just really technically challenging? I told you that Lin's implemented in Lin. Of course, it was not always like that, right? I mean, it had to be implemented in something else at the beginning. The switch from originally was CC++.

The switch from C6 plus to Lean was extremely painful. Really, really. I remember I literally want to cry. When I managed to compile Lean with Lean, I was just Sebastian Ulrich and I at the time were building Lean 4 together. But this was before we had a nonprofit. I remember calling him and I said wow man it's insane I mean say are you not excited he said yes I am I am I mean I'm I mean I'm super excited what made that switch hard the first thing is imagine you're going to implement

the language in itself the first thing you want is to reduce to minimize number of features as much as possible is that you want to implement Lin using bare bones features because you're going to have to be able to compile it with itself. Then now you have like 100,000 lines more or less. I don't know the exact number, but it was between 100, around 100,000 lines. And you start trying to compile, you fail the first, you cannot even compile the first file in the pipeline. that more than 1000 and the first one fails. Then you fix the bug, you can compile the first

one. Then you can compile the second and you keep moving and you are always finding discrepancies between the new and the old one. I mean, and you're trying to reconcile, make things easier for the new one

because you want to replace the old one. This process is painful. And Lin is a complicated language because of these dependent types and so on, the proofs. For example, when you're implementing Lean, you still need some proofs there. There are some basic proofs you need. But you have to construct these proofs without no interactivity, nothing.

Bare bones, you have to provide the proof. It's almost like programming in assembly the proof. This was also super painful. Oh, my God. But it took, yeah, many people thought we were going to fail, Sebastian, I would not be able to do it. 100,000 lines is a lot, like all human written. Yes, all human written. We talked a lot about lean, and I know there's competitors to lean.

What are the pros and cons of the different proof assistance? In what scenarios is one preferred over the others, for instance? The first disclaimer I have a completely biased person here, right? But I can tell you what users tell me about. For example, one thing the user's love is the fact that Lean is super extensible.

Because Lean is implemented in Lean. You can add extensions to imagine you're doing your math proof. In the middle of this math proof, I say, oh, I want this fancy automation here. You can write in the same file or the AI can write for you, the extension for automating and approve.

And it will do it. I mean, even the AIs, they know about the fact LIN is extensible. If I ask the AI to isolate an issue in LIN, I give the AI a lien file. It will start writing a Lean meta program, a program about the LIN tunnels, to validate the conjecture it has about why it doesn't work. It's crazy. I mean, it keeps writing lean meta extension there. The fact that Lean is extension is really popular with so many people.

For example, there is Patrick Massou. He's a French mathematician. He wrote something called Lean Verbales. Lin Verbales, he uses for teaching. We have this language for writing the proofs. But he made the language look like English. And he has the info view now is a point and click. You can click there. It gives you suggestions about the next move that's written in Structures English like you find a textbook.

The students has a really good idea on how to write an informal math proof. And he did that without asking me any questions. All this stuff, the point and click, the new language, the new interactivity, he did all by himself. He's not a computer scientist, he has a math degree, and he did all this stuff. And it's for English and French. I mean, you can choose.

I mean, you can write the proofs in French. And looks textbook proof. I mean, there are people that write visualizations, writes for, you're trying to prove something about a math object. You can write an extension that visualize these objects in your info view. There are people that write new domain-specific languages

embedded in LIN for different purposes. For example, for protocol verification, there is a language called Vail. It's a LIN file. You open Vail. You feel like it's a different system for protocol verification, but it's just a LIN file with these extensions for protocol verification.

The language for writing protocols, in a very convenient way. These folks wrote the whole thing without ever talking to us. They only talk to us after they had done it, said, look, I want this part of link to be faster. That was the only interaction we had.

Interactivity is a big deal. Another big deal now is the mathematical library. It's vast. I mean, for stating problems, open conjectures, you need a library. with the concept, to even state the problem, right? So, Lean has a massive library and a massive community.

The community also plays a big role. People, before AI, I think now most people ask questions about Lean to AI, but in the past, people would go to the Lean Zulip channel. Ask a question about Lin, they would get an answer in five minutes. People would say human-based AI. I mean, people would be writing answers instantaneously to your problems. The community played a big role. Another one was, we listened to our users.

The math, I mean, if you talk, for example, Jeremy Fagat was the first user. I mean, he has math backgrounds. He, you ask him, look, he said look I could ask anything any new feature I would get back the same day I mean this the fix the new feature the same day

and this attracts people right I mean because you're making improvements making sure the system does what they wants they come back for more I mean this also has a huge impact in growing the community when I was doing some research

there was this idea I think you mentioned this conversation too. There's this dependent type proof assistance and then there's higher order logic. What is that difference there? At the beginning, when I start to lean, I won't choose higher other logic because it's much easier to implement. I mean, the penthouse is way harder. But the math community, I mean, Jeremy is the one that convinced me that I would never be able to attract serious mathematicians like fields metal level math people with higher logic.

His point is like harder logic is good for concrete math, but if you want to talk about abstract objects, dependent type theory is way more powerful. And it's beautiful. It's easy to explain why is it codependent. For example, you can have a structure in Lean. When you have several fields like x and y natural numbers or integers, let's say they are integers. You can have another field. The type of the field is a proof that X greater than Y. The type of this field is X, let's call greater. Colon, you say X greater than Y.

The type depends on the value of the previous fields. That's why it's called dependence type theory. You can have types that depends on the values of other parameters, other fields, and so on. But the beautiful thing about that, that's in this, you have this very small language that is so expressive. For example, this field now that's a proof. You have to provide the proof. You can do it as an variance. I can only build elements of this type. If I give the X and Y, like in other programming languages, but I have to give a proof that the x is greater than y. It's impossible to construct elements without providing this evidence, right?

You can view this invariance. You don't have to invent invariants, right? It's just the fact you have these dependencies you can express. In the functions, you can have a function, for example, that says it takes x, a y, and a proof that's why is different from zero. Right? It's impossible to call the function if you do not provide evidence that's why it's different from zero. This was always cool.

But in the past, people would say, wow, providing these proofs is really annoying. But with AI now, the AI can't synthesize the proofs for you. And it's really cool. In higher order logic, though, could you express the same? No, no, that's, you cannot, you don't have the, you lose the dependencies. For example, one thing that you cannot do in higher than logic, in Linn, in serious math, people, you have a bunch of structures they manipulate. You have like something, a field, I mean, a ring, a group. You can write a function in Linn that takes a group and returns a new group, a new structure.

you're not money you don't really care about the elements of the structure you are viewing the structure as a first-class citizen that's something that the penitap theory can do easily in higher the logic is you have to play encoding tricks it is a mess I mean some people say oh it works for math none of the mathematicians agree with this statement none I mean you talk to to turnstile to allow Alex Contouravish, Jeremy Avigods, Kevin Buzzards, Patrick Massoud. They would say, no, no, you have to do the penist type theory. I mean, that's another example for me that listening to your users is important. If you want to appeal to this community, it's totally okay to say,

I don't care about this community, but if you care, listening to what they really want is important. So when we think about the future of Lean, I'm curious to hear thoughts on where you think Lean is going, things you're excited about in the future, what might it look like in a few years? Yeah, I think we have this non-profits behind Lean since 2003. I mean, Lin is 13 years old. The first 10 years was a research project. right. Only when we got the non-profit behind the Lean that it became you can view as a product. You have a team of engineers. And we managed to do it because they impact on math. But Sebastian

Oedick and I, I mean, we co-founded this non-profits. What we are really excited about is Lean as a programming language, a programming language where you can prove things about your programs. That's a direction we are pushing really hard, right? Lean 2. We are super grateful for AWS, Amazon. They're making the largest

donations so far to this non-profit, where the goal is to accelerate this path. I mean, Lean is doing super well in the math path, but let's make, Lean is a programming language. Lean is a system for software verification, hardware verification.

Let's push to the extreme. Let's give some love. to this people, to this path that's right now, we do not really have funding to push seriously this path at the non-profits, right? For me, to be in a world where you can reason about your codes is part of my life. I'm not writing units' tests anymore.

I'm writing properties and proving them. The AI is proving most of them for me. This is a direction we are pushing hard. And one thing that people don't realize is that when you have proofs, it enables optimizations for free. You can ask the, for example, if you ask the AI to optimize, you have to inspect the code to make sure no bugs were introduced it in the process. But if the AI is telling you, look, I optimize it, it still computes the same thing.

is the proof. This is a game change in my point of view. Yeah, I've heard multiple people say this decade will be the, you know, the decade of formal verification of software. And yeah, maybe, you know, Lean will be a huge part of that. Yeah, yeah, we for sure, we're super excited to make it happen. And we're, uh, scalability is super important. because there's a big difference between math and software verification. In math, the statements are usually really tiny or small. Fermat's last term is an example. It's super small, but the proof is insanely cheap.

For software verification is the opposite, right? The statements are big, but the proofs are shallow. The reason why this is true is shallow, but you have to manipulate these big objects, right? So for someone who wants to learn more about formal verification or learn more about Lean, do you have a top technical book recommendation? In the Lean websites, I mean, we have several books there

that's introduced Lean, functional programming Lean, theorem improving Lean, mathematics in Lean, The mechanics of proof is great for educational purposes. We have a collection of books. If people go to lean-dashlang.org, they will find all these books there. But one thing I tell people these days is that learning, lean using AI, is super efficient.

I mean, you keep talking to AI in natural language, asking what you want, asking it to write, examples. Many people split the screen in three now, right? We had the link codes, the info view, and on the bottom now, many people now use an AI agent there that's writing the codes and explaining in natural language what's going on there. It's a super effective way. I mean, Terrestal, he told me when he learned lean,

he uses an old version of it was before agents, He would have the chatypchee on one window and the Visual Studio code in the other window and he would copy and paste between them and that's how he learned. But now is even more effective with the AI agents. It's easy to pick up. I mean, just talk to the agent.

Sometimes people say, how do I start? Start talking to the agents. He will help you. He will customize. you can explain what you know already. What's your backgrounds? For example, if you tell, oh, I know Haskell, it's so much easier, right?

You can customize the process. And then last question for you is, you know, if you go back to the beginning of, you know, building C3, building, lean, and give yourself some advice knowing what you know now, what would you say? I'll keep it as secrets. I think ignorance is a bliss.

You don't know how hard things are when you start an adventure. Maybe I'll keep secrets. What I would tell, I think one thing, especially before starting Ling, I'm super introverted. And I would tell, look, you should work on your people's skills. Because it helps a lot. I mean, when you have to interact with a community, with people. For me, it was hard to learn that. And I would tell myself, look, it's really important to have people's skills too.

Well, thank you for your time today. Thank you. Thank you. Hey, thank you for watching this podcast. If you liked it and you want to see the show grow, please support with a comment or a like. Also, if you have any recommendations for people you want me to bring on, please drop a comment. guests like Barbara Liskov, Mike Stonebreaker, Mark Brooker,

these were all people that I brought on because someone left a comment. On another note, aside from the podcast, I'm working on building the ergonomic keyboard that I wish existed. Here's a glance at the prototype. It's a split keyboard. So there's two sides. This is in the case. But yeah, we launched on Kickstarter and we hit our goal within eight hours of launching. I really appreciate it if you were one of the people who grabbed one of the early units.

We're now working on the long-jerkers. journey of building the tooling now. And so if you still want to pick one up, I've left the late pledges open on Kickstarter. So you can grab one there. I'll put a link in the description. Thank you again for watching the podcast, and I'll see you in the next episode.