Aug 28, 2026 · 25 min · 9 segments
Ryan chats with Leo de Moura, Senior Principal Applied Scientist at AWS and the creator of the Lean language, about proving correctness in AI agents with the Lean language, how automated reasoning…
Leo de MouraGuestRyan DonovanHostWith a sort of formal proof of agentic behavior, what's possible now that wasn't before?
Uh, another thing you don't-- For example, this optimization example I gave you.
In the past, if-- 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.
I think you get productivity, the peace of mind that you do not have to check whether the code is correct or not.
And productivity, right? I mean, you can keep asking the agent to keep optimizing your codes.
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.
Different hardware, they're, they have a special instruction set sometimes that nobody uses because it's hardware specific.
But now he-- 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.
I mean, something that as a human, you would say, "Oh my gosh, I will not implement twenty different versions for twenty different hardware."
I assume with a proof, it would apply across all the hardware versions or languages, right?
And, and you can have a different proof for each hardware, right? Because you're, you're going to use different instructions.
They have different semantics, and you're going to have a different proof for each case.
I mean, a-as a human, you would not want to write the same thing twenty times in slightly different ways, right?
With a sort of formal proof of agentic behavior, what's possible now that wasn't before?
Uh, another thing you don't-- For example, this optimization example I gave you.
In the past, if-- 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.
I think you get productivity, the peace of mind that you do not have to check whether the code is correct or not.
And productivity, right? I mean, you can keep asking the agent to keep optimizing your codes.
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.
Different hardware, they're, they have a special instruction set sometimes that nobody uses because it's hardware specific.
But now he-- 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.
I mean, something that as a human, you would say, "Oh my gosh, I will not implement twenty different versions for twenty different hardware."
I assume with a proof, it would apply across all the hardware versions or languages, right?
And, and you can have a different proof for each hardware, right? Because you're, you're going to use different instructions.
They have different semantics, and you're going to have a different proof for each case.
I mean, a-as a human, you would not want to write the same thing twenty times in slightly different ways, right?
The rest of this transcript — segmented and speaker-labeled, so you land on the exact moment something was said
Search every transcript — by keyword, by phrase, or by meaning, across every show Radar indexes
Trends — what is surging across podcasts, measured against its own baseline
Alerts — when a name you follow appears in a newly indexed episode
No account is needed to search Radar.
