AI Can Write the Proof. Who Checks It? — Leonardo de Moura

Lean creator Leonardo de Moura explores the intersection of formal verification, software engineering, and artificial intelligence. The discussion centers on the evolution of Lean from a centralized project to an extensible platform capable of supporting massive mathematical libraries. AI significantly impacts this field by automating complex, low-level proof tasks and identifying vulnerabilities, which necessitates a multi-kernel approach to ensure system integrity. By leveraging dependent type theory, Lean provides a robust framework for capturing software invariants and preconditions. While AI excels at solving specific, well-defined problems, human expertise remains critical for setting research roadmaps, defining specifications, and distilling abstract mathematical structures. Future development focuses on scaling Lean to handle millions of lines of code and verifying the compiler itself to minimize the trusted code base, ultimately making formal verification a standard, invisible component of modern software development.