Weekly
News about Lean, the theorem prover and programming language.
Edition 26: 18 items published for Aug 15 to Aug 27, 2026.
Daniel Selsam used OpenAI internal models to find soundness issues in the official Lean kernel and runtime from July 30 to August 20, and Lean v4.33.1, released August 21, fixes all of them. Starting with Lean v4.35.0, lake check will export and recheck projects using lean4checker.
Checked against: leodemoura.github.io
The roadmap covers lake check commands for external kernel checking, a code formatter, Nerodia (a Lean/Python FFI inspired by PyO3), and faster typeclass inference. It also covers the FRO's AI projects Tau Ceti, Hex, and Palomar, and defers investment in debugger infrastructure.
Checked against: lean-lang.org
Lean v4.33.1 is a patch release with runtime and kernel fixes, including soundness issues reported by Daniel Selsam (OpenAI) using OpenAI's internal models, and all users of v4.33.0 or earlier are encouraged to upgrade. Release candidate 2 for v4.34.0 was published the same day.
Checked against: v4.33.1 release noteslean4 v4.33.1lean4 v4.34.0-rc2v4.34.0 release notes
A merged Lean 4 pull request freezes objects whose 32-bit reference count overflows, preventing a use-after-free in the official kernel. The new logic is validated with a transliteration of its core to Lean followed by correctness proofs in a test file. Daniel Selsam (OpenAI) reported the issue using internal models.
Checked against: lean4#14838
The competition asks participants to improve the performance of verified computation in the Lean 4 kernel (the trusted component that checks every proof accepted by Lean) with optimized implementations and machine-checked proofs of correctness. Stage 1 pre-registration is open, with the official launch on September 15, 2026.
Checked against: @Leonard41111588 on XLinkedIn post
Palomar, a public, searchable registry of machine-checked Lean formalizations incubated by the Lean FRO and ICARM, is now open for submissions, Terence Tao announced. Submitted repository snapshots are checked mechanically with the Lean tool Comparator and by a large language model, though Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.comLinkedIn post
Researchers including Kaiyu Yang, Soonho Kong, Jingxuan He, and Dawn Song introduce Vero, a benchmark of 43 multi-module instances sourced from real-world repositories, each a multi-module Lean 4 repository with predetermined API interfaces. The strongest agent fully solves only 27 of 43 instances.
Checked against: arXiv:2608.13522
Scott Armstrong wrote on X that in March, Lean formalization was not possible for his papers, and by August it had become essential and increased the efficiency of his workflow dramatically. Scott Armstrong says the papers are getting written informally and finished much faster because of the Lean formalization.
Checked against: @scottnarmstrong on X
The Vilin97/MazurTheorem repository targets the classification of rational torsion on elliptic curves, using Mazur's degree-one formal-immersion argument at the auxiliary prime 5. The project reports an integrated score of 17.2% on its 48-node, 1,000-point theorem DAG, and it accepts claims only on contracts marked open or research_open.
Checked against: Vilin97/MazurTheorem
The repository adds passwordless sign-in, SQL migrations, OpenTelemetry traces and logs, an MCP endpoint, and deployment to AWS Lambda, built on Paul Butcher's own Lean libraries. Markup is typed and formally verified (a <div> inside a <p> is a type error), and lean-json is proved correct against the grammar of RFC 8259.
Checked against: paulbutcher/lean-todomvc-max
A pull request by Robin Arnez, merged on 2026-08-20, changes Decidable p to a structure containing a Bool and a proof of either p or ¬p, giving more definitional equalities and letting the decide tactic stop carrying proofs. The breaking change was possible now that the new compiler is enabled.
Checked against: lean4#8309
Sebastian Ullrich merged leanchecker-paranoid, a variant of leanchecker built with allocator hardening, and lake challenge, a frontend to comparator that simplifies its setup. Joachim Breitner's lean-inductive-models performs translation validation of user-defined Lean inductives into an extensional type system with a small hard-coded inductive basis.
Checked against: lean4#14885lean4#14884nomeata/lean-inductive-modelsarena.lean-lang.org
The CSLib Initiative, a program of Renaissance Philanthropy, supports the growth of the CSLib open-source project (a focused effort on formalizing computer science in Lean) in the same way that the Mathlib Initiative supports Mathlib. Its site lists a team, a Strategic Advisory Board, and a roadmap of operational goals guiding its funding.
Checked against: cslib.io
Two merged Lean pull requests by Sebastian Graf state each VERINA program's requires, ensures and loop invariants on the definition itself, for all 27 programs. A second pull request names a verification condition's variables after the program (acc, x instead of b✝), so proofs no longer need rename_i.
Checked against: lean4#14759lean4#14590
A merged pull request by Mac Malone makes Lake fetch dependencies as treeless partial Git clones of a single revision, minimizing the amount of data downloaded. One caveat: Git operations inside a dependency, such as a git blame triggered by a VSCode extension, can cause lazy fetches.
Checked against: lean4#14782
Wojciech Różowski merged a Lean pull request that generates strong_coinduct for coinductive_fixpoint predicates, strengthening coinduct, plus strong_induct for inductive_fixpoint ones. A second merged pull request adds a monotonicity_by clause so users can prove monotonicity of the underlying fixpoint functor with an explicit tactic block when automatic proof search fails.
Checked against: lean4#14855lean4#14861
Leo de Moura's course "Lean 4 for Program Verification in the Age of AI" at the Marktoberdorf Summer School in Herrsching am Ammersee, August 2026, covers dependent type theory, programming and proving in Lean, proof automation and AI, and software verification in Lean.
Checked against: leodemoura.github.io
Tim Sweeney called the response "an exemplary handling of a bug in the Lean theorem prover and proof verifier kernel." The bug was discovered in an AI generated proof, a contributor simplified it down to a straightforward reproduction, and the team fixed it speedily.
Checked against: @TimSweeneyEpic on X