Machine Learning Street Talk · Published 2026-09-29

AI Can Write the Proof. Who Checks It? — Leonardo de Moura

privateReview: unreviewedConfidence: high
leanmathlibformal verificationtheorem proverai proofsformal-verificationkernel-bugstheorem-proverspecification-drivenverification-pipelineai-code-generation
Open on YouTube ↗

Summary

Overview

  • Speaker: Leonardo de Moura
  • Channel: Machine Learning Street Talk
  • Main topic: Formal Verification, Lean Theorem Prover, AI-driven Mathematics and Software Verification
  • Purpose: To explore the implications of AI writing formal proofs, the necessity of trusted verification kernels, and how formal methods scale alongside AI code generation. Leonardo de Moura, creator of the Lean theorem prover and Senior Principal Scientist at AWS, discusses the intersection of artificial intelligence and formal verification. He examines how AI-generated proofs and code can exploit bugs in official and community checkers, the shift in software engineering towards specification-driven development, and the future of mathematical libraries like Mathlib in the era of large language models.

Topic Map

The Collatz Conjecture AI Proof Incident

  • Explanation: An AI-generated disproof of the Collatz conjecture was submitted using Lean, exploiting bugs in both the official Lean kernel and a community kernel called nanoda.
  • Key claims:
    • A disproof of the Collatz conjecture was submitted with an AI-built Lean proof.
    • The proof exploited one bug in the official Lean kernel and a completely different bug in nanoda.
    • AI has the patience for low-level implementation details that humans lack.
  • Examples:
    • Submitting 1.2 million lines of AI-generated Lean code to disprove the Collatz conjecture.
  • Terminology:
    • Lean
    • Collatz conjecture
    • kernel
    • nanoda
    • axiom-free proof of False
  • Why it matters: Highlights the danger of trusting AI-generated proofs when the underlying formal verification checkers contain undiscovered bugs.

Who Checks the Checker?

  • Explanation: The necessity of having trustworthy checkers and the architecture of Lean, including the core kernel versus mathlib.
  • Key claims:
    • Nobody wants to check 1,200,000 lines of Lean proof line by line.
    • Lean relies on a small trusted kernel surrounded by a vast ecosystem of libraries and community extensions.
    • The cathedral model of open source (central control over core) versus the bazaar model (open contribution).
  • Examples:
    • Comparing Lean's core architecture to Quake 3 shooter bounce bugs and community evolution.
  • Terminology:
    • Lean kernel
    • mathlib
    • cathedral and bazaar
    • comparator
    • landrun
  • Why it matters: Understanding how trust is distributed across a large software verification system.

Velvet and Real-World Software Verification

  • Explanation: Academic and applied work like Velvet and Veil demonstrating multi-modal verifiers for imperative programs built on top of Lean.
  • Key claims:
    • Velvet is a foundational multi-modal verifier for imperative programs in Lean created by Ilya Sergey and students.
    • Such tools make it significantly easier for people to verify imperative software using Lean.
    • Proving software correctness is moving into practical software engineering workflows.
  • Examples:
    • Velvet: A Foundational Multi-modal Verifier for Imperative Programs in Lean.
  • Terminology:
    • Velvet
    • Veil
    • imperative programs
    • software verification
  • Why it matters: Shows that formal verification is expanding beyond pure mathematics into imperative software engineering.

Specification-Driven Software Engineering

  • Explanation: How AI changes specification acquisition, moving from implementation details to formal specifications and automated verification.
  • Key claims:
    • High-level programming languages without optimization can be viewed as specifications.
    • AI can optimize code from high-level specifications without breaking semantic properties.
    • Specification acquisition engineering will replace manual low-level implementation.
  • Examples:
    • Using Lean to specify sumSquares and having AI optimize it into sumSquaresFast using mutable arrays.
  • Terminology:
    • specification acquisition
    • dependent types
    • optimisation
    • invariants
  • Why it matters: Redefines the role of human developers towards defining correct specifications while AI handles implementation.

The Evolution of Mathlib and Formal Mathematics

  • Explanation: The growth of Mathlib from Lean 3 to Lean 4, scaling from 1.1 million lines to 2.4 million lines, and the vision of reaching 100 million lines.
  • Key claims:
    • Mathlib grew from 1.1M lines in Lean 3 to 2.4M lines in Lean 4.
    • Some estimate that capturing all mainstream mathematics will require 100 million lines of Lean.
    • Human-AI collaboration is essential to scale formal mathematics to the research frontier.
  • Examples:
    • Formal Frontier initiative funded by Renaissance Philanthropy and XTX Markets.
  • Terminology:
    • Mathlib
    • Formal Frontier
    • dependent type theory
    • Fermat's Last Theorem
  • Why it matters: Demonstrates the roadmap for formalizing all of human mathematics with AI assistance.

Key Points

AI exploits kernel bugs

  • Explanation: Large language models can generate massive codebases that inadvertently or maliciously trigger edge cases and bugs in theorem provers.
  • Evidence: Collatz conjecture disproof PR exploiting bugs in Lean kernel and nanoda.
  • Practical implication: Kernel implementations must be rigorously verified to prevent accepting false proofs.

Specification over implementation

  • Explanation: In dependent type systems, precise types act as specifications, allowing humans to define what to compute while AI handles how to compute it efficiently.
  • Evidence: Lean function types capturing preconditions like y != 0.
  • Practical implication: Developers will spend more time writing precise specifications and less time debugging low-level code.

The scaling challenge of Mathlib

  • Explanation: Formalizing mathematics requires millions of lines of verified code, which is impossible without automated assistance.
  • Evidence: Mathlib growth from 1.1M to 2.4M lines.
  • Practical implication: AI agents must be integrated into mathematical library development to handle scaling.

Frameworks, Models & Processes

Lean Verification Pipeline

  • How it works: A multi-layered checking pipeline that validates proofs against trusted kernels and external checkers.
  • Components:
    • Lean kernel
    • Mathlib
    • nanoda
    • Comparator
  • When to use: When verifying complex mathematical theorems and software implementations.

Examples & Case Studies

An AI-generated proof attempting to disprove the Collatz conjecture was submitted to Lean.

  • Illustrates: AI capability to exploit bugs in theorem provers.
  • Lesson: Theorem provers must harden their kernels against sophisticated AI-generated edge cases.

Kim Morrison used Claude to implement a Lean version of the zlib compression format (lean-zip).

  • Illustrates: AI capability in complex systems programming and formal verification.
  • Lesson: AI can bridge low-level implementation with high-level formal verification.

Actionable Takeaways

  • Immediate:
    • Use Lean as a functional programming language before attempting proofs.
    • Understand the role of small trusted kernels in theorem provers.
  • Strategic:
    • Software engineering will shift from coding to specification writing.
    • AI will drive the scaling of formal mathematical libraries like Mathlib toward 100 million lines.
  • Questions to investigate:
    • How can we formally verify the compilers that compile our proof assistants?
    • What are the cost-to-performance trade-offs of hybrid tree-search LLM proof generation?

Claims Worth Verifying

  • A disproof of the Collatz conjecture was submitted with a 1.2M line Lean proof exploiting kernel bugs. (empirical)
  • Mathlib in Lean 4 contains 2.4 million lines of code. (empirical)

Notable Quotes

"A disproof of the Collatz conjecture was submitted with a Lean proof." (at 0:01) "We strongly believe it was built by AI, exploits one bug in the official kernel and this completely different bug in nanoda." (at 0:13) "Who checks the checker?" (at 0:59) "Software is only fun if the software doesn't have to work. If it has to work, the fun disappears very quickly." (at 10:47) "Comparator is a trustworthy judge for Lean proofs." (at 25:35) "It takes exponentially more work to debug bullshit than create it." (at 16:46)

Compressed Summary

  • AI-generated Collatz disproof exposed bugs in Lean and nanoda kernels.
  • Lean relies on a small trusted kernel to verify massive libraries like Mathlib.
  • Specification-driven development allows humans to specify what to compute while AI optimizes it.
  • Mathlib has scaled to 2.4 million lines with a path toward 100 million lines via human-AI collaboration.
  • Keywords: lean, mathlib, formal verification, theorem prover, ai proofs
  • Core insight: AI-generated formal proofs accelerate mathematical verification and software engineering, but require hardening trusted verification kernels against exploit-driven bugs.

Core insights

6
Failure Modehigh noveltystrong evidence

An AI-generated disproof of the Collatz conjecture defeated BOTH the official Lean kernel and the independent community kernel nanoda, but via two completely different bugs in each checker. Redundant cross-checking with independently-implemented verifiers therefore provides weaker assurance than assumed, because an AI searching a huge space can find distinct exploitable edge cases in each implementation independently.

Why it matters

Multi-checker / N-version redundancy is a common reliability pattern for agentic and verification systems; this shows that shared adversarial search pressure can defeat diversity-based defenses, so checker diversity alone is not a trust guarantee.

Generalization

Any system relying on independent implementations for cross-validation (multiple models, multiple runtimes, multiple validators) is vulnerable if a capable searcher probes each one separately rather than hitting a shared bug.

The proof exploited one bug in the official Lean kernel and a completely different bug in nanoda.
Open source video
A disproof of the Collatz conjecture was submitted with an AI-built Lean proof.
Open source video
Architecturehigh noveltymoderate evidence

In a dependent-type setting, a high-level program without optimization can itself serve as the specification, and AI can transform it into an optimized implementation while semantic properties are preserved and machine-checked. The human role shifts from writing low-level implementation to acquiring/authoring precise specifications.

Why it matters

This redefines where the human/agent boundary should sit in code-generation pipelines: humans own the spec, AI owns the implementation, and the verifier enforces equivalence. It makes correctness a specification problem rather than a code-review problem.

Generalization

Applied broadly, any AI code-generation workflow can be reframed as spec-authoring plus verified-synthesis, with verification replacing line-by-line human review.

High-level programming languages without optimization can be viewed as specifications.
Open source video
AI can optimize code from high-level specifications without breaking semantic properties.
Open source video
Specification acquisition engineering will replace manual low-level implementation.
Open source video
Empirical Resultmedium noveltystrong evidence

AI's distinguishing capability here is not insight but stamina for low-level implementation detail at scale: it produced ~1.2 million lines of Lean to attempt the Collatz disproof. This scale of generation is precisely what makes human line-by-line review impossible, so trust must be pushed into small, mechanized checkers rather than human inspection.

Why it matters

It quantifies the review-bandwidth asymmetry that forces architectures toward mechanical verification: if generated artifacts vastly exceed human review capacity, review-based assurance collapses.

Generalization

For any agentic system producing large artifacts (code, configs, proofs), assurance must be automated and tractable to check, because generation capacity outstrips human audit capacity.

AI has the patience for low-level implementation details that humans lack.
Open source video
Submitting 1.2 million lines of AI-generated Lean code to disprove the Collatz conjecture.
Open source video
Nobody wants to check 1,200,000 lines of Lean proof line by line.
Open source video
Architecturemedium noveltymoderate evidence

Trust in a large formal system is concentrated in a small kernel surrounded by a vast ecosystem of libraries and community extensions, with an explicit tension between a 'cathedral' centrally-controlled core and a 'bazaar' of open contributions. This is a trust-boundary design decision: minimize and harden the trusted core, allow open evolution around it.

Why it matters

Defines a reusable pattern for agent and ML systems: draw a tiny, heavily-verified trusted computing base and push everything else—extensions, tools, models—outside it, so the attack surface that must be correct is small.

Generalization

Applies to any platform where a trusted core enables an untrusted, fast-moving extension ecosystem (plugin systems, tool registries, model gateways).

Lean relies on a small trusted kernel surrounded by a vast ecosystem of libraries and community extensions.
Open source video
The cathedral model of open source (central control over core) versus the bazaar model (open contribution).
Open source video
Predictionmedium noveltymoderate evidence

Scaling formal mathematics is a volume problem that cannot be solved by humans alone: Mathlib grew from 1.1M lines (Lean 3) to 2.4M lines (Lean 4), while covering all mainstream mathematics is estimated to require 100M lines, making AI-agent participation in library development a structural necessity rather than an optimization.

Why it matters

It frames agent involvement in large knowledge/code repositories as mandatory at a specific scale threshold, and gives concrete order-of-magnitude targets for where automation must take over.

Generalization

Large structured knowledge bases beyond a certain size cannot be maintained by human contribution alone and require agent-integrated maintenance pipelines.

Mathlib grew from 1.1M lines in Lean 3 to 2.4M lines in Lean 4.
Open source video
Some estimate that capturing all mainstream mathematics will require 100 million lines of Lean.
Open source video
Human-AI collaboration is essential to scale formal mathematics to the research frontier.
Open source video
Practicemedium noveltymoderate evidence

Formal verification tooling is expanding from pure mathematics into imperative software engineering via layered verifiers (e.g., Velvet, a foundational multi-modal verifier for imperative programs in Lean), and AI itself has been used to implement verified low-level systems code (lean-zip). This moves verified-correctness into mainstream engineering workflows.

Why it matters

Signals that verification is becoming an engineering-layer capability over real imperative code, not only a mathematics tool, changing what developers can assume about correctness guarantees.

Generalization

Verification harnesses built on a trusted kernel can generalize from math theorems to production imperative code, suggesting a path toward machine-checked correctness in ordinary software pipelines.

Velvet is a foundational multi-modal verifier for imperative programs in Lean created by Ilya Sergey and students.
Open source video
Kim Morrison used Claude to implement a Lean version of the zlib compression format (lean-zip).
Open source video

Deep dives

5

Adversarial search against N-version verification checkers

Research question

Can a high-volume adversarial generator reliably find distinct accept-false bugs in each independently-implemented checker (Lean kernel, nanoda) such that N-version redundancy reduces to the union of exploits rather than the intersection?

Why

Multi-checker redundancy is treated as a core assurance pattern in agentic and verification pipelines; if a capable searcher defeats each implementation through different bugs, checker diversity provides far weaker assurance than assumed and trust must be re-anchored in a tiny audited core plus adversarial input detection.

A disproof of the Collatz conjecture was submitted with an AI-built Lean proof.
Open source video
The proof exploited one bug in the official Lean kernel and a completely different bug in nanoda.
Open source video
Submitting 1.2 million lines of AI-generated Lean code to disprove the Collatz conjecture.
Open source video
Source video

Review-bandwidth asymmetry and mechanized assurance thresholds

Research question

At what ratio of generated-artifact volume to feasible human review capacity does review-based assurance become strictly dominated by mechanized checking, and how should that threshold be measured?

Why

AI produced ~1.2M lines of Lean, which nobody will review line by line; quantifying the point where generation capacity outstrips audit capacity turns 'we should automate verification' from a preference into an engineering constraint with concrete triggers.

AI has the patience for low-level implementation details that humans lack.
Open source video
Nobody wants to check 1,200,000 lines of Lean proof line by line.
Open source video
Submitting 1.2 million lines of AI-generated Lean code to disprove the Collatz conjecture.
Open source video
Source video

Spec-as-source and machine-checked equivalence in AI code synthesis

Research question

When an unoptimized dependent-typed program is used directly as the specification, can AI-produced optimized implementations be proven semantically equivalent with high coverage, and where do those equivalence proofs fail?

Why

If human effort migrates from low-level implementation to specification acquisition, the trustworthiness of AI code generation depends entirely on how completely equivalence checking covers the real semantic properties of the specification, not on the example at hand.

High-level programming languages without optimization can be viewed as specifications.
Open source video
AI can optimize code from high-level specifications without breaking semantic properties.
Open source video
Specification acquisition engineering will replace manual low-level implementation.
Open source video
Source video

Trusted-core minimizing architecture under open contribution pressure

Research question

What is the measurable trust-assumption surface of a small trusted kernel once community extensions and tooling are included, and does kernel minimization actually reduce total exploitable surface under a cathedral/bazaar governance split?

Why

The pattern of a tiny hardened core with a fast-moving extension ecosystem recurs in plugin systems, tool registries and model gateways; knowing whether the minimized core or the surrounding bazaar dominates risk determines where verification budgets should be spent.

Lean relies on a small trusted kernel surrounded by a vast ecosystem of libraries and community extensions.
Open source video
The cathedral model of open source (central control over core) versus the bazaar model (open contribution).
Open source video
Source video

Agent-integrated maintenance pipelines at knowledge-base scale thresholds

Research question

What is the artifact-size threshold at which human-only contribution to a structured knowledge or code library becomes infeasible, and what provenance, attribution and spot-audit mechanisms keep agent-maintained libraries trustworthy?

Why

The 1.1M to 2.4M line Mathlib growth against a 100M line coverage estimate frames agent participation as structural necessity, but no governance or review model for agent-authored contributions is described, making provenance and audit design the binding constraint.

Mathlib grew from 1.1M lines in Lean 3 to 2.4M lines in Lean 4.
Open source video
Some estimate that capturing all mainstream mathematics will require 100 million lines of Lean.
Open source video
Human-AI collaboration is essential to scale formal mathematics to the research frontier.
Open source video
Source video

Article ideas

3

Redundant Checkers Are Not a Safety Net: How One AI Proof Broke Two Independent Kernels

Independent implementations are commonly treated as cross-validation, but an AI searching a large proof space found a different exploit in each checker, so diversity-based assurance must be replaced by adversarial-input detection around a minimized trusted core.

Angle

Use the Collatz disproof attempt as the concrete case study, then generalize the failure of N-version redundancy to multi-model and multi-validator agent pipelines.

Source video

A Million Lines and No Reviewer: Why Generation Volume Forced Verification To Become the Product

Once AI can emit artifacts on the order of 1.2 million lines, human line-by-line review stops being a viable assurance mechanism, so the engineering frontier moves to hardening the small checker that everything else trusts.

Angle

Quantify the review-bandwidth asymmetry, then argue that verification tooling quality is now the primary determinant of code-generation reliability.

Source video

From Code Review to Spec Review: The Coming Shift to Specification Acquisition Engineering

If unoptimized high-level programs can serve directly as specifications and AI produces the optimized implementations, then the human bottleneck and the human value both relocate to authoring precise, checkable specifications.

Angle

Contrast code review as an assurance practice with machine-checked equivalence against a specification, and detail what teams must build to make the shift real.

Source video

Project ideas

4

Dual-Checker Adversarial Prober

beyond-evals

Given two independently-implemented checkers of the same logic, an automated generator with bounded search budget can find at least one input accepted by both while being semantically false, at a materially higher rate than a single-checker prober finds on one implementation.

Proof of concept

Build a harness with two structurally distinct validators (e.g., a reference checker and an independent reimplementation) plus a generator that mutates candidate artifacts to maximize acceptance under each; log every case where both accept a known-false artifact.

Measurement

Rate of joint accept-false findings per 1,000 generated candidates versus single-checker findings, and overlap between the bug classes each checker is defeated by.

Source video

Spec-Equivalence Gate

gatehouse

For a benchmark suite of imperative routines, an AI optimizer that must produce machine-checked equivalence to an unoptimized reference implementation will maintain functional correctness at a fixed success rate while achieving measurable performance gains, and failures will cluster in specific semantic property classes.

Proof of concept

Take a set of small imperative programs, treat the unoptimized versions as specifications, have an agent generate optimized implementations, and gate each on a checker that proves equivalence (e.g., extensional equality on all inputs within a modeled domain).

Measurement

Fraction of optimizations that pass equivalence checking, average speedup, and a taxonomy of the semantic properties that failed first.

Source video

Trust-Surface Mapper

gatehouse

In a small-trusted-core platform with a large extension ecosystem, the majority of realistically exploitable trust assumptions live outside the core, so overall risk is dominated by extension volume rather than core size.

Proof of concept

Instrument a kernel-plus-extensions system, enumerate every component that can influence acceptance of an artifact, and classify each as core, library, or community extension; then run a targeted probe suite against each class.

Measurement

Count and severity of successful trust violations per component class, and the share attributable to non-core components.

Source video

Agent-Library Maintenance Threshold Study

movement-lab

There is a repository-size threshold beyond which human-only contribution throughput falls below the rate required to maintain the library, and agent-assisted contribution above that threshold requires provenance and spot-audit tooling to keep defect escape rates at human-only levels.

Proof of concept

Simulate a growing structured library with both human-only and human-plus-agent contribution modes across increasing sizes, tracking defect rate, review backlog, and provenance completeness.

Measurement

Contribution throughput and defect escape rate versus library size for each mode, and the size at which human-only throughput saturates.

Source video

Architectural implications

3

The Collatz incident shows a single independent kernel is not sufficient assurance against an adversarial or high-volume proof generator.

Before

Trust a single well-tested kernel, or assume redundant independent checkers provide strong cross-validation.

After

Treat every checker as a potential exploitable surface; expect an AI-generated search to find distinct bugs in each independently-implemented checker.

Consequence

Verification pipelines need a small, exhaustively-audited trusted core plus detection for adversarial edge-case inputs, and should not equate checker diversity with correctness.

Source video

Specification becomes the human-owned artifact while AI owns implementation, with the verifier enforcing equivalence.

Before

Human reviews and debugs AI-generated low-level implementation code.

After

Human authors precise specifications; AI produces optimized implementations; the checker proves semantic preservation.

Consequence

Tooling and workflows shift toward specification-acquisition engineering, spec-diffing, and invariant capture rather than code review.

Source video

Generated artifact volume (e.g., 1.2M lines) exceeds feasible human review, forcing mechanized trust.

Before

Human line-by-line review as the assurance mechanism for generated code or proofs.

After

Small trusted checkers as the only tractable assurance layer for large AI-generated artifacts.

Consequence

Investment moves to hardening and verifying the checker itself, since it becomes the single point of trust.

Source video

Tradeoffs and failure modes

4

Redundant independent checkers vs. adversarial bug discovery

Benefit

Independent implementations (Lean kernel and nanoda) should catch each other's mistakes through cross-validation.

Cost or risk

An AI-generated proof exploited one bug in the official kernel and a completely different bug in nanoda, so both accepted a false result.

The proof exploited one bug in the official Lean kernel and a completely different bug in nanoda.
Open source video
Source video

Open contribution ecosystem vs. trusted core integrity

Benefit

The bazaar model allows broad community contributions and rapid ecosystem growth.

Cost or risk

A large extension surface around a small trusted kernel creates many places where trust assumptions can break, complicating verification of the whole system.

Lean relies on a small trusted kernel surrounded by a vast ecosystem of libraries and community extensions.
Open source video
Source video

AI code optimization vs. semantic-preservation risk

Benefit

AI can transform high-level specifications into fast implementations (e.g., sumSquares into a mutable-array sumSquaresFast).

Cost or risk

Optimizations must not break semantic properties; without machine-checked equivalence, optimized implementations can silently violate the spec.

AI can optimize code from high-level specifications without breaking semantic properties.
Open source video
Source video

Generation scale vs. human review capacity

Benefit

AI can produce vast volumes of proofs/code cheaply.

Cost or risk

1.2M lines are effectively unreviewable by humans, so assurance cannot rely on human inspection.

Nobody wants to check 1,200,000 lines of Lean proof line by line.
Open source video
Source video

Open questions

3

How can the trusted core (kernel) itself be verified well enough to resist AI-generated adversarial edge cases?

Why unresolved

The summary shows bugs in both the official Lean kernel and nanoda but does not describe a method for exhaustively verifying kernels.

Research direction

Formally verify or differentially fuzz kernels against an adversarial generator that searches for accepting-but-false proofs.

Source video

What mechanisms reliably detect when an AI optimization breaks semantic properties rather than preserving them?

Why unresolved

The summary asserts AI can optimize without breaking semantics but gives no evidence of an enforcement mechanism or its coverage.

Research direction

Build and benchmark verified-optimization pipelines where equivalence between spec and optimized implementation is machine-checked, measuring where guarantees fail.

Source video

What is a tractable human-review and governance model for 100M-line verified libraries maintained with AI agents?

Why unresolved

The 100M-line target and Mathlib growth are stated, but no review, provenance, or ownership model is described.

Research direction

Study contributor-attribution, proof-provenance tracking, and spot-audit strategies for agent-augmented large libraries.

Source video

Key claims

7
factualVerification needed

An AI-built Lean proof attempting to disprove the Collatz conjecture exploited one bug in the official Lean kernel and a different bug in nanoda.

Evidence

The proof exploited one bug in the official Lean kernel and a completely different bug in nanoda.

Question

What were the specific kernel and nanoda bugs, and did the PR actually pass both checkers before being caught?

Source video
causalVerification needed

AI can optimize code from high-level specifications without breaking semantic properties.

Evidence

AI can optimize code from high-level specifications without breaking semantic properties.

Question

Is semantic preservation guaranteed by the proof checker, or merely asserted for the specific example?

Source video
predictionVerification needed

Specification acquisition engineering will replace manual low-level implementation.

Evidence

Specification acquisition engineering will replace manual low-level implementation.

Question

Is there empirical evidence of teams shifting effort from implementation to specification authoring?

Source video
comparativeVerification needed

Covering all mainstream mathematics is estimated to require about 100 million lines of Lean, versus Mathlib's growth from 1.1M to 2.4M lines.

Evidence

Mathlib grew from 1.1M lines in Lean 3 to 2.4M lines in Lean 4.

Question

How was the 100M-line estimate derived, and does line count meaningfully proxy for coverage?

Source video
factualVerification not requested

Lean's safety model concentrates trust in a small kernel surrounded by a large community ecosystem, reflecting a cathedral-vs-bazaar tension over the core.

Evidence

Lean relies on a small trusted kernel surrounded by a vast ecosystem of libraries and community extensions.

Source video
opinionVerification needed

AI possesses patience for low-level implementation details that humans lack, enabling generation at scales like 1.2 million lines.

Evidence

AI has the patience for low-level implementation details that humans lack.

Question

Does sustained long-horizon low-level generation actually improve end-to-end success rates, or mainly increase volume?

Source video
factualVerification needed

Velvet provides a foundational multi-modal verifier for imperative programs in Lean, enabling verification of ordinary software.

Evidence

Velvet is a foundational multi-modal verifier for imperative programs in Lean created by Ilya Sergey and students.

Question

What classes of imperative programs can Velvet verify, and with what soundness guarantees?

Source video

Connections

5

Lean kernelnanoda

Independent reimplementations used as redundant checkers, but exploited via different bugs, undermining diversity-based assurance

Source video