AI Can Write the Proof. Leonardo de Moura Explains Who Should Check It

1. Guest Background

Leonardo de Moura is not speaking in this episode as an outside observer of formal methods. He is identified as the creator of Lean, chief architect and co-founder of Lean FRO, and a senior principal scientist at AWS. The evidence describes Lean FRO as the non-profit behind Lean, while the relevant work includes the Lean theorem prover, its core system, its extension ecosystem, Mathlib community development, and formal proof verification.

That background matters because the episode is not merely a discussion of whether AI can solve mathematical problems. The title asks, “AI Can Write the Proof. Who Checks It?” The interview examines what happens when AI systems can generate Lean proofs, assist with software verification, maintain proof artifacts, and perhaps also search patiently for soundness bugs in proof checkers. The subject being analyzed is therefore the trust chain around AI-written formal work: kernels, independent checkers, compiler trust, open-source governance, and the infrastructure needed to verify mathematics and software.

de Moura also clarifies his present role in Lean governance. He says he no longer personally controls the core system. Lean FRO has about 20 people, with developers owning different parts of the system and deciding whether to accept external requests. This point frames the whole episode: Lean’s reliability is not presented as the product of one founder’s personal control, but as a layered social and technical system built from ownership, transparency, a small trusted base, community extensions, and checks on checks.

2. What the Episode Covers

The first major thread is why de Moura defends a cathedral model for Lean’s core. He distinguishes core-system contributions from library contributions. A binary tree library can be incomplete and still useful; a tightly interconnected core system with missing pieces, crashes, or half-finished features undermines the entire tool. He says randomly merging core PRs can introduce bugs, leave features that appear to work but are incomplete, constrain future optimization, and scramble priorities. He also recounts removing Slack participants who only threw out ideas without writing useful code, leaving the core group focused on building a working system.

That protective stance does not mean Lean is closed. A central design choice is that Lean lets users build extensions and domain-specific languages without changing the core or coordinating with the core team. de Moura mentions extensions for distributed protocols and software verification, including a demonstration by Ilse Sergey and a student that initially did not even look like Lean to him. Lean 4 deepens this design: it is implemented in Lean, exposes internal representations to Lean code, and enables AI and autoformalization groups to extract training data from Mathlib proofs. Tools such as Velvet and Veo sit on top of that extensibility.

The episode’s sharpest security thread is the Collatz-related incident. A submitted proof or disproof was claimed to be accepted by both Lean’s official kernel and Nanoda, an external Rust checker. The team concluded that it exploited one bug in the official kernel and a completely different bug in Nanoda, and they strongly believed it was built by AI. de Moura’s concern is not merely that AI can produce false proofs. It is that AI has the patience to explore low-level implementation details that humans often do not want to grind through, making it especially good at finding soundness bugs.

That is why the answer to “who checks AI?” becomes an engineering architecture question. de Moura rejects a hidden private kernel as a security strategy. He says Lean’s community needs transparency, not safety by secrecy. His preferred route is multiple independent kernels, implemented by different people in different languages, with some of them eventually proved correct. Mario Carneiro’s Lean for Lean is important in this account because its goal is not just to be another checker, but a proved-correct kernel. The incident also produced concrete process lessons: Comparator can export proofs and recheck them in a sandbox, and one improvement is to always download the latest Nanoda so checker bug fixes are used immediately.

The episode also gives positive evidence for AI’s usefulness. Kim Morrison used a Claude agent on Zlib-related Lean work: translating C code to Lean, fixing the Lean implementation until it passed the C version’s test suite, and proving that compressing and then decompressing any data at any compression level returns the original data. de Moura says this had seemed almost out of reach at the beginning of the year. The example pushes AI’s role beyond high-level code generation. In his view, AI can keep optimizing low-level implementations while proofs ensure that required properties are preserved; he even imagines future AI writing and proving assembly that exploits processor instructions.

A final major thread is Mathlib as large-scale infrastructure. de Moura says Mathlib 3 stopped at about 1.1 million lines, while Mathlib 4 is around 2.4 million lines. The episode also cites community estimates that supporting mainstream mathematics and arbitrary research-level formalization could require a 100-million-line mathematical library. At that point Mathlib becomes comparable not to a small proof collection but to a large software project with build systems, version control, multiple teams, and governance problems. de Moura compares it to a crate ecosystem: when background components exist, researchers can focus on their contribution; when they are missing, a task that should take a month can become years of infrastructure work.

3. Core Views: Reasoning, Examples, and Limits

The episode’s central view is that Lean’s trust should not rest on the absence of bugs in a large system. It should rest on making the trusted base small and then checking that base more aggressively. The Collatz incident changes the risk model. A bad AI proof is not the only concern; an AI-generated artifact may be able to exploit implementation bugs and still receive the appearance of approval from checkers. If one sample can target different bugs in the official kernel and Nanoda, then a green check cannot be treated as the end of the verification story.

de Moura’s reasoning has a clear boundary. More checking does not mean hiding an undisclosed checker as a secret final test. He rejects safety by secrecy because it moves trust from public mechanisms to an unaudited claim. His alternative is transparent diversity: independent kernels built by different people, in different languages, with formal correctness proofs where possible. But even that has limits. Once a kernel is proved correct, trust questions can move to the compiler, then to hardware and runtime assumptions. de Moura’s stated direction is therefore reducing what must be trusted, not pretending that trust disappears.

A second core view is that an open-source ecosystem should not use the same governance model everywhere. The Lean core needs cathedral-style control because the pieces are interconnected and because design mistakes can create long-term constraints. The extension layer, by contrast, should be permissive enough for community creativity. The distributed-protocol and software-verification DSL examples show why this matters: domain experts can build tools for their own users without forcing those designs into the core. The limitation is that this model depends on a durable boundary. If extensions require core changes too often, the cost returns to the central system.

A third view is that current AI is best understood as a powerful proof and implementation searcher, not a settled replacement for human abstraction. de Moura says models are extremely strong at filling proof holes, combining existing components, and micro-optimizing code. But he says they fail badly when asked to invent new implementation techniques. His conjecture is that they have absorbed a great deal of literature during training, so they are biased toward existing solutions; if a problem can be solved by combining known tricks, they can perform extraordinarily well. The host’s flashlight metaphor adds a complementary point: expert prompting gives perspective, seeded solutions, tricks, and objectives that make the model’s search effective.

This capability boundary is exactly why Lean is such a powerful setting for AI. Lean gives a strong signal: the theorem still has to be proved, and the property must not be broken. The Zlib case shows how AI patience can become engineering value under that signal. The Collatz case shows the same patience becoming a security threat when the target is the checker itself. The limitation is that proof signals only enforce the formal target supplied to the system. If the specification is incomplete, the objective is wrong, or the checker is unsound, AI can still move efficiently in the wrong direction.

A fourth view is that machine-checkable certificates remain necessary even if models become highly accurate. de Moura does not reduce the AlphaProof, pure LLM, Monte Carlo tree search, and neural-symbolic discussion to a single winner. He separates how proof moves are generated from whether we still need verification. His answer is yes: even if a model produced correct answers at very high rates, large formal arguments still need certificates. Boris Alexeev’s 1.2-million-line Lean formal proof after OpenAI disproved the unit distance conjecture is the concrete example. No one wants to inspect that line by line; the value lies in a machine-checkable certificate.

A fifth view is that humans are likely to move rather than vanish. de Moura says humans will still state what they want and benefit from AI outputs. In Mathlib, AI may maintain boring proofs and construct many new proofs, while humans keep responsibility for key proofs that need beauty, structure, teaching value, or communicative clarity. Humans also remain important in roadmap decisions: what belongs in Mathlib, how rings should be defined, and how a library should be organized. This is not a confident prediction of a stable five-year future. de Moura explicitly says prediction is difficult, which makes the claim more modest: given current AI limits and formal ecosystem needs, human specification, taste, and structure still matter.

4. Learning and Application

For teams building trusted software, proof tools, or AI-agent infrastructure, the practical lesson is to redraw the trust boundary. Do not stop at “AI produced something that passed a check.” Separate the kernel, libraries, tactics, code generator, external checkers, sandbox, compiler, and runtime environment. Lean’s model suggests that the smaller the trusted base, the easier it is to audit, independently recheck, and eventually prove. But the boundary changes with the product: once proofs are used to generate executables, the compiler becomes part of what must be trusted.

For open-source maintainers, Lean offers a governance pattern: treat the core and the extension layer differently. A highly interconnected core needs ownership, priority management, and long-term design discipline. A surrounding extension ecosystem can be much more experimental. The tradeoff is real. Too much openness in the core risks bugs, half-finished features, and locked-in design choices; too much control over extensions prevents the community from discovering domain-specific tools that the core team would never design itself.

For software teams using AI, de Moura’s view of specifications is especially actionable. A specification does not always begin as a perfect logical contract. A simple, clear, inefficient reference implementation can function as a specification because it states what should be computed. AI can then optimize the implementation while proofs or property checks preserve behavior. This pattern fits compression code, compiler transformations, data-structure replacement, micro-optimization, and migration work. The boundary is that the reference implementation must actually encode the intended semantics; otherwise, AI only optimizes the wrong target.

For AI-assisted engineering, the Zlib example and the Collatz incident should be read together. AI is valuable when strong feedback constrains it: passing tests, preserving properties, repairing proof artifacts, and maintaining equivalence. The same persistence can also search for vulnerabilities. The practical response is not to ban AI, but to add independent checking, automatic checker updates, sandboxed rechecking, auditable process, and a minimized trusted base. For applications that embed AI at runtime, de Moura’s distinction is important: guardrails matter, and verified guardrails or verified sandboxes would be better still. Using AI to build software that does not itself contain AI is a safer scenario because the main adversary is ordinary application bugs, not live AI behavior.

For mathematical formalization projects, the Mathlib lesson is to think beyond individual theorems. The bottleneck is often background infrastructure: available components, abstraction maturity, dependency structure, build scale, and governance. If the required library material is missing, formalizing a paper can turn into years of infrastructure work. If the components exist, researchers can focus on their actual contribution. Projects such as Formal Frontiers matter because filling library gaps changes the economics of future formalization, not merely the count of proved statements.

For learners, de Moura’s advice is deliberately practical. Software developers can begin by treating Lean as a programming language and ignoring proofs at first. Once the syntax is familiar, they can try proving simple properties about their own code. AI agents can help because they have read documentation, know many extensions, and can tailor explanations to a learner’s background, whether that background is Haskell, Lisp, C#, or Java. The boundary is that AI is a tutor and translator, not a substitute for building judgment about proof moves, specifications, and where a formal result can still fail.

Source

• Original episode: AI Can Write the Proof. Who Checks It? — Leonardo de Moura