AI FOR SCIENCE · INTERVIEWS
De Moura says a false proof claiming to settle the Collatz conjecture passed both Lean's official kernel and the external kernel nanoda, through a different bug in each, and his team believes an AI built it. His conclusion: checkers must be several, open and eventually proved correct, and a proof only certifies the statement people wrote.
Lean's lead gives his account of the exploit and the fix (the official kernel patched, the comparator now always pulling the latest nanoda), and numbers: Mathlib is at 2.4 million lines, up 44% since 2025 while compile time fell 10%, and the community estimates 100 million lines are needed to formalise any research paper.
The official kernel is not yet proved correct: Mario Carneiro's Lean4Lean proves parts of it, not the parts this exploit used; and when Lean produces an executable, the compiler is trusted too, and it is not verified.
In de Moura's telling, a bug was reported in nanoda and fixed at once; days later someone submitted a Lean 'disproof' of the Collatz conjecture that the official kernel accepted, and so did nanoda before the fix. The proof carried irrelevant terms built to force a hash collision, there only to pass nanoda. The submitter called it a coincidence; his team cannot rule out that a model read nanoda's fix by itself and crafted the exploit.
“We strongly believe it was built by AI.”Leonardo de MouraHe wants more independent kernels written by different people in different languages, and in the end one proved correct (Lean4Lean), then a verified compiler below it. When the host suggests a private kernel, like ARC-AGI's hidden test set, he refuses: trust has to come from transparency, not secrecy.
Kim Morrison used a Claude agent to translate zlib from C to Lean, pass the C version's test suite and prove that, at any compression level and for any data, decompressing what was compressed gives the original back. De Moura says he thought this out of reach at the start of the year; but what is proved is that property, and choosing the property stays a human job.
He says today's models beat people at 'nut-sniping': a fixed statement, no new theory needed, only existing pieces to combine; ask them for a new technique and they 'fail miserably'. Their memory is breadcrumbs left for the next instance to wake up to; their weights are not learning.
Whether a paper can be formalised depends on whether its background is in Mathlib. Mathlib is at 2.4 million lines; the community estimates 100 million are needed to formalise any research-level paper. The Mathlib Initiative's Formal Frontiers wants humans and AI to fill the gaps, with theorems easy to state and hard to prove, such as Fermat's Last Theorem, as milestones.
The record's Lean entries treat passing the check as the end point: Claude's formalisation of Fermat's Last Theorem (2026-09-04) is recorded as 'computer-checked'. Nothing on the record said the checker itself could fail.
Lean's lead says a false proof has just passed the official kernel and an external one, that his team believes an AI built it, and that this 'is going to keep happening'.
The timeline has no entry on Lean itself or the Lean FRO before 2026-09-29.
The Lean FRO has about 20 people; the official kernel is fixed; the comparator, which exports proofs and rechecks them in a sandbox, now always pulls the latest nanoda; bounties for kernels and a simpler kernel are only ideas under discussion.
The record's mathematics entries are about single results and carry no figure on Mathlib's size or growth.
Mathlib 3 stopped at 1.1 million lines and Mathlib 4 is at 2.4 million, up 44% since 2025 while compile time fell 10%; with AI writing mathematics, he says the library can grow faster than they can speed Lean up.
When AI produces more proof than anyone reads line by line, the checker is the one point of trust, and by de Moura's account AI is also best at finding its holes. So a result 'proved in Lean' should be read with how many independent kernels checked it and whether a comparator-style recheck ran. That is our reading of his account.
In the zlib example the machine proved the property people chose and nothing they did not. He puts people at the specification, the definitions, Mathlib's roadmap and how key proofs are written. Review effort belongs on whether the formal statement is the problem meant.
In his account, a paper whose background is missing means building the infrastructure first; the gap between 2.4 million lines and an estimated 100 million is where AI is most likely to speed things up, and where people most need to keep the structure sound.
A Lean 'disproof' of Collatz was accepted by the official kernel and by nanoda before its fix, through two different bugs; his team 'strongly believes' an AI built it, and the submitter called the overlap a coincidence.
Company-reported
De Moura's account; the Lean issue and fix the transcript cites were not opened for this page. That an AI built it is an inference, not a finding.
He has fixed the official kernel's bug; the comparator would have rejected the proof had it used the latest nanoda, and it now always downloads the latest version.
Current system
De Moura's description; no written account from the Lean FRO was read.
A Claude agent translated zlib from C to Lean, passed the C test suite and proved that decompression restores what was compressed; the optimised version 'beats our implementation in Rust'.
Company-reported
The project is Kim Morrison's at the Lean FRO, described by de Moura; which Rust implementation 'ours' means and by how much it was beaten are not said.
Mathlib 3 stopped at 1.1 million lines and Mathlib 4 has 2.4 million; up 44% since 2025, with compile time down 10%.
Company-reported
De Moura's figures; the underlying count was not read.
To formalise any research-level paper, Mathlib needs about 100 million lines.
Industry context
A community estimate he relays, with no source given.
For OpenAI's disproof of the unit-distance conjecture, Boris Alexeev submitted a Lean proof of 1.2 million lines.
Industry context
Cited to show proofs grow too large to read; the proof was not read for this page.
Models beat people at combining known tricks and fail at inventing new ones; GPT 5.6 and Claude Fable outperform Monte Carlo tree-search systems, but which is cheaper is unsettled.
Guest's judgment
His judgment; the cost point relays colleagues' experiments at a conference, with no figures.
The kernel is not yet proved correct; for executables the compiler is trusted too, and it is not verified.
Not yet closed
Stated plainly by de Moura, and named as the work ahead.
Whether the Lean FRO publishes a written account of both bugs, and whether any later AI-built exploit gets past the comparator.
Would show up as The Lean FRO's own post-mortem, or a new kernel soundness issue.Whether Lean4Lean is completed as a kernel fully proved correct, covering the parts this exploit used.
Would show up as A complete correctness proof released by Mario Carneiro.Whether AI mathematics results claimed as 'proved in Lean' state which kernels checked them and whether the comparator ran.
Would show up as The check record in the paper or repository itself.Partly answered AlphaProof Nexus's Science paper (8 October) states its check: every proof validated with SafeVerify against the theorem statement and guarded against exploits such as injected axioms, with each statement checked by team experts, but not which kernel ran or whether a second one rechecked. Peking University's Poincaré formalisation (6 October) reports an independent-kernel recheck; OpenAI's 722 manuscripts (6 October) say only that many but not all are formalised.Whether Formal Frontiers names its milestone theorems, and whether an AI-built library reaches one.
Would show up as A list from the Mathlib Initiative and a proof that passes the check.Whether lean-zip's claim to beat Rust is published with benchmarks.
Would show up as Benchmark results in the repository naming the comparison, the data and the hardware.Later evidence that tests or limits what was said, and targets whose date has passed.
A Peking University team's agent-built Lean formalisation of the Poincaré conjecture reports a full build, a check against target statements written only with Mathlib, and a recheck by an independent kernel: the extra kernel and statement check de Moura describes. Whether the statements say what Perelman proved is still left to human review, as his point that a proof certifies only the specification predicts.Timeline entry →
OpenAI posts 722 mathematics manuscripts, says many but not all are formalised, and Altman says three of the four headline results have Lean proofs. It is the scale de Moura describes, too large for anyone to read line by line; and a Lean proof checks each step, not that the formal statement is the open problem.Timeline entry →
AlphaProof Nexus is published, peer-reviewed, in Science. The paper says every proof was validated with SafeVerify against the theorem statement, a guard against environment exploits such as injected axioms; team experts checked each of the nine Lean statements against Erdős's question, and the agent's proofs exposed an ambiguous 'density' in two problems, which were restated and still solved. It bears out de Moura's point that a proof certifies only the statement written, and that people must review the statement. The paper does not say whether a second kernel rechecked the proofs.Timeline entry →
Read 2026.10.08 The show's own full transcript, labelled by speaker, read in full and checked against the episode description. The transcript cites the Lean and nanoda issues and fixes behind the Collatz incident; this page did not open them, so that account is de Moura's. Open the interview ↗Podcast episode page ↗The show's full transcript (ReScript) ↗