When AI Writes the Code, Who Proves It Works?
Summary
The episode features Leo de Moura discussing Lean, a programming language and theorem prover, and how AI-enabled formal verification could transform software engineering. It covers autoformalization, trusted kernels, and the shift toward specification-driven development and the verified software stack. The conversation also explores implications for math, physics, and finance, and the practical challenges of trusting AI-generated proofs.