Lean is a functional programming language and proof assistant that allows developers to write programs and verify their mathematical correctness within the exact same system.
Connect with Leo on LinkedIn and check out his many badges on Stack Overflow.
Congrats to Populist badge winner Peter Lawrey for winning the badge on their answer to Check two float/double values for exact equality.
TRANSCRIPT
[intro music]
Ryan Donovan: Hello and welcome to the Stack Overflow podcast, a place to talk all things software and technology. I am your host, Ryan Donovan, and today we are talking about proving correctness in AI agents with the Lean Language. So my guest for that is Leo De Moura, who is the Senior Principal Applied Scientist at AWS and also the creator of the Lean Language. So welcome to the show, Leo.
Leo De Moura: Thank you very much. I'm happy to be here.
RD: Happy to have you. Before we get into the discussion of Lean, let's get to know you a little bit. How did you get into software and technology?
LDM: Oh, I started when I was really young. I love computers. I love to program. With 12 years old, I was already writing games, computer games.
RD: And obviously, you went from a 12-year-old making their own games to writing a mathematical programming language.
LDM: Yes.
RD: That's a little bit of a jump.
LDM: Yeah, yeah. I started first working on a technology that's called model checking. It's more for finding bugs in protocols and so on. I made a move to working on automated provers. And then I moved it to interactive, to Lean. It's a programming language and a proof assistant. And you can do math. You can verify codes. Everything in the same system.
RD: The Lean programming language. Can you talk about what it is? My understanding that it is to sort of formalize proofs.
LDM: Yeah, you can write regular programs. At AWS, people use, for example, for implementing a compiler for training. Our AI accelerator ship, parts of this compiler is written in Lean. It's a programming language. But you can also write mathematical proofs. If you're a mathematician, you can use it only for proving theorems and defining mathematical objects. But if you're a developer, you can write your codes and prove your codes correct in the same system.
RD: So when I've talked to other folks talking about proving correctness and stuff with the programming language, it's generally a sort of functional programming language.
LDM: Lean is a functional programming language, but it's also used for verifying, for example, Rust code. It's not limited to code that's written in Lean. It's also used for verifying code written in other programming languages.
RD: Oh, okay. So you can have a Lean library that you can call from other places.
LDM: Yeah. Well, in this case, it's more like to verify Rust code, you translate. There's a tool called Aeneas that translates Rust into Lean, and you do the verification in Lean after that.
RD: And there you're verifying the correctness of the actual code.
LDM: One thing that's important to keep in mind when you're using Lean, you're responsible to specify what correct means. One misconception people have about Lean is that you're going to write your program, press a button, prove it correct. What correct means, right? It means different things for different programs, right? A good example is a compression library. We all have used something like Zlib to compress a file. One key property you want is if you compress a file and you decompress the file, you get the original file back. If you don't, it would be a disaster, right? And you can prove that that's indeed the case. And I think most users of your compression library will want this property, right?
RD: Yeah, yeah. They definitely want their old file back, yeah. So compression is an algorithm. So how do you verify the correctness of the file using that algorithm?
LDM: The first thing you're going to do is state this in Lean. You're going to say for all data, for all compression levels, if you compress a single line in Lean, you're going to say if you compress and then you call the decompression function, you're going to get the original data back. But the proof can be extremely long. But in this case, the statement of the property you want is very compact. And proofs can be done using the same techniques mathematicians use to prove hard theorems, like Fermat's theorem, you name it.
RD: Do you have a background in math for this, or did you do math for fun?
LDM: Yeah, math for fun. I'm a computer scientist. I like to code. I know math, but I do not have a math degree. I have a computer science degree, all my education in computer science. You learn a lot of math, but I'm not a professional mathematician.
RD: So with your work with AWS, you're using it to prove AI agent functionality. Is that correct?
LDM: It's using many different places. For example, one of them, since you mentioned agents, we have a system called the AgentCore. AgentCore, you can put boundaries on what the agents can do using a language called Cedar. Cedar has been verified using Lean. We want to check that Cedar has key properties. Like if you say something is not allowed, it is indeed the case. You want to say, for example, if you have a policy, it should evaluate to true or false at runtime. And they want to prove that for any policy you can write, if the system accepts your policy at runtime, it will evaluate to true or false. And the CIDA designers did exactly that using Lean.
RD: I read something recently that was basically your guardrails, unless you're blocking something, if you're using like a prompt guardrail, it's going to be ignored. So how does it stop an AI agent from taking an action?
LDM: You can write policies. You can specify what the agent is allowed. You can view it as a domain-specific language for setting policies. At runtime, these policies will be enforced to your agents, right?
RD: I think a lot of people talk about AI agents, AI in general, as being a very non-deterministic system, right? Lean sounds very, very deterministic.
LDM: Yes, exactly.
RD: How much are they fighting when they're working together?
LDM: I think they complement each other. The fact that agents, large language models are probabilistic is a strength. They do amazing things all the time. In many cases where they surprise it. But as you said, they can hallucinate, they're probabilistic. And we've automated reasoning, the nice things that you can prove with your agents in decisive codes. For example, if your agent synthesizes codes, you can prove whether the code has the properties you want. And you can even go one step ahead. And people are already doing that today. You can ask the agents. We have the compression example I just told you. You can ask the agent, implement Zlib for me, this compression and decompression functions. But you have to also write the proof that this property holds, you're asking two things, both things, right? At the end, Lean will check whether the proof is correct or not. If it's not correct, the agents will have to try to keep trying. I mean, we will not accept the solution. They work together. The agent can be creative. It would be really hard to implement a program that would synthesize this kind of program automatically, but the agents can do it. It feels sometimes like magic, but the powerful automated reasoning that we can put these controls, these guardrails, that you say, look, you can do your magic, but you have to come back with a certificate that you did what I wanted. This is powerful. Imagine that the agent succeeds, implements the compression, but you're not happy with the performance. You can ask the agent, keep optimizing. Keep improving. Keep trying to implement a more efficient version. But you have to keep proving that it's correct. It feels like science fiction, but this is happening today. A friend of mine, Kim Morrison, we worked together. She did exactly that. It's this exact experiment. Kept asking the agent, keep trying to improve the performance. It kept improving, improving, improving. But always proving that it's correct. You can try wild optimizations that we sometimes don't have the patience to do it. It's too boring, it's too time-consuming, but the agent has infinite patience.
RD: With the sort of infinite optimization there, does the proof have to change?
LDM: It will change. And that's why in the past, when these proofs had to be written by hands, put yourself in the position of the developer. They wrote the program. Now you're asking them to optimize the program, to modify the program. And imagine if they had to write the proof too. Really, they would have to keep updating the codes and updating the proof. And you keep asking them, no, I want faster. It's too time consuming. Very few people would do it, but the agents are happy to do it.
RD: I imagine there are more than a few people listening who may not have an idea of what a proof for a sort of agentic algorithm would look like, right? Like, how do you formalize, you know, in agentic engineering, it's often a very sort of broadly specified, you know, using English to do it.
LDM: It's really important. Do I have to learn to write formal statements? Our answer is you have to learn how to read them. And learning how to read is much easier than learning how to write. Because to read a formal statement in Lean, you have machine assistance. You can click on things and ask for explanations. You can ask the AI to explain to you. Of course, you should not trust because the AI can hallucinate in the explanation, but they can help you. They can point you to the exact documentation you should read to understand the formal statements. But a common workflow today is to interact with the agents, right? Tell the agents in natural language the specification. What do you want? And the agent will write in Lean for you. There are people that solve it. Open conjecture in mathematics without using Lean, without knowing Lean. They talk to the agents in natural language. The agents write the specification. They read the specification and say, yes, this is what I want. And after that, you can fire the agent saying, look, implement the program. Prove that it meets my specification and keep going, keep optimizing, keep making it better, right?
RD: That's good you say people have to learn how to read the formal proofs. At some point we're talking, I'm thinking like, oh, the agents are just checking themselves, right? They're just like patting themselves on the head like, oh, I did it. Look at my formal proof. You know, always the sort of risk with AI generated tasks too, where I've heard them just saying, like, assert true at the end.
LDM: It's much easier than curating the proof, coming up with the proof. We have multiple checkers in Lean. We have tools to check. For example, if the AI is trying to trick you. For example, one way to trick you is adding an axiom, making an assumption that's false. It's saying, I proved what you want, model this assumption here. But this assumption is false. You can prove anything from this assumption. And we have tools to detect if the agent is trying to trick you in this way. And it's a good point. I get these days proofs. People reaching out saying, I proved the Riemann hypothesis using Lean. Common failure modes. The formal version is not the Riemann hypothesis. There's a mismatch between their intent and what the agent wrote. Prove something that looks like the Riemann hypothesis, but it's not. Another failure mode is, I proved everything. There's only one piece left. Another failure mode is, prove it, model this extra assumption. That's trivial, believe me. This is a trivial assumption, but it's not. But these are real failure modes that people should be aware. And agents will try to trick you in believing something is not true.
RD: With a sort of formal proof of agentic behavior, what's possible now that wasn't before?
LDM: I think it's to give more independence to the agents. Another thing you don't, for example, this optimization example I gave you. In the past, you could have asked the agent to optimize your code, but then you would have to check if the code is still correct, if it still makes sense. You can skip. I think you get productivity. The peace of mind that you do not have to check whether the code is correct or not, I think that's the main win. And productivity, right? I mean, you can keep asking the agent to keep optimizing your codes. You don't have to spend time doing this kind of task anymore.
RD: Yeah, I mean, even before current generation of AI, AI came up with weird, unexpected solutions, right? I could see AI optimizing code, like, you know, optimize it. And it's like, all right, this database is now a variable, right? That's faster.
LDM: They come up with wild optimizations sometimes. And a friend of mine the other day was different hardware. They have special instruction sets sometimes that nobody uses because it's hardware specific. But now one thing he was doing is specifying what these instructions do and asking the agent, look, try to optimize using these instructions that nobody uses, but let's try to put them to good use. And they succeed doing that. Something that, as a human, you would say, oh my gosh, I will not implement 20 different versions for 20 different hardware.
RD: And, you know, that's a good point. I assume with a proof, it would apply across all the hardware versions or languages, right?
LDM: Yeah, and you can have a different proof for each hardware, right? Because you're going to use different instructions, they have different semantics, and you're going to have a different proof for each case. It's okay. I mean, as a human, we would not want to write the same thing 20 times in slightly different ways, right?
RD: Yeah, and, you know, upgrades, especially language and dependency upgrades, are always a huge pain in the butt. I know at AWS, you had a great use of AI agents upgrading the Java and the code base Deepak Singh was on. He said it saved something like 100,000 years of developer time.
LDM: One thing that happens in Lean is when we modify Lean, sometimes we have to update the libraries. The mathematical library is huge in Lean, and you have to adjust it. One year ago, these adjustments were done by hand. We have a team of people that would be there manually patching things and doing mechanical changes. But with AI, we cannot fully automate the process nowadays. Human supervision to see if AI doesn't... I mean, sometimes the proof is correct, but it's not pleasant. Believe it or not, many people want to read the proofs and understand for learning purposes. And they want a proof that is readable, that's approachable. And we don't want like a hackish proof even if it is correct, in some parts of the library. And now AI helps us to maintain the libraries. I mean, it's a huge time save.
RD: For those AI updates of the libraries, do you have a proof that verifies that the libraries are correct?
LDM: Oh, yeah, yeah. They always check it, always.
RD: I wonder, is this... sort of new testing pipeline, right? People do sort of end-to-end unit tests. Do they now need to do a sort of proof?
LDM: Yeah, well, the great thing about proofs, when you prove property-based testing, you mentioned property-based. Property-based testing is great, I mean, but you are testing for a finite number of examples. With proofs, you can show the property holds for all possible inputs. This is powerful. But there is wrong. I'm not discarding tests. There's a role for testing, right? For example, in Lean, when you write code in Lean, there are things that we are not going to be able to talk about that are outside of the logical framework. One of them is memory consumption. This is one kind of thing. We will run tests to show the memory consumption is reasonable when you're executing the program. There is a role for testing. And it's always good to test before you waste time trying to prove something that's not true. We have tools for finding dummy bugs. I mean, sometimes you have stupid mistakes we have done. Testing is great to catch them before you try to prove something.
RD: The memory consumption example is interesting. Are there things that a proof can't catch?
LDM: You can have a model of a programming language where you even talk about the memory, the memory is explicit. It's like it's a much lower level model where you talk about memory, stack space, everything's explicit. You're in a very low level of abstraction. If you do that, you can even prove properties about the memory consumption, the amount of stack space we're going to need, then this is in reach. But when you’re working with a higher level of abstraction, like when you're working with Lean as a programming language, there's no way to talk about memory at this point, because it's completely abstract. The functions look like mathematical functions, and you will not be able to talk about memory. There's no concept of memory. There are applications where memory consumption matters. And usually for this kind of program, we are going to write using a lower level language with a model where the memory is explicit, stack is explicit, and you can talk about all these things.
RD: With any level of abstraction, you're losing information on it. And it seems like to get the full information, you almost have to rebuild the program itself within Lean. Is that accurate?
LDM: The advantage of using Lean as your programming language is that Lean was designed for proving, right? It's a language that is much easier to prove your programs to be correct if they are written in Lean because the language was designed for that. But you are in a much higher level of abstraction. You are not going to be able to talk about memory consumption, for example. But the same way you can verify Rust programs, there are people that verify assembly codes in Lean. You can write a model of assembly. RISC-V or x86, you can write them in Lean. And one thing that is important is that your proofs are correct. If your model of the x86 is faithful, reflects the real hardware, right? This is part of what you are trusting. You're saying, look, this mathematical model of the x86 reflects exactly what Intel built. But if it is, your proofs... you can use it to reason about assembly codes in Lean.
RD: How hard is it to get a proof of assembly code? Like how much do you have to build for that sort of simulation of the hardware?
LDM: At AWS, we have experts that verify cryptography written in assembly codes. They are special people. They have years of experience verifying cryptography written in assembly codes. But the good news now is that AI is really capable of writing these proofs for us. It's our belief that this is going to become mainstream because AI will write these proofs in the future for us. For example, one year ago, I would tell you science fiction, but now it's feasible. You can write a specification mathematically in Lean, and you can ask the AI, write an assembly code. And I have here the model of the x86. Using this model, prove that your program meets my specification. There are people doing that. This already is going to keep happening more and more often. I mean, we are just seeing the beginning of what people can accomplish using proof assistance. We could have been doing that in the past, but it was so time consuming. The same AI that produces hallucinations is capable of writing these proofs that would take lots of efforts in the past.
RD: Right. You still have to read them and verify them, right?
LDM: Yeah, but the verification, after they write the proof for us, the verification is not a bottleneck. The bottleneck is finding the proof, checking the proof. I can give you a concrete number. The mathematical library has 2.4 million lines of link. We can check it in 22 minutes, the whole thing. So checking the proofs is way faster than finding these proofs.
RD: You know, you said we're at the beginning of this with proofs. Are there sort of use cases you're excited to see tried out? Are there things that have surprised you as they've been tried out?
LDM: Oh, yeah, yeah. I'm excited about the optimization. Supported to write your code. People debate whether writing specifications. Oh, I don't know how to write a specification. I don't even know the properties. But imagine the scenario you write an inefficient program. We all agree that writing an inefficient program is way easier than writing a super optimized one. You don't have to keep spending time in fancy data structures and algorithms. You implement just the most naive implementation. And now you can ask the AI to write the efficient version, but you have to prove that computes the same thing as my inefficient version. I'm excited about this kind of scenario where just asking the AI, optimize my code, but you have to prove it still computes the same thing. So much time is spent on testing because it's a disaster if there's a bug in the hardware. I think we can accelerate the time you design, in the time you manufacture can be compressed dramatically with this technology. It's really cool that you can prove things, but what excites me the most is the ability now to optimize your hardware, optimize your software without introducing bugs right in the process.
RD: And not having to handcraft that proof yourself.
LDM: Yes, I will probably not do it. I mean, the optimization. It's common. I have so many colleagues that have been through this. The dilemma is like they don't want to optimize because they would have so much effort to get it right. And now if you try an optimization, you're going to have to do everything again. And they say, oh my God, the optimization doesn't pay off the cost of doing all this process again. But if you could get the proof for free, I mean, you're not doing it. The AI is doing it. Why not? And you can try more ideas in parallel. I mean, I have friends that try 10 ideas. They ask the AI to explore different ideas. They can do that because the AI is proving whether the idea will work or not. I can see this acceleration happening. It's a super great time to be alive. I mean, one year ago, this was not possible.
[music]
RD: It is that time of the show again where we shout out somebody who came onto Stack Overflow, dropped some knowledge, shared some curiosity, and earned themselves a badge. Today we're shouting out the winner of a populist badge, somebody who dropped an answer that was so good it outscored the accepted answer. So congrats to Peter Lowry for answering “check to float slash double values for exact equality”. If you're curious about that and you don't have a mean to do the proofs, we have the answer for you. I'm Ryan Donovan. I host the podcast, edit the blog here at Stack Overflow. If you have questions, comments, concerns, you can email me at podcast@stackoverflow.com. And if you want to reach out to me directly, you can find me on LinkedIn.
LD: [indistinct], I'm Leo De Moura. I'm a Senior Principal Applied Scientist at AWS. I'm the creator of Lean and the chief architect of the Leanflow. Very happy to be here. And I have many badges on Stack Overflow.
RD: Well, thank you for listening everyone. And we'll talk to you next time.
[outro music]