Leonardo de Moura discusses the integration of AI in formal verification through the Lean theorem prover, highlighting challenges like ensuring proof soundness via trusted kernels and the balance between a stable core and an innovative community. He envisions AI as a powerful tool for automating tedious verification tasks and accelerating software development, while emphasizing the continued necessity of human oversight, creativity, and incremental learning in advancing formal methods.
In this insightful discussion, Leonardo de Moura, the creator of the Lean theorem prover, addresses the challenges and opportunities presented by AI-generated formal proofs. He recounts a recent incident where an AI-generated proof claiming to disprove the Collatz conjecture exploited bugs in Lean’s core and an external kernel called nanoda. This event highlighted the vulnerabilities in formal verification systems and underscored the importance of maintaining a small, trusted kernel and multiple independent kernels to ensure soundness. De Moura emphasizes ongoing efforts to improve security, including simplifying kernels, proving their correctness, and integrating automated tools like comparator to detect false proofs.
De Moura elaborates on the governance model of Lean’s development, explaining the balance between a controlled “cathedral” core system and a vibrant, creative community that builds extensions and libraries independently. He values transparency and rigorous prioritization in core development to avoid chaotic feature additions that could compromise system integrity. The extensibility of Lean allows users to create domain-specific languages and tools without altering the core, fostering innovation while preserving stability. This model has enabled significant community contributions, including advanced software verification extensions demonstrated by researchers.
The conversation also explores the evolving role of AI in formal verification and software engineering. De Moura shares a remarkable example where AI successfully translated and verified the compression algorithm zlib in Lean, outperforming traditional implementations in some respects. He envisions AI as a game-changer capable of handling low-level, detail-oriented tasks that humans find tedious, accelerating the development and verification of complex software. However, he acknowledges that AI currently excels at combining existing knowledge rather than inventing fundamentally new techniques, suggesting a complementary relationship between human creativity and AI efficiency.
Regarding the future of Lean and formal verification, de Moura highlights ongoing challenges such as scalability, performance optimization, and reducing the trusted code base by verifying compilers and other components. He foresees Lean evolving into a platform that supports massive mathematical libraries and software verification projects, aided by AI to manage growth and maintain performance. The community is actively discussing modularizing the extensive Mathlib library to handle its increasing size and complexity. De Moura is optimistic about Lean’s longevity, supported by a dedicated nonprofit organization and a growing user base that includes prominent mathematicians.
Finally, de Moura reflects on the nature of understanding and creativity in AI and humans. He notes that while AI models demonstrate impressive competence in specific tasks, they lack experiential learning and deep comprehension, often relying on reproducing existing knowledge. He suggests that future advancements may involve AI systems capable of learning by doing and adapting their internal representations. Despite rapid progress, human oversight remains crucial, particularly in specifying goals, maintaining trust, and guiding AI development. De Moura encourages new users to approach Lean incrementally, leveraging AI assistants to ease the learning curve, and expresses confidence that humans will continue to play a meaningful role in formal verification and software engineering alongside AI.