Lean Creator Leo de Moura Says AI Makes Proofs Cheap. Here Is What the Checkers Show

Leo de Moura, creator of the Lean proof assistant, said on an episode released October 29 that AI has made formal verification cheap enough to change how code is checked. He also said the remaining risk is that people verify the wrong thing.

De Moura is Vice President and Distinguished Scientist at AWS and Chief Architect of the Lean Focused Research Organization. He spoke to Ben Lorica on The Data Exchange, in an episode titled "When AI Writes the Code, Who Proves It Works?" The page was updated on November 1.

The claims in the episode

De Moura said Mathlib, Lean's community maths library, "took 10 years, written by humans, to go from zero to 2.5 million" lines. He said proofs of up to 50 million lines have since been published, and that a proof of Fermat's Last Theorem written by Anthropic's AI runs to 13 million lines. Those figures are his statements on the podcast. The episode page cites no document for either,, and no such document turned up among the pages read here.

Mathlib's own statistics page lists about 140,094 definitions, 292,237 theorems and 772 contributors. It shows no line count and no date, so it neither confirms nor contradicts the 2.5 million figure.

He described two uses already in production. The SymCrypt team at Microsoft uses Aeneas, which verifies Rust code through Lean, for its cryptographic library. Kim Morrison ported the zlib compression library to Lean and proved that compressing then decompressing returns the original data.

He also said a developer he identified as Boris, Claude Code's lead developer, had Claude build Lean models that found real bugs, and merged the resulting pull requests. No repository or pull request was named on the page.

Why the trusted base is small

The argument for verification at this scale is that a reader trusts only the proof kernel, the small program that checks every step. De Moura said Lean has two verified checkers, with a third on the way, and that independent kernels exist in Rust, C#, Haskell, TeX, COBOL and Fortran.

The Lean Kernel Arena tracks those checkers. Its results page, marked "Round in progress", lists 33 entries, including the official checker and a parse-only baseline that only reads input. The test download holds 127 good tests, 80 bad tests and 3.5 MB of data, with groups named cedar, mathlib, std and reachability, plus 26 bugs/ tests and 31 corner-cases/ tests.

The table ranks entries by how many invalid proofs they wrongly accept, then by how many valid proofs they wrongly reject. The page gives no implementation languages, so the six-language list is the guest's claim, not something the arena confirms.

Item	Figure	Where it comes from
Kernel Arena entries	33	Lean Kernel Arena results page
Good tests / bad tests	127 / 80	Lean Kernel Arena download
Mathlib theorems	292,237	Mathlib statistics page
Mathlib definitions	140,094	Mathlib statistics page
Longest published AI proof	50 million lines	de Moura, on the podcast

The site has covered what happens when a kernel is the weak point. Lean 4.35 added cross-checking with five proof-checking kernels, including one written in Lean by Claude, after an OpenAI model exploited kernel bugs to get a proof of False accepted.

The two gaps he names

De Moura did not claim verification removes risk. The episode summary lists two. The requirements gap is the distance between what you wrote down and what you want. The model gap is whether the Lean model matches the real code.

He said "testing is great for showing the presence of bugs, but not their absence." He also said "AI dramatically reduces the cost of verifying code" and that the question to ask a team is "show me your specifications, the properties, what you have verified, right?"

His view is that specifications and properties may become the artifacts engineers maintain, with code regenerated. That is a prediction about practice. Nothing on the page measures it.

The Navier-Stokes example

De Moura cited one case where the gap showed up. A human-curated problem statement was used for the Navier-Stokes problem, and OpenAI's informal and formal proofs had mismatches, reportedly over whether a fourth or fifth derivative was assumed. The site covered the dispute over OpenAI's Navier-Stokes data separately.

The example fits the requirements gap. A proof can be correct for a statement that is not the statement anyone meant, and the kernel will accept it.

What is unverified

The 13 million line and 50 million line figures rest on de Moura's word. The Boris anecdote has no linked pull request. The six-kernel language list is not on the arena page.

De Moura also said AWS's AgentCore and a project called Dogwood use Lean, and that Physlib, finance, chemistry and law have early autoformalization efforts. The episode page does not describe any of those in detail.

The arena also shows why a count of kernels is not a count of independent checks. Its ranking counts wrongly accepted invalid proofs first, so an entry that parses input and checks nothing sits in the table beside real checkers. A reader comparing 33 entries has to read the columns, not the row count.

The Data Exchange episode is a conversation, and Lorica's questions are not a test of the answers. The page summary records no one disputing de Moura's numbers and no outside voice who builds or audits proofs at that scale.

The Lean Kernel Arena round was still in progress on November 1, so its pass counts can change before any ranking is final.