The Programming Language That Referees Mathematics — Leo de Moura

The Programming Language That Referees Mathematics — Leo de Moura

by Leo de Moura · View the channel on PSI

Formal & Physical Sciences Computing & Cybersecurity UMComputer programmingUMXProgramming and scripting languages: general
🎙 Leo de Moura 👥 220K 📅 September 29, 2026 ⏱ 74 min 👁 18K 📄 expert opinion 🧭 2026-10-06
Available in: English (current) Français

Keywords

Leanformal proofCollatz conjecturekernel exploitAI-generated proofsMathlibdependent typesformal verification

Summary

In this episode of Machine Learning Street Talk, Tim Scarfe interviews Leo de Moura, creator of the Lean proof assistant and co-founder of the Lean FRO. The conversation opens with de Moura clarifying that he no longer controls Lean’s core; instead, the Lean FRO and its developers guide evolution under a ‘cathedral’ model, contrasting with the community-driven ‘bazaar’ approach for libraries like Mathlib. De Moura explains why the core remains small and protected, citing risks of half-baked features and the difficulty of prioritization. A major topic is the recent Collatz conjecture exploit, where a purported proof was accepted by Lean’s official kernel and the independent checker nanoda, exploiting different bugs in each. De Moura details the investigation, the role of AI in crafting the exploit, and strategies to mitigate such attacks, including multiple independent kernels, kernel verification (Lean4Lean), and the comparator tool. The discussion then shifts to AI-generated proofs: Kim Morrison’s Claude agent successfully translated and verified the zlib compression library in Lean, and even optimized it to outperform Rust—a surprising feat. De Moura reflects on specification-driven software engineering, noting that AI can ease the cost of re-verification when specifications change, but emphasizes that formal verification only certifies the specification chosen by humans. The interview concludes with thoughts on proof search as a game, the distinction between formal competence and mathematical understanding, and the importance of human responsibility in defining problems, curating Mathlib, and deciding what to prove. De Moura also gives advice for newcomers to Lean and reflects on the project’s future beyond its founder.

256 words

Critical Evaluation

Value of the Information & Strength of the Argument

The video offers exceptional value by granting access to the creator’s perspective on current events and future directions in formal verification and AI. De Moura’s arguments are well-structured and supported by concrete examples, such as the Collatz exploit and the zlib proof, which illustrate both the power and the pitfalls of AI-assisted formalization. He defends the cathedral model with clear reasoning about software engineering and community dynamics, and his anti-obfuscation stance on kernel security is compelling. The dialogue with Scarfe adds depth, with questions that push for nuance and logical consistency. The argumentation is solid, though sometimes de Moura’s opinions (e.g., on transparency) are presented as principled stands rather than empirical conclusions, but they are coherent and well-articulated.

Scientific Rigor, Source Quality, Title Accuracy

The scientific rigor is high: de Moura references specific repositories, issues, PRs, and documented incidents. He distinguishes between verified and non-verified components, and discusses the limits of current verification approaches. The sources cited in the description are comprehensive and directly relevant, including Lean, Mathlib, nanoda, Lean4Lean, and related projects. The title ‘The Programming Language That Referees Mathematics’ is apt and not overstated; the episode indeed explores Lean’s role in mathematics and the challenges of certification. There are no comments provided, so no public sentiment analysis is possible. Overall, the episode is rigorous and trustworthy, coming from the primary authority on the subject.

235 words

Title / Content Match

The title accurately captures the central theme: Lean as a language that 'referees' mathematics, with a focus on its kernel, correctness, and role in formal verification.

Quality & Reliability

9/10

Interview with the creator of Lean, providing unique first-hand insights into the design, security, and governance of the proof assistant. The discussion is technically deep and grounded in specific incidents (e.g., Collatz exploit, zlib proof) and references to official repositories and publications.

Chapters

Cited Sources

  • Lean — Official Lean home page, referenced at 00:00:48 as the proof assistant developed by de Moura.
  • Mathlib — Community-maintained mathematical library for Lean, discussed at 00:01:24 as the main repository of formalized mathematics.
  • nanoda_lib — Independent kernel written in Rust, referenced at 00:12:09 in the context of the Collatz exploit.
  • CollatzLean — Repository containing the purported Collatz disproof, discussed at 00:12:19.
  • Lean issue 14576 — Issue reporting the bug in the official kernel exploited by the Collatz proof, referenced at 00:13:06.
  • Lean pull request 14577 — PR fixing the kernel bug, referenced at 00:13:21.
  • nanoda_lib pull request 22 — PR fixing a bug in nanoda, referenced at 00:13:45.
  • Lean comparator — Tool for cross-checking proofs with independent kernels, discussed at 00:15:33.
  • Lean4Lean — Kernel written in Lean, intended to be proven correct, referenced at 00:18:02.
  • lean-zip — Kim Morrison's Lean implementation of zlib, discussed at 00:21:59.
  • CompCert — Verified C compiler, mentioned as an example of formal verification in safety-critical systems at 00:29:45.
  • seL4 — Verified microkernel, mentioned as an example of formal verification at 00:29:45.
  • Z3 — SMT solver co-created by de Moura, referenced at 00:30:23.
  • Veil — Verification tool built on Lean, referenced at 00:38:10 as an example of Lean extensibility.
  • Velvet — Another verification tool, referenced at 00:38:10.
  • Brandolini's law — Referred to at 00:10:05 to explain the difficulty of debunking false claims.

Concurring Sources

External References

Contribution & Novelties

The video provides a rare insider perspective on Lean’s development, its security incidents, and the intersection of formal verification with AI. The novelty lies in the detailed account of the Collatz exploit, the challenges of kernel trust, and the demonstration of AI’s ability to generate verified code (e.g., zlib). It also clarifies philosophical positions on transparency and governance. These insights are valuable for researchers and practitioners.

Pour aller plus loin :

  • Formal verification — Overview of the field where Lean operates, providing context for the video’s claims.
  • Lean (proof assistant) — Detailed history and features of Lean, complementary to the conversation.
  • De Bruijn criterion — Concept related to the ‘small trusted kernel’ design discussed in the episode.
  • Collatz conjecture — The mathematical problem central to the exploit incident; essential background.
  • Proof assistant — General context for interactive theorem proving.

139 words

Radar Profile

The profile shows a high level of technical depth (9) and information quality (9), with a slightly lower but still strong quantity (8) and reliability (8). This reflects a dense, expert-level discussion that is trustworthy but assumes prior knowledge.

Reliability 8/10