Who Checks a Proof No Human Can Read? — Leo de Moura

Summary

Leo de Moura argues that Lean’s safety depends on a very small trusted kernel, while the broader system can remain extensible, transparent, and open to community-built tools and DSLs. He recounts the recent Collatz-related incident as an example of how different bugs in separate kernels can be combined, and says the response should be more independent kernels, better sandboxing, and eventually formally verified kernels, compilers, and hardware specs. The discussion then shifts to AI: de Moura says current models are excellent at proof maintenance, translation, and optimization, but still weak at inventing genuinely new techniques. He cites a Claude-assisted zlib formalization as a standout success, and expects similar workflows to expand into lower-level code and assembly proofs. The episode closes on mathlib scaling, the Formal Frontiers initiative, and a future where many developers use verification indirectly through AI-assisted pipelines.

Notes

• Lean relies on a small trusted kernel, while the rest of the system can contain many bugs and moving parts.
• The Collatz incident was framed as a proof accepted by both the official Lean kernel and an external checker, apparently by exploiting two different bugs.
• He says the exploit was likely AI-generated and stitched together from repository details and prior pull requests.
• The official lesson from the incident is that more than one independent checker is needed.
• He wants at least one kernel to be formally proved correct, not merely trusted by convention.
• The trust chain should keep shrinking upward from kernel, to compiler, to hardware specifications.
• He rejects security through secrecy for proof infrastructure.
• Lean’s cathedral model keeps core governance centralized rather than letting random pull requests reshape the core.
• He says the Lean foundation now absorbs community communication, bug triage, and roadmap coordination.
• Lean was intentionally made extensible so others can add DSLs and verification tools without changing core internals.
• That extensibility now supports domain-specific languages for areas like distributed protocols.
• He still thinks the core should stay tightly controlled because it is highly interconnected.
• He lists four core-maintenance hazards: bugs, half-baked features, design lock-in, and chaotic pull-request churn.
• He says popular features can constrain future optimization and become hard to remove.
• Randomly merging pull requests does not scale for a system like Lean.
• The Lean foundation reduces operational load by handling bugs and community coordination.
• Comparator is used to export proofs and verify them in a sandbox.
• Comparator should automatically fetch the latest Nanoda so stale vulnerable versions are not used.
• He views transparency plus stronger proofs as better than hiding the checker implementation.
• AI is already good at proof maintenance, optimization, and translation of known software into Lean.
• The zlib case was a standout: Claude translated C to Lean, preserved the C test suite, and proved round-trip correctness.
• He says the AI even optimized the Lean implementation enough to beat Rust on array-heavy code.
• He expects AI to eventually prove assembly-level properties once x86 semantics are formalized.
• Current models still struggle when they need a genuinely new technique rather than a known pattern.
• He characterizes today’s LLMs as breadcrumb followers rather than persistent learners.
• LLMs can recite SMT and Z3 theory, but they do not actually experiment the way humans do.
• He thinks learning by doing could give future models new perspectives.
• Tim Scarfe argues that strong AI still needs human direction, seeded examples, and a clear objective.
• Scarfe says the missing piece is abstraction, not raw capability.
• De Moura thinks verified guardrails are especially important when AI is embedded inside applications.
• He expects formal verification to become more invisible to end users as it moves into the pipeline.
• Human mathematicians will still write the important elegant proofs by hand.
• Formal certificates still matter even if models become extremely accurate.
• He says proofs are needed because humans will not line-by-line check massive formal artifacts.
• Lean should evolve into a programming language competitive with Rust for array-heavy and verification-heavy work.
• He wants Lean to verify full systems, not just individual libraries.
• He says a verified compiler would materially reduce the trusted code base.
• Lean 4’s extensibility exposes internal data structures and proof objects to user code.
• That openness helped AI labs extract training data and proof information from mathlib internals.
• mathlib grew from about 1.1 million lines in Lean 3 to 2.4 million lines in Lean 4.
• He believes mathlib will keep expanding indefinitely as mathematics itself keeps generating new objects and structures.
• At some scale, mathlib may need to split into several coherent libraries with different leadership.
• He compares future formalization needs to huge software stacks that require extensive infrastructure.
• Formal Frontiers is meant to use humans plus AI to fill gaps in mathlib.
• He frames missing library infrastructure as the main bottleneck to formalizing research papers.
• He says AI is already strong at filling routine proof gaps and maintaining boring proofs.
• Milestone theorems like Fermat’s Last Theorem can act as a benchmark for AI-assisted formal math.
• He thinks hybrid AlphaProof-style systems and pure LLM approaches are both still under evaluation.