AI Can Write the Proof. Who Checks It? — Leonardo de Moura
Summary
Lean’s strategic advantage is a tightly governed core surrounded by a permissionless extension layer. Leonardo de Moura rejects random pull-request accumulation because bugs, incomplete features, and premature design commitments can constrain the whole system. Lean FRO’s 20-person ownership model now distributes that stewardship, while extensibility lets outsiders build surprising domain-specific tools without touching the trusted core.
An apparent Collatz refutation exposed how AI changes the economics of attacking proof checkers. The submission reportedly exploited one bug in Lean’s official kernel and an unrelated bug in the Rust-based Nanoda checker; de Moura says they are convinced AI created it. Joachim’s investigation raised the possibility that an LLM had seen a pull request in another repository and assembled the exploits. His conclusion is operationally urgent: “AI is very good at finding errors in logic and vulnerabilities in kernels.”
Kim Morrison’s AI-assisted zlib project moved formally verified, low-level software from implausible to newly plausible. A Claude Code agent translated C into Lean, reached compatibility with the C test suite, proved round-trip correctness for every compression level and input, and then optimized the array-heavy implementation into something resembling Rust’s approach. “We don’t have the patience for such low-level implementation, but AI does,” Scarfe says.
AI could make specification-driven development routine, but it cannot eliminate the hard work of deciding what software should do. Specifications emerge through user feedback, change after deployment, and can invalidate generated code and its proofs; AI’s value is in updating those artifacts so verification survives iteration. A simple, unoptimized Lean implementation can itself serve as the specification from which AI derives an optimized equivalent.
Mathlib is approaching an AI-amplified scaling problem rather than a shortage of theorem production. Lean 4’s library has reached 2.4 million lines versus Lean 3’s 1.1 million, and de Moura cites estimates of 100 million lines to support arbitrary scientific papers. Although Mathlib grew 44% from 2025 to today while compilation time fell 10%, AI could make library growth outrun human performance work and governance.
Today’s models excel at bounded “sniper proving” but remain unreliable at abstraction, experimentation, and selecting the right direction. They can fill proof gaps, explain obscure internals, and micro-optimize code better than most humans, yet still make “idiotic mistakes” and often reproduce established tricks rather than invent new ones. The durable human role is taste: specifying the vector, structuring libraries, choosing worthwhile problems, and preserving explanatory proofs.
Machine-verifiable certificates remain essential even if raw model accuracy approaches 99.99999%. Boris Alekseev’s 1.2-million-line Lean proof around the unit-distance conjecture illustrates why “nobody wants to check such a proof line by line.” Whether proofs come from GPT-5.6, Claude Fable, Monte Carlo tree search, or future systems, Lean’s opportunity lies in checking the moves while progressively verifying the kernel, compiler, and surrounding trust chain.
Deep dive
1. Lean’s core behaves like a cathedral so its ecosystem can behave like a bazaar
Tim Scarfe frames the tension through Quake 3 speedrunning: communities often turn unintended behavior into creative culture. De Moura’s answer is that he no longer personally controls Lean’s core; Lean FRO has roughly 20 people, with individual developers owning components and deciding whether to accept outside pull requests.
De Moura nevertheless remains “a strong believer in the cathedral model” for core development. Libraries can remain useful while incomplete, but a tightly interconnected core “full of holes” cannot; random contributions introduce bugs, half-built features, and design commitments that later prevent more important optimizations.
His counterbalance is extensibility. Community members can create specialized languages for areas such as distributed protocols or imperative-software verification without changing Lean’s core; one demonstration surprised him so thoroughly that he initially insisted, “This is not Lean,” only to learn it was entirely a Lean extension.
2. Cheap idea generation creates an expensive governance problem
De Moura recalls ejecting people from a Zulip channel because they continually proposed ideas without developing them. Each superficial revision made the next defect harder to expose: “Finding holes in an unfinished idea takes more and more time in exponential progression.”
Scarfe connects that experience to Brandolini’s law and generative AI: producing plausible suggestions is cheap, while refuting them consumes expert attention. De Moura’s complaint is not about creativity itself but asymmetric responsibility—one side brainstorms for fun while the core team must make a working system.
Lean FRO has materially changed that burden. When a serious kernel issue appeared, Joachim Breitner handled the technical investigation, community explanation, and coordination; de Moura says that previously this combination of engineering and public communication “would have been a nightmare for me.”
3. The Collatz exploit made proof checking an AI-security problem
Roughly a week or 10 days before the incident, a bug was found and fixed in Nanoda, a main external Lean kernel implemented in Rust. A purported Collatz refutation then appeared that allegedly passed both the official Lean kernel and the formerly vulnerable Nanoda implementation.
Investigation showed two distinct exploits: one targeted Lean’s official kernel, which de Moura fixed, while seemingly irrelevant hash-collision machinery targeted Nanoda’s different flaw. The explanation that this overlap was a coincidence did not rule out an LLM seeing a pull request in another repository and constructing the combined attack.
The immediate defense is mundane but consequential: Lean’s comparator, which exports proofs and tests them in a sandbox, should always fetch the latest Nanoda rather than awaiting a manual update. Longer term, de Moura wants more independently implemented kernels and support for Mario Carneiro’s Lean4Lean work, which has proved many parts but is not yet fully proven; its eventual value would be a kernel proved correct.
Scarfe proposes a private, hidden kernel analogous to a private benchmark test set. De Moura rejects the premise: “I don’t like security through obfuscation or hiding.” Trust should come from transparent implementations, diversity, and correctness proofs—not a secret checker presented as an unverifiable trump card.
4. AI has made verified low-level optimization newly plausible
De Moura initially considered Kim Morrison’s zlib project “hopeless.” The Claude Code agent nevertheless translated the C implementation into Lean, repaired it until it passed the C test suite, and proved that compressing and then decompressing any input, at any compression level, returns the original data.
The larger surprise came after correctness. Lean is optimized around syntax and expression trees, not arrays, yet continued AI-directed optimization produced an implementation somewhat like Rust’s while preserving the proof. De Moura’s updated view is blunt: “Last year I thought it was impossible, but now it’s quite possible.”
His extrapolation is verified assembly: give an AI formal x86 semantics and an assembler and ask it to exploit complex instructions while proving required properties. Scarfe says humans lack the patience for such low-level work; de Moura notes that each proof obligation supplies a clear signal about whether the optimization remains valid.
5. Specifications become more valuable precisely because they are incomplete
Scarfe’s pushback is that real software rarely begins with a stable specification; Agile exists because teams discover requirements through iteration. De Moura agrees: users continually ask for more control, less behavior, another checkbox, or a different proof location, so specification is “a constant dialogue.”
His practical bridge is to treat an unoptimized, high-level Lean program as an executable specification: implement “the simplest right idea” without sophisticated algorithms, then ask AI to produce a faster implementation and prove equivalence. This captures known behavior without pretending every requirement is settled.
Changing a specification invalidates code and its conformance proof, historically making formal verification painfully expensive. De Moura expects AI to update both, though he anticipates a transitional complaint: every specification change might require “billions of tokens to update everything.”
The implied endpoint is verification embedded in ordinary development. Engineers may merely write properties and submit pull requests; behind the interface, the system checks whether changes preserve those properties, even when users do not recognize the workflow as formal verification.
6. Lean 4’s extensibility prepared it for AI, while Mathlib now faces industrial scale
Lean 0.1 was de Moura’s compact but nearly unusable dependent-type-theory training tool; Lean 2 reached perhaps 50–100 users. Adam Chlipala’s demand for user-extensible tactics shaped Lean 3, after which Mathlib grew quickly and exposed the limits of extending tactics without extending the whole system.
Lean 4 was rebuilt in Lean itself, taking from early 2018 until late 2020 to compile itself. Its internal representations are accessible from ordinary Lean files, letting researchers extract proof data and letting developers build sophisticated verification languages without modifying the platform.
Dependent types provide the unifying mechanism: a structure containing integers X and Y can require a third field proving X is greater than Y, while a function can require evidence that a value Y is nonzero. Preconditions, postconditions, and invariants can be modeled as types.
Mathlib 4 has 2.4 million lines against Mathlib 3’s 1.1 million, and some community estimates put comprehensive scientific coverage near 100 million. Its unified abstractions—“there is only one ring”—are valuable, but that scale may require a coordinated collection of libraries with separate maintainers rather than one monolith.
7. AI can generate proofs, but humans still choose the mathematics worth keeping
De Moura sees models doing two apparently incompatible things: explaining obscure internals perfectly, then making simple top-level errors. They excel at “sniper proving”—closing a defined gap, combining known lemmas, or micro-optimizing code—but “if you ask them to come up with a new way of doing something, they fail miserably.”
Scarfe describes expert prompting as a flashlight aimed through embedding space: the human supplies a promising direction, initial constructions, useful tricks, and a precise objective. Models follow the beam brilliantly, yet their memory remains “crumbs for the next one” rather than a durable reorganization of understanding.
De Moura agrees that an LLM asked to implement SMT tends to repeat textbooks rather than conduct experiments. Learning by doing and updating weights from experience might supply the missing perspective, but continually adapting agent societies would also complicate safety and accountability.
Whatever generator wins, verification remains. A 1.2-million-line formal proof cannot be audited manually, and even 99.99999% model accuracy leaves a need for certificates; the unresolved competition is economic, with hybrid search taking many cheap steps while GPT-5.6 or Claude Fable takes fewer, costlier ones.
Lean’s roadmap therefore moves trust downward: Rust-competitive array performance, whole-system verification, handling libraries that could reach 100 million lines, and a verified compiler so executable software does not rely on implementation faith. Humans retain the roadmap—specifications, abstractions, library admission, and key proofs written beautifully enough to teach.