Leonardo de Moura explains how Lean combines an extensible ecosystem with a deliberately controlled core. He describes a purported mathematical proof that apparently exploited different bugs in two checkers, showing why a green acceptance signal is not enough when the implementation itself is unsound.
Leonardo de Moura advocates independent, transparent kernels and stronger proofs about the tools that verify other proofs. He describes AI-assisted translation and verification of compression code as a promising example, while stressing that correctness concerns the property specified, not every desirable behavior.
Leonardo de Moura and Tim Scarfe discuss how changing requirements, library infrastructure and human expertise shape formal software development. Models can be excellent at narrow proof and optimization tasks yet still make basic mistakes or struggle to invent genuinely new techniques.
The future work includes scaling mathematical libraries, improving Lean as a programming language and reducing trust in compilers and checkers. Leonardo de Moura expects people to remain responsible for specifications and problem selection, and recommends that beginners start by writing ordinary Lean programs before attempting proofs.
Watch on YouTube
