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

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-done Podcast 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-handwritten Thank 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) Outro Where 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/Leonard41111588 Where 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/@ryanlpeterman Referenced 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

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

• 0:00Ryan Peterman?

  L L M's 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 L L M 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:32Ryan Peterman?

  There's this famous Dijkstra quote I want to start the conversation with. It's that, you know, program testing can be used to show the presence of bugs, but never to show their absence. And in 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?

• 0:59Speaker 01

  Lean's 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 Lean as a platform. You can write code, you can write properties about your codes, and you can prove them.

• 1:30Ryan Peterman?

  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?

• 1:42Speaker 01

  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's a programming language. You can write programs in Lean itself. Then, a Lean program is not that different from a definition you have in math. The techniques are very similar. But when you, if you want to verify programs written in a different programming language, they're basically two different approaches. One of them, they translate, it's called shallow embedding. They translate for Rust. This happens today.

• 2:26Speaker 01

  We have a tool called the N E S that maps Rust into Lean. And you can verify the Lean translation, right? And there's another technique called GIB, where you have the semantics. You write a semantics of the programming language of C in Lean. And now you have a data, 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.

• 2:58Ryan Peterman?

  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?

• 3:13Speaker 01

  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. You can write in Lean that the value of i at this point in your program is going to be greater than or equal to 0 and less than 10, right? You can write that as a mathematical statement, right? Another way to view is that if you can express in math what you care about your program,

• 3:57Speaker 01

  you can verify using Lean, right? That's another way to view it.

• 4:02Ryan Peterman?

  So I have my, my C source files. And then somehow, there's an equivalent Lean proof that's almost like metadata on top of the C program.

• 4:11Speaker 01

  Yes.

• 4:12Ryan Peterman?

  And that's a line by line proof. And Lean will go and check.

• 4:16Speaker 01

  Exactly. People will build automation for automating the process. They're going to use techniques like Hoare 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, right? And they will have a lot of automation to, to process. Make your proof modular, right? I mean, our complexity is a challenge in software verification. Handling the complexity is a big deal. And there are all these frameworks for verifying programs. They're trying to manage the complexity, make your proofs modular.

• 5:00Speaker 01

  Even if A I now, A I can prove things automatically for us, but they have to be modular to the proofs if you want them to scale.

• 5:08Ryan Peterman?

  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:21Speaker 01

  Yes, yes, you can view this way. You can also flip and imagine a future where you're writing what you want mathematically precisely, and A I synthesizing the codes and a proof that's the code that was synthesized meets your specification, right?

• 5:42Ryan Peterman?

  Oh, interesting. So you could start by writing what you want to be true and then

• 5:49Speaker 01

  Ask the A I, please.

• 5:50Ryan Peterman?

  And A I is gonna just go and hammer at it till the Lean proof says you're good.

• 5:55Speaker 01

  Yes, 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, she, a few months ago, she started a project I thought was, was, six months ago, I would say it's not possible at all. She said, we have Z Lib, this C compression library written in C. And she says, she creates a very complicated prompt for A I saying, I want you to translate to Lean, ensure the Lean version passes the test suite for Z Lib. Then I want you to prove that if you compress data and you decompress,

• 6:40Speaker 01

  you get the original data back. It's a really strong property, right? And believe it or not, the A I, 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 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 original. I mean, it's real.

• 7:16Ryan Peterman?

  I mean, it's, I mean, it's crazy. And I hear in the industry, a lot of people, they use a really comprehensive test suite coupled with A I to do some really amazing rewrites because they have some more confidence that the rewrite is accurate and the A I can check itself. And it sounds like a specification is even better than a comprehensive test suite.

• 7:45Speaker 01

  Yes, yes, because with, 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 it is, you may have a really cornered 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, to ensure they are true. But they are checking with testing, right? But now we can prove them.

• 8:30Speaker 01

  And you'll say, look, there's no point testing anymore. I prove it.

• 8:34Ryan Peterman?

  It seems like having a, 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, you know, how much more work is it to come up with a great specification?

• 8:58Speaker 01

  There is a lot. I mean, the programs, in many, 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. Properties, usually their properties are very clear in your minds. Another thing that I tell people to keep in mind is that an inefficient program can be viewed as a specification. Usually, writing an efficient 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.

• 9:41Speaker 01

  And you ask the A I, 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 that specifications are always easy to come up with. But properties, usually the developers have good ideas about properties they care about. An inefficient program is a spec, right? You can view it as a specification. And the technology, formal verification complements testing, right? I think your quote from Dijkstra captures perfectly.

• 10:21Ryan Peterman?

  And I think I saw this on Twitter because Jane Street was more heavily investing in formal verification.

• 10:28Speaker 01

  Yes.

• 10:29Ryan Peterman?

  And I read their post and they talked about this. I think it was a sell for some software that was entirely formally verified.

• 10:38Speaker 01

  Yes.

• 10:38Ryan Peterman?

  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:48Speaker 01

  Your example, sell for, is a great example. This was a major milestone. It's a micro kernel they verify. Done manually, was before A I. This project was done before A I was a big deal. And it's a lot. The cost is super expensive, right? At S A W S, we have been using formal verification for decades, but only for the super safe and critical components because it's expensive until now, right? With A I, it changes the game.

• 11:21Speaker 01

  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. Imagine, you know, I I've seen people complaining that, oh, I I changed the program right now. I have a bunch of failures in my test suites and I have to patch, go one by one. Imagine if proofs is the same process. You have to fix the proofs. Uh, sometimes you don't remember anymore why the proof, what what's the story behind this proof is a lot, but we AI is extremely good at proving,

• 12:06Speaker 01

  uh, writing formal proofs, maintaining formal proofs. For example, yesterday I I was

• 12:15Speaker 01

  changing something in Ling. I want to modify some proofs for technical reasons. And I didn't even know what the proofs were about. Someone else wrote, then I said, look, I want you to, I asked AI, rewrite these proofs without using this feature because I'm going to change it. I don't want to break the libraries. It's tempestuous. 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 was almost like, if your program took X amount of time to do the formal verification in the past, it would take ten X. That would be normal.

• 13:00Speaker 01

  But imagine if your program is changing. That's something that's really common. Now you have to keep maintaining the proofs true. It's a lot of work. But AI eliminates uh this pain for us.

• 13:15Ryan Peterman?

  You mentioned that Lean is, because I I hear it as a proof assistant, but and then you also said it's a programming language.

• 13:23Speaker 01

  Yeah, yeah.

• 13:23Ryan Peterman?

  Is that typical for proof assistants to be both a programming language and a proof assistant?

• 13:30Speaker 01

  Some of them, especially the ones that are based on dependence type theory, uh, they are like rock and lean. Our programming languages and proof assistants, right? I mean, uh, you can write definitions, uh, like, uh, 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 it is a programming language, but is in that the family of code 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, I mean, but with the support for proofs. That that's a way to to view Lean.

• 14:16Ryan Peterman?

  Are there major use cases where people use it as a programming language but not as a proof assistant?

• 14:21Speaker 01

  Well, the first big use case is Lean is implemented in Lean. We have many of our tooling is implemented in Lean, like the the documentation uttering system called Verso is implemented in Lean. The build system that's called Lake is like Lean make. Lake is implemented in Lean. Uh, at AWS, we have a compiler for AI accelerators. It's half 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, uh, use Lean as a programming language in this project. The proofs are like a a a bonus, right, that you can get the proofs and find problems in the design.

• 15:06Ryan Peterman?

  I think most people are familiar with programming languages and the tool chains they have and but um, what are all the major components that you would need for a proof assistant?

• 15:19Speaker 01

  It's not that difference. I mean, i- if I use two modern programming languages like Rust, the tooling, for example, Lake is is our cargo, right? I mean, uh, you're going to open Visual Studio Code, same way, and I want to get all the intelligence. Uh, one big difference is that we have something called the Info View in Lean. Your screen usually is going to be split in two. You have your your file on the right hand side. You have the Info View that tells you information about your proofs, about your codes, uh, it it is giving you constant feedback about your developments.

• 16:00Speaker 01

  That's basically the main difference, but the tooling versus code, everything works the same way. I mean.

• 16:07Ryan Peterman?

  It seems like a programming language is the the fundamental layer and then there's some additional layer on top that keeps track of that stuff.

• 16:14Speaker 01

  Good, good, good question. Uh, uh, in in Lean, you have definitions that show your program, but you have theorems, yes, statements. Like you're going to say, for example, factorial is always greater than or equal to zero or something like that. Or if you add two even numbers, you get an even number. You 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 as a domain-specific language for writing proofs. In Lean, when you write by, it switches to this domain-specific language.

• 16:56Speaker 01

  And you can, you have steps like simplify my goal, uh, the state of my proof. You can say, oh, apply this rewriting step. Apply, for example, we know that X plus zero 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. You you get immediate feedback and you get this feeling that you said you you keep telling, applying transformations to your proof, step by step. You can see what's happening until you get no goals left. I mean, you are done. The proof is complete. And some people view this process as a game.

• 17:38Speaker 01

  I I have users that told me, you built my favorite computer again.

• 17:44Ryan Peterman?

  That's funny. Is Lean itself verified in Lean?

• 17:49Speaker 01

  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 asking, they keep changing the specification all the time. I want this, I want that. No, add this knob here. It's so it's really hard to have a full specification of it, but the kernel is possible to have a specification. We have a kernel. The kernel that comes with Lean is not verified,

• 18:34Speaker 01

  but there are other kernels that you can use. One of them is implemented by a Mario Carnedo. It's called Lean for Lean. And it's implemented in Lean and he's verifying, it's proving that this this kernel has been verified with respect to the semantics of Lean. These are cool projects, but for us, having multiple kernels is the best way to ensure that your results are correct. I mean, uh, some users implemented their own kernels. We have kernels implemented in Rust, uh, in different programming languages.

• 19:10Ryan Peterman?

  And when you say kernel, what's what's the responsibility or what's the inputs and outputs of that portion?

• 19:16Speaker 01

  Yes.

• 19:18Speaker 01

  In Lean proof checking, it's type checking. These kernels, they are type checking in your programs. I mean, 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 you have a term that has a type and you're checking if the type of this star matches the type that you claim it has. For example, the example of the even numbers. This is a type in Lean saying that's, uh, uh, the sum of two even numbers is an even number. You can write, you can do that. It is exactly a typing in.

• 20:00Speaker 01

  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, and the the kernel will check, it will do this type checking. Uh, the kernels vary between a high performance kernel to, it's like five thousand lines of codes. I mean, the goal of the kernel should be something you can write yourself. Uh, of course, sometimes people put bells and whistles like, uh, one thing concerns people have is like, okay. But how do I know, suppose I wrote Fermat's Last Theorem in Lean.

• 20:42Speaker 01

  How do you know that when you export it, it's really Fermat's Last Theorem, it's not two plus two equals four, I mean. Uh, and people, some external kernels, they write print printers. I mean, they 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.

• 21:06Ryan Peterman?

  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?

• 21:25Speaker 01

  Well, there are so many, I mean, that I thought it was impossible. For, for, for example, getting a gold medal in the International Mathematical Olympiad. A few years ago, everybody thought was impossible. Now, everybody, they, they use it as a benchmark of an easy problem. They say, oh, this is like a IMO problem, I mean, this is easy. But it's not, I mean, these are really challenging problems. Uh, the others conjectures that people close using Lean, AI with Lean also impressed me. Uh, there's this unit distance conjecture for others. First, OpenAI proved using formal, right, uh, uh, uh, was not formal.

• 22:11Speaker 01

  And we have a system now in Lean, it's a website where we call LeanVal, where we collect challenges. Uh, the same Kim Morrison saw this, this, this, this proof from OpenAI. And she puts on LeanVal as a challenge, saying, okay, I want to see someone formalizing. We knew it was huge to formalize it. It's serious math, it depends on. Uh, and Boris Alexey from OpenAI, he did, he submits a one million line proof for, for, for formal proof in Lean for this conjecture. Uh, we estimate, I mean, the, the background math that is needed for the proof.

• 22:54Speaker 01

  We knew it would take months, I mean, for experts to do by hands, I mean.

• 22:59Ryan Peterman?

  How, 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?

• 23:06Speaker 01

  I think it was one month.

• 23:08Ryan Peterman?

  Yeah.

• 23:08Speaker 01

  And after Kim was a few, I think, less than two weeks after Kim puts as a challenge on LeanVal. It took, I think, two weeks to get the, the, or, or less, I mean.

• 23:21Ryan Peterman?

  That's, that's insane.

• 23:22Speaker 01

  Yes, yeah, yeah.

• 23:24Ryan Peterman?

  We talked about verifying programs, but also there's using it directly for mathematics, like in this case. How popular is Lean in, in terms of, um, 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?

• 23:44Speaker 01

  Well, historically, Lean got popular first with math, right? I mean, no, with the beginning of the Lean Mathematical Library in two thousand seventeen. We, we had like a big project called Liquid Tensor Experiments. Uh, it started beginning of two thousand twenty. 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. Uh, he felt like this was one of the most important results in his career. He wants to be sure it was correct. It was done manually, the verification.

• 24:27Speaker 01

  Uh, was a big deal because the team that formalizes led by Johann Komelin. They not only formalize the results without fully understanding it, they do not fully understand the, the proof. Uh, but having this info view helped them, guided them step by step. They 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 you, you, they managed to simplify. It, it's almost like when people do refactoring codes, you start changing the codes.

• 25:10Speaker 01

  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 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 like it's shown, that's not about verifying, but enabling people to work together in large numbers. Because you can trust, you, you don't need to trust someone else's proof, right? They can fill holes for you. Uh, this was, I mean, what attracts a lot of attention from the math community. Then came Terrence Tao, he starts using after this project.

• 25:54Speaker 01

  He has really cool projects with and without AI. And he got addicted, actually. I, 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 Lean and he did a new result he had.

• 26:13Ryan Peterman?

  When you say addicted, you mean, because that game, that like completion engine?

• 26:17Speaker 01

  Yeah, some people, I, I feel, we feel like when I talk to professors that use Lean for teaching. They tell me that the class is more like 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, it's 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 to prove things. It's really easy to get addicted, it gets lost proving things.

• 27:02Speaker 01

  You get this buzz every time you prove something.

• 27:07Ryan Peterman?

  You mentioned the IOI gold medals. How is Lean used in that kind of, uh, I think maybe you're referring to Alpha proof by DeepMind or maybe something else?

• 27:17Speaker 01

  Yes, DeepMind was, they got in two thousand twenty-four, was a big surprise in two thousand twenty-four, they got a silver medal. And now we have gold medals from startups like Harmonic. By Dance got a medal. I never imagined By Dance, they are the, they, 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 proof is really good.

• 27:48Ryan Peterman?

  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.

• 27:57Speaker 01

  Yeah, there's the AI, you can view it like, uh, uh, you have goal that was very popular with AI. The AI is playing the game. I, I told you that many people see Lean as a game. It's the same, I mean, the AI is viewing Lean as a game. They have the statements of what you want to prove. You have the by keywords, now you have a blank fill. Make sure that you have no goals left, right? It keeps applying steps in this game. And seeing the, the state of the board, right? That's the info view changing. And the AI, they use reinforcement learning for, for, for trying to get to, to no goals left. It's a single player game.

• 28:43Speaker 01

  Some people play together these days, but yeah, the AI is learning to play the game.

• 28:49Ryan Peterman?

  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.

• 28:59Speaker 01

  Yes, the problem, yeah, 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, you want to be able to talk about the problems, right? For example, suppose the problem uses the real numbers, you need a definition in Lean. And we have it inside of MathLib, the Lean Mathematical Library. The, the first thing you have to be, you have to be able to write the problems in Lean. And this now, because of MathLib, it's easy part. Uh, 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, to create that has some property.

• 29:45Speaker 01

  But yeah, that's how it is.

• 29:47Ryan Peterman?

  I remember you said one of the first use cases of Lean was, um, 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?

• 30:08Speaker 01

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

• 30:24Speaker 01

  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 we, right now, we don't have evidence they can come up with new math.

• 30:47Ryan Peterman?

  OpenAI, Anthropic, Cursor, and Versel 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 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.

• 31:29Ryan Peterman?

  And I appreciate them for supporting my work and sponsoring this podcast. When I see on Twitter this, you know, major conjecture, they made headway on it. It's that they made headway on confirming something.

• 31:42Speaker 01

  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 do not came up with a new theory or anything like that. They are coming up with a proof, right?

• 32:04Ryan Peterman?

  At what points would you say someone should evaluate formalizing something in Lean?

• 32:11Speaker 01

  I think if it's safe to 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, wow, after I implemented this algorithm, now I understand it's much better.

• 32:41Speaker 01

  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 with proofs. You eliminate this discomfort, right? You can prove it again, or the AI can prove for you, or find a counter example, they

• 33:26Speaker 01

  are good at both things.

• 33:29Ryan Peterman?

  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?

• 33:46Speaker 01

  Oh, I think it will change dramatically, right? We have to keep in mind, the big labs, they almost start training for formal verification Lean 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 pipelines to optimize. The behavior we see today that is already amazing will get way better in the future.

• 34:16Speaker 01

  The costs will reduce. Programming languages like Lean and RAC 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 are the specification level, right? Doesn't really matter how the code has been written. Yeah, I think it will change a lot because of that. At least that's the direction we are pushing Lean to.

• 34:53Ryan Peterman?

  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?

• 35:07Speaker 01

  I think there will be always aspects that is handwritten.

• 35:12Speaker 01

  Some people like to make a proof look, they want to use the proof as an artifact, you communicate ideas to others. I can't imagine, there will always be people polishing, making them super easy to understand for, 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.

• 35:55Speaker 01

  I would be surprised as if there is someone that's completely, AI is not in their workflow somehow, right? I mean, 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 as super painful process. And with AI, it's crazy how it brings you awareness of how many steps are just repetitive

• 36:33Speaker 01

  and there's no creativity, you're just patching things and AI automates removes lots of this pain, right? I mean, I cannot go back to, I'm looking forward to this future you described.

• 36:50Ryan Peterman?

  Yeah, I guess the thing that gives people, and I'm guessing, the discomfort is the worry that if it kept going, then, you know, then we need less mathematicians or less computer scientists or something like that.

• 37:06Speaker 01

  People don't see that AI can bring more people. There's also the specification. I mean, I've seen people saying, oh, we are going to leave AI, we'll come up with new math. But if there's no connection to our worlds, this is some alien thing that's going by itself. You need an interface. For example, we want to build programs because we 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, right? Writing this interface, interacting with the AI.

• 37:49Speaker 01

  The AI will have math libraries and everything to prove things about these, these programs we are writing, these artifacts, this, whatever we are trying to build.

• 38:03Speaker 01

  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 eliminated. We are always going to be there, we're in the interface, right? We are telling them what we want, right? Specifications will be there. I can see people always writing codes. Even, 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 a product is never fun. I can tell you, it's never fun.

• 38:48Speaker 01

  And AI can take over this part, nobody really likes doing.

• 38:54Ryan Peterman?

  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?

• 39:10Speaker 01

  Yeah, I started this really long, it's going to be, yes, 20 years ago, I started this tree. I mean, when I joined Microsoft Research.

• 39:21Speaker 01

  Yeah, the Z3 SMT solver is like a SAT solver, but you have backgrounds, theories, like you have support for arithmetic, for arrays. These are not random choices, right? This is because we use for doing task generation software, for doing software verification. Lean's fully, Z3 is fully automated, is a push button. Although Lean's Z3 are called theorem provers, they are completely different beasts. Z3 is fully automatic, Lean is interactive, has automation, but it's interactive.

• 39:58Speaker 01

  Z3 is not a programming language. It's like you can do, it's more like a constraint solver. It turns out you can prove simple things about it, not, you cannot do advanced math with abstract math. You can solve constraints with Z3.

• 40:16Ryan Peterman?

  What's an example of the inputs to this SMT solver and what you get out from it?

• 40:22Speaker 01

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

• 41:06Speaker 01

  It means it's impossible to execute this path and you are happy. Or it gives you back an example saying, look, with these inputs, you're going to be able to do it. I mean, and people use Z3 for doing software verification.

• 41:22Speaker 01

  But because the problem becomes undecidedal, at that level, you have many universal quantifiers for stating properties about your program. Your pre and post conditions. The solver has heuristics. And it 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 is push-button. But when the property is not trivial, they would come back saying, come on, I know the proof. I mean, why is Z3 can't find it? That's why Lean started, I started Lean to make sure that we would have a system that's really good for software verification, right?

• 42:07Speaker 01

  For five, Z3 was successful for finding bugs. But not so much for software, for proving the absence of bugs. It was never super successful there. But Lean was born to fill this gap.

• 42:25Ryan Peterman?

  You said undecidedal, but in practice, in the real world, if you run it, does it typically terminate?

• 42:32Speaker 01

  Yeah, great question.

• 42:35Speaker 01

  Z3 goes the whole complexity ladder, right? You have sets, you have NP complete, a P-space complete, XP complete. You have the whole, too undecidedal, right? I mean, surprisingly, even for sets, you can write really tiny set problems that are really hard to solve. No set solver 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 steps, right? Everything's bounded, you're not trying to prove.

• 43:17Speaker 01

  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 are not correct by esoteric reasons, right? They are correct because for very simple reasons. I mean, that's why these tools are super effective there.

• 43:46Speaker 01

  Yeah, but when you get too undecidedal, 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, Eminato, like, chooses the name proof instability. Because sometimes if you change the problem, you just flip. I mean, you have A and B, you write B and A, where B and A are complicated formulas. You may fail to prove. And when she was just trying to maintain things, proofs would break.

• 44:27Speaker 01

  If you're using this kind of technology, but with Lean, she switches to Lean and it's super smooth, right? Because you're controlling the proof.

• 44:38Ryan Peterman?

  In the Lean case, why is it so much more efficient?

• 44:43Speaker 01

  Your proof is basically you can use the sequence of steps for solving the problem. In Z3, you can do that, you have only one proof step, solve, right? I mean, you're saying, you have options to solve, flags, but you have very, you don't, you cannot influence what Z3 is going to do. It's much harder to influence this kind of system. In Lean, you can, if you want to give a super detailed step-by-step proof, you can. You can use proof automation like is available in Z3. But you can also break it down step by step.

• 45:25Speaker 01

  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 Lean that it can provide a proof.

• 45:44Ryan Peterman?

  When you were working on Z3 and Lean, what was the most technically challenging part that you had to build for either project?

• 45:55Speaker 01

  I underestimate how much harder Lean is in comparison with Z3. It's always of magnitude harder, I mean. One, I talked to many colleagues about that, why I felt like Lean was so much harder. I think it's the surface, the interface of humans is way. For Z3, you have a defined language for, it's called SMT lib. It's a very simple language. It's not meant for humans, it's meant for tools. I mean, Z3 is used as the back end of many different tools. Someone, some program is generating input for Z3.

• 46:37Speaker 01

  And people expect a counter example or saying it's impossible, it's unsatisfiable to come up with a counter example. The interface is really, really simple, right? You can use Z3 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 with yes or no. And Lean, you have, it's a programming language, you have libraries, you have mechanisms, you have interactivity, you have user interface, you have LSP, you have build system, you have this, you have that. It's so vast, I mean, that's.

• 47:18Speaker 01

  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, it's completely different, right? The first users are all math people. They have a completely different backgrounds, different expectations, difference. Everything and different community. And then you have people that want to use Lean as a programming language.

• 47:59Speaker 01

  You have, I'm not a programming language person, my background is automated reasoning. And yeah, it's different language, different expectations.

• 48:11Ryan Peterman?

  Was there like a singular component that was just really technically challenging?

• 48:18Speaker 01

  I told you that Lean is implemented in Lean. Of course, it was not always like that, right? I mean, it had been implemented in something else at the beginning. The switch from, originally was C++. The switch from C++ to Lean was extremely painful, really, really. I remember, I literally want to cry when I managed to compile Lean from. I was just, Sebastian Urick and I at the time were building Lean4 together. But this was before we had a nonprofit for Lean.

• 49:00Speaker 01

  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 super excited.

• 49:13Ryan Peterman?

  What made that switch hard?

• 49:16Speaker 01

  The first thing is, imagine you're going to implement the language in itself. The first thing you want is to minimize number of features as much as possible. So you want to implement Lean using bare bones features. Because you want to have to be able to compile it with itself.

• 49:37Speaker 01

  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, compile, you fail the first, you cannot even compile the first file in the pipeline. That, the 1,000, 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're 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. I mean, because you want to replace the old one.

• 50:22Speaker 01

  This process is, Lean is a complicated language because it depends types and so on, the proofs.

• 50:31Speaker 01

  For example.

• 50:33Speaker 01

  When you're implementing Lean, you 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 a proof to arm. It's almost like programming in assembly, the proof. Uh, this was also super painful.

• 50:55Ryan Peterman?

  My god.

• 50:56Speaker 01

  Yeah. But it it took, yeah, many people thought we we were going to fail, Sebastian. I would not be able to do it.

• 51:05Ryan Peterman?

  Hundred thousand lines is a lot, like all human written.

• 51:07Speaker 01

  Yes, all human written, yeah.

• 51:10Ryan Peterman?

  We talked a lot about Lean, and I know there's competitors to Lean. What are the pros and cons of the different proof assistants? You know, in what scenarios is one preferred over the others, for instance?

• 51:24Speaker 01

  The first disclaimer, I'm a completely biased person here, right? But I can tell you what users tell me, uh, uh, I mean about. For example, one thing the users 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, you say, oh, I want this fancy automation. You can write in the same file. Or the AI can write for you the extension for automating a proof. And it will do it. I mean, even the AIs, they know about the fact Lean is extensible.

• 52:05Speaker 01

  If I ask the AI to isolate an issue in Lean, I give the AI a Lean file. It will start writing a Lean meta-program, a program about Lean terminals to validate the conjecture it has about why it doesn't work. It it it's crazy. I mean, the AI keeps writing Lean meta extension there. The fact that Lean's extension is really popular with so many people. For example, there is Patrick Masso, he's a French mathematician.

• 52:40Speaker 01

  Uh, he wrote something called Lean variables. Lean variables, you can, he 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 structured English, like you find in a textbook. And so the the the students has a really good idea on how to write an informal math proof. And he did that without asking me any questions. I mean, he all this stuff, the point and click, the the new language, the new interactivity. He did all by himself.

• 53:25Speaker 01

  He's not a computer scientist. He he's 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 uh, the proofs in French. It looks textbook proof. I mean, uh, uh, there are people that write visualizations, writes for. You want to visualize, you're trying to prove something about a math object. You can write an extension that visualizes these objects in your info view, right? There are people that write new domain-specific languages embedded in Lean for different purposes. For example, for protocol verification, there is a language called Veil.

• 54:08Speaker 01

  It's a Lean file, you open Veil, you feel like it's a different system for protocol verification. But it's just a Lean file with these extensions for protocol verification. The language for writing protocols in a very convenient way.

• 54:25Speaker 01

  These folks wrote the whole thing without ever talking to us. They only talked to us after they had done it and said, look, I want this part of Lean to be faster. That was the only interaction we had. Uh, and so interactivity is a big deal. Uh, uh, uh, another big deal now is the mathematical library. Uh, it's vast. I mean, for stating problems, open conjectures, you need a library with the concepts to even state the problem, right? So Lean has a massive library and a massive community.

• 55:03Speaker 01

  The community also plays a big role. People, uh, before AI, I think now most people ask questions about Lean through AI. But in the past, people would go to the Lean Zulip channel. Ask a question about Lean, they would get an answer in five minutes. I mean, uh, people would say, human basis AI. I mean, people would be writing answers instantaneously to your problems. The community played a big role. Another one was we listen to to to our users. I mean, uh, uh, the math, I mean, if you talk, for for example, Jeremy Viegat was the first user. I mean, he has math backgrounds.

• 55:47Speaker 01

  He 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, same day. And this attracts people, right? I mean, because you are making improvements, making sure the system does what they want. Uh, uh, uh, they come back for more. I mean, uh, this also has a huge impact in growing the community.

• 56:16Ryan Peterman?

  When I was doing some research, there was this idea. I think you mentioned this conversation too. There's this uh, dependent type proof assistants, and then there's higher order logic. What what is that difference there?

• 56:29Speaker 01

  At the beginning, uh, uh, when I started Lean, I won't choose higher order logic because it's much easier to implement. I mean, uh, dependent types is way harder, this.

• 56:43Speaker 01

  But the math community, I I I mean, Jeremy is the one that convinced me that I would never be able to attract serious mathematicians, like fields medal level math people with higher order logic, right? His his point is like, higher order logic is good for concrete math. But if you want to talk about abstract objects, uh, uh, dependent type theory is way more powerful. And and it's beautiful. Uh, it's easy to explain why it's called dependence. For example, you can have a structure in Lean. When you have several fields, like X and Y are natural numbers or integers. Let's say they're integers. You can have another field. The type of the field is a proof that X greater than Y.

• 57:28Speaker 01

  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 you have to provide a proof. You can view it as an variance. I can only build elements of this type.

• 58:12Speaker 01

  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? Uh, you can do this as an variance, that's, you don't have to invent invariance, right? The lang, it's just the fact you have dependencies you can express.

• 58:36Speaker 01

  In the functions, you can have a function, for example, that says takes a X, a Y, and a proof that's Y is different from zero, right? I mean, it's impossible to call the function if you do not provide evidence that Y is 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 synthesize the proofs for you. Uh, and it's it's really cool.

• 59:07Ryan Peterman?

  In higher order logic, though, could you express the same?

• 59:10Speaker 01

  No, no, that's, you cannot, you don't have, you lose the dependencies. For example, one thing that you cannot do in higher order logic, uh, in Lean. In in in serious math, people, you have, you have a bunch of structures they manipulate. You have like something, a fields, I mean, a ring, a group. You can write a function in Lean that takes a group and returns a new group, a new structure. You you're not, you 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 penetratory can do easily.

• 59:52Speaker 01

  And in higher order logic, is you have to play encoding tricks, it is a mess. I mean, uh, so some people say, oh, it works for math. None of the mathematicians agree with this statement, none. I mean, you talk to to Terence Staal, to Alex Konturvich, Jeremy Viegat, Kevin Buzzard, Patrick Masso, they would say, no, no, you have to do dependence type theory. I mean.

• 1:00:22Speaker 01

  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.

• 1:00:37Ryan Peterman?

  So when we think about the 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, you know, what might it look like in in a few years?

• 1:00:51Speaker 01

  Yeah, I think we have these nonprofits behind Lean since two thousand twenty-three. I mean, Lean's thirteen years old. The first ten years was research projects, right? I mean, only when we got the nonprofits behind Lean that it became, you can view as a product. You have a team of engineers. And we managed to do it because the impact on math, right? But Sebastian Ulrich and I, I mean, we co-founded this nonprofit. What we are really excited about is Lean as a programming language, a programming language where you can prove things about your programs, right?

• 1:01:34Speaker 01

  That's a direction we are pushing really hard, right? Lean to. We are super grateful for AWS, Amazon, they're they're making the largest donation so far to this nonprofit, where the goal is to accelerate this path. I mean, Lean's doing super well in the math path, but let's make Lean as a programming language, Lean as a system for software verification, hardware verification, let's push to the extreme. Let's give some love to these people, to this path that's right now, we do not really have funding to push seriously this path, that's the nonprofits, right?

• 1:02:17Speaker 01

  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 people, one thing that people don't realize is that when you have proofs, it enables optimizations for free. You can ask the, for example, today, if you ask the AI to optimize, you have to inspect the code to make sure no bugs were introduced in the process.

• 1:02:56Speaker 01

  But if the AI is telling you, look, I optimized it, it still computes the same thing, here's the proof, this is game changer in my point of view.

• 1:03:10Ryan Peterman?

  Yeah, I've heard multiple people say this decade will be the, you know, the decade of formal verification of software and yeah, maybe Lean will be a huge part of that.

• 1:03:23Speaker 01

  Yeah, we for sure, we're super excited to make it happen. I mean, we are, scalability is super important, right? Because there's a big difference between math and software verification. In math, the the statements are usually really tiny or small. I mean, Fermat's Last Theorem is an example, I mean, super small, but the proofs insanely cheap. For software verification, it's the opposite, right? The statements are are are big, but the proofs are shallow.

• 1:04:02Speaker 01

  The reason why this show is shallow, but you have to manipulate these big objects, right?

• 1:04:09Ryan Peterman?

  So for someone who wants to learn more about formal verification or learn more about Lean, do you have a top technical book recommendation?

• 1:04:21Speaker 01

  In the Lean websites, I mean, we have several books there that introduce Lean, functional programming Lean, tier improving Lean, mathematics in Lean, the mechanics of proof is great for for educational purposes. We have we have a collection of books. If people go to lean-lang.org, they will they you'll find all these books there. But one thing I I tell people these days is that learning Lean using AI is super efficient. I mean, you you keep talking to AI in natural language, asking what do you want, asking it to write examples.

• 1:05:05Speaker 01

  Many people split the screen in three now, right? We had the Lean 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, Terence Stowe, he told me when he learned Lean, he uses old version, it was before agents, he would have the chat P T 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 it's even more effective with the AI agents.

• 1:05:49Speaker 01

  It's easy to pick up, I mean, just talk to the agent. Sometimes people say, how do I start? Start talking to the agent, he will help you, he will customize, right? You can explain what you know already, right? I mean, what's your backgrounds? For example, if you tell, oh, I know Haskell, it's so much easier, right? You can customize the process.

• 1:06:15Ryan Peterman?

  And then last question for you is, you know, if you could go back to the beginning of, you know, building C three, building Lean, and give yourself some advice, knowing what you know now, what would you say?

• 1:06:28Speaker 01

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

• 1:07:07Ryan Peterman?

  Well, thank you for your time today. I really appreciate it.

• 1:07:09Speaker 01

  Thank you.

• 1:07:10Ryan Peterman?

  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 Liskoff, 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 journey of building the tooling now.

• 1:07:54Ryan Peterman?

  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.