Skip to content

When you keep AI Lean, you keep AI correct

August 28, 2026 · 25 min

Show notes

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 complements probabilistic AI models, and the use of AI for continuous code optimization.

Episode notes:

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.

See Privacy Policy at https://art19.com/privacy and California Privacy Notice at https://art19.com/privacy#do-not-sell-my-info.

All episodes of The Stack Overflow Podcast

Settings

Display

Language

Decides which stations you see first on the home page.

History

Recently played stations and episodes and your latest searches are only stored in this browser.

Notifications

A short notice when a podcast you follow has a new episode. Turn off single podcasts with the bell on their page.

Account

Save favorites – in the app and on the website.

Keyboard shortcuts

/
Open search
Space
Play or pause
← →
In the player: back 15 s, forward 30 s (episodes) · in a row: next tile
↑ ↓
In a row: target within the tile
Home / End
In a row: first or last tile
Esc
Close window or menu
?
This overview
Now playing

Go to station page

Play next

    Add episodes with “Play next” – they play after the current episode.