Weekly
News about Lean, the theorem prover and programming language.
Edition 28: 14 items published for Sep 3 to Sep 17, 2026.
XTX Markets announced $10mn to Lean FRO, a focused research organisation run by Convergent Research, and $10mn to the Mathlib Initiative, each covering core operating costs to 2030. XTX Markets says Lean provided the verification layer in the auto-formalisation of Fermat's Last Theorem.
Checked against: xtxmarkets.com
Working largely autonomously over 11 days, Claude wrote 13 million lines of Lean (over 5x the size of Mathlib, the principal community library) and proved 29,500 intermediate theorems. Kevin Buzzard compiled the code and ran comparator on it, and the full proof is on GitHub with a written walk-through.
Checked against: anthropic.comxenaproject.wordpress.comanthropics/fermats-last-theoremnature.com
OpenAI said 10,000 autonomous AI agents found a singularity in the Navier-Stokes equations in three dimensions, with the result formally checked in Lean. Hours earlier, Tristan Buckmaster at New York University and Levent Alpöge at Anthropic reported Lean-verified proofs for three related results, including one for the Euler equations.
Checked against: quantamagazine.orgblog.computationalcomplexity.org
Lean 4.34.0, released 2026-09-14, fixes three soundness issues found with AI adversarial testing and adds defensive kernel checks. bv_decide gets integrated with sym and grind interactive modes and is up to six times faster, linters can carry state across commands, and lake lint gains a --code-quality mode emitting machine-readable JSON.
Checked against: v4.34.0 release notes
In under two weeks, Certora built an experimental C-to-Lean pipeline and proved that the Clight (CompCert's C intermediate representation) model of zlib's 266-line inflate_table function is memory-safe and terminating. The proof, around 20,000 lines of Lean, was written almost entirely by LLMs, and the Lean kernel checked every step.
Checked against: certora.com
The multi-stage competition seeks faster algorithms for verified computation (using the Lean kernel to check computational results in a proof) across eight problems, including Fibonacci, prime counting, Rule 110, and SHA-256. Entrants prove each algorithm matches its specification; submissions close November 20, 2026.
Checked against: terrytao.wordpress.comcompetition.sair.foundation
con-leche is an external checker for Lean, proven in Lean never to accept a proof of False, implemented and proven by Claude (Fable and Opus) under heavy supervision by Joachim Breitner at the Lean FRO. On the FLT proof by Anthropic, it accepted 1,044,222 declarations in 2 h 22 min wall time.
Checked against: leanprover/con-lecheleanprover.zulipchat.com
A meta issue by Arthur Adjedj, worked out with @nomeata, plans kernel changes that move feature selection for inductives to the elaborator and aim for a decidable, transitive definitional equality algorithm. Recursive predicates like Acc would lose large elimination, and the kernel changes would ideally ship in a single release.
Checked against: lean4#14977
On a 1,000-module slice, adopting the module system and import minimization cut task-clock to 3,268 s (down 63.1%) and wall-clock to 140 s (down 86.3%). Sebastian Ullrich also released the proof as a single 1.01 GiB .olean download that can be run through lean4export for external checkers.
Checked against: hackmd.iofermats-last-theorem export
The leanprover/hex repository bundles the released hex libraries for verified computational algebra in Lean 4, including LLL lattice reduction, integer polynomial factorization, graph canonical labelling via a formalization of nauty, and algebraic numbers. Each computational library is Mathlib-free, with Mathlib correspondence proofs in separate theory libraries.
Checked against: leanprover/hex
con-ron ports con-leche, an external Lean checker with a formal consistency proof, to Rust. It was written by AI under supervision from Joachim Breitner, and its Rust code is proven (partially) correct via an Aeneas-generated model, so checking a proof with both tools guards against compiler or runtime bugs.
Checked against: leanprover/con-ron
Julia Markus Himmel merged a change that compiles mimalloc as part of the Lean runtime, and Sebastian Ullrich moved rarely-updated Core.Context fields into a cold subobject (mathlib4: -0.82% instructions, -2.03% wall-clock). Lean also updated to mimalloc 3.4.5, fixing a Windows memory leak, and CI changes should halve merge queue run times.
Checked against: lean4#15017lean4#14982lean4#15060lean4#15123
Two merged pull requests add Lean.Data.Html, a type of HTML forests aimed primarily at authoring HTML, with a renderer that produces a String, plus HTML-like syntax with an elaborator into that type. Companion downstream-lean4 pull requests adopt the type and syntax throughout supported packages.
Checked against: lean4#14935lean4#15002
Greg Brockman says OpenAI pointed Astra at its own systems until it ran out of vulnerabilities to find, putting 25% of its production engineers on defense. Greg Brockman added: "There are ideas, for example, formally verifying all of software, that are possible with AI."
Checked against: @a16z on X