AI Can Write the Proof. Who Checks It? — Leonardo de Moura
Leonardo de Moura discusses Lean's journey, from its strict "cathedral model" of core development to its current extensibility. He reveals insights from the Collatz exploit, showcasing AI's role in uncovering kernel vulnerabilities and the critical need for robust formal verification. The conversation highlights AI's transformative impact, from generating complex, optimized code (like the zlib proof) to its limitations in true creativity, emphasizing the enduring human responsibility in defining specifications, curating knowledge, and maintaining trust in an AI-assisted future for software and mathematics.
Leonardo de Moura, creator of Lean, discusses its evolution, the challenges of formal verification, and the profound impact of AI on the field. Initially, Lean adopted a “cathedral model” for its core development, emphasizing stability and coherence, which Leo maintains is crucial for complex, interconnected systems. While he once personally oversaw much of the core, the Lean Functional Research Organization (FRO) now distributes ownership. Despite this tight control over the core, Lean 4’s extensibility allows extensive user-driven innovation, enabling the creation of domain-specific languages and extensions without altering the core, sometimes to Leo’s own surprise.
Leo highlights the difficulties of maintaining a core system, from preventing bugs and half-baked features to managing community input, famously citing Brandolini’s law regarding the disproportionate effort needed to debunk bad ideas. A recent incident involving a purported disproof of the Collatz conjecture, accepted by both Lean’s official kernel and an external checker (nanoda) due to different bugs, underscores these challenges. Leo suspects AI involvement in crafting the exploit, noting its “patience” for low-level implementation details like hash collisions. To bolster kernel security, he advocates for multiple independent kernels, “bulletproof” bounties, kernel simplification, and formal verification of kernels (e.g., Mario Carneiro’s Lean4Lean project), along with automated proof comparators and a reduction of the trusted computing base.
The conversation shifts to AI’s transformative role. A Claude agent successfully translated zlib from C to Lean, debugged it, and formally proved its compression-decompression property. Surprisingly, the AI-optimized Lean code even outperformed a Rust implementation, indicating AI’s potential for complex code generation and optimization, even for low-level tasks. Leo suggests that while specifications are often fluid, AI can make the process of updating proofs due to specification changes significantly cheaper, potentially integrating formal verification into every developer’s pipeline.
Regarding AI’s capabilities and limitations, Leo observes that AIs excel at “nut-sniping” tasks—filling proof holes or micro-optimizations—but struggle with genuine creativity, failing to invent new theories. He posits they demonstrate “competence without comprehension,” lacking the experience-driven understanding of humans. He distinguishes between using AI to develop software without embedded AI (safer) versus applications with embedded AI, where verified guardrails are essential.
Looking to the future, Leo anticipates humans will remain crucial for defining specifications, curating mathematical libraries like Mathlib, and identifying “interesting problems.” AI, he believes, will enable humans to explore more ideas by automating tedious implementation. Machine-checkable certificates for proofs will remain vital for trust, especially as proofs grow to millions of lines. Lean’s future involves significant investment in its performance (e.g., array manipulation), scalability for a potentially 100-million-line Mathlib, a formally verified compiler, and continuous reduction of its trusted code base. Leo reflects on Lean’s unexpected journey, from a tool for verified safety-critical systems to a global phenomenon embraced by top mathematicians like Terence Tao, attributing much of its success to an interactive design and a supportive community.
For new users, Leo advises starting with Lean as a programming language to build comfort before tackling proofs. He emphasizes leveraging AI agents, which he says “know Lean better than I do,” to explain concepts and offer customized guidance based on the user’s background.