Weekly
News about Lean, the theorem prover and programming language.
Edition 30: 21 items published for Sep 24 to Oct 15, 2026.
Lean 4.35.0, published on 2026-10-12, adds vcgen, a faster and more general successor of mvcgen, plus lake check and lake comparator, which check a project with Lean's kernel and optionally several independent kernels now included in the toolchain.
Checked against: v4.35.0 release noteslean4 v4.35.0
OpenAI's openai/math repository holds manuscripts and proof artifacts produced by an internal OpenAI model, organized into 372 families, with 300 of 719 top-line results formalized in Lean. An October 7, 2026 update withdrew three manuscripts after a sign error and revised 14 others.
Checked against: openai/math
Ziyang Qin, Yuan Liao, Ayush Khaitan, and Bennett Chow formalize the smooth three-dimensional Poincaré conjecture via Ricci flow with surgery and finite-time extinction. Together with the Moise smoothing theorem, the result yields the topological three-dimensional Poincaré conjecture.
Checked against: arXiv:2609.33842
The AI for Math Fund selected 22 applications representing 30 organizations from more than 470 submissions, bringing its total commitments to $35.1 million. Winners include TorchLean, a Lean-native framework for verified machine learning, and a project turning a Lean 4 visual proofwriting prototype into open-source infrastructure for reading AI-generated proofs.
Checked against: renaissancephilanthropy.org
A paper in Science by George Tsoukalas, Swarat Chaudhuri and coauthors describes an agent for formal proof search that autonomously resolved nine of 353 open Erdős problems and proved 44 of 492 On-Line Encyclopedia of Integer Sequences conjectures. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes.
Checked against: science.org
A repository by @dpwoodru contains a complete, machine-checked Lean 4 proof of the general Courtade–Kumar inequality (the most informative Boolean function conjecture), formalizing the paper by Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair and D. P. Woodruff. The whole proof spans 45,500 modules.
Checked against: dpwoodru/general-courtade-kumar-lean
Scott Armstrong writes that autoformalization of research-level mathematics has become easy, citing a Lean formalization of a 145-page paper with Vicol in about 36 hours (270k lines of code), and makes the agent skill files public. A separate Xena post weighs mathematicians' reactions to AI, noting "You cannot fool Lean."
Checked against: scottnarmstrong.comxenaproject.wordpress.com
Google's launch post for Gemini 4 Argon (dated 2026-10-13) reports an arcsin implementation, a building block in recent quantum simulation algorithms, written by Argon and formally verified in Lean. It cuts spacetime cost by more than 100x compared to a published quantum CORDIC baseline.
Checked against: blog.google
During an audit of the Miden VM, a zero-knowledge VM with its own assembly language, Trail of Bits had agents build a Lean model of the VM executor, producing 95 correctness proofs covering all binary arithmetic components of the core library. The work identified two subtle bugs that the existing unit test suite did not catch.
Checked against: blog.trailofbits.com
SymCert, implemented in Lean, builds verified SMT-based analyses of Cedar policies, an open-source authorization language. In the FMCAD 2026 paper, five analyses used in a Cedar analysis service at Amazon Web Services were modeled and proved in one work day, and three extensions for new Cedar features took 4 to 8 days each.
Checked against: paper (pdf)
Flapjack is bringing the Pancake compiler, originally verified in HOL4, and its proofs to Lean, with a path compiling a fragment of Pancake to RISC-V where all stages except parsing and AST conversion have a correctness theorem. A MIPS32 backend targets the Ziren zkVM, but its output has been run only on Ziren's Lean model.
Checked against: flapjack-lang.dev
A pull request by Sebastian Graf documents the vcgen tactic and its Std.WP framework, adds the tutorial "Verifying Imperative Programs Using vcgen", and moves the mvcgen chapter and tutorial to their own files. The Kraken project already uses vcgen to prove that FFmpeg's FMA3 dot-product loop, over two arrays that may alias, terminates without faulting.
Checked against: reference-manual#927zrlk/kraken
Two merged pull requests by Sebastian Ullrich keep type class resolution results for later commands and let queries differing only in free variables share a cache entry. Building Mathlib takes about 4% fewer instructions and 8% less wall-clock time, and spends about 16% less time in type class resolution.
Checked against: lean4#14369lean4#14316
con-leche, a checker for Lean 4, comes with a proof in Lean that every environment it accepts has a model in set theory, so no accepted environment holds a proof of False. A new document gives a pen-and-paper account of that argument on a simplified fragment of the checker.
Checked against: leanprover.github.io
A merged pull request by Sebastian Ullrich removes the limit of 255 object fields per constructor, and thus per structure. When a constructor has more, the compiler keeps the first 254 in the constructor object and stores the rest in a chain of spill objects, with one pointer followed per spill object on access.
Checked against: lean4#15516
Julia Markus Himmel redefined the order on String as the lexicographic order of its UTF-8 encoding, made Min Float follow the IEEE-754-2019 minimum operation, and added missing order instances for BitVec, List, Array, Vector and ByteArray. Sofia Rodrigues fixed leaks and refactored the libuv bindings.
Checked against: lean4#15581lean4#15257lean4#15274lean4#15304lean4#15329lean4#15175lean4#15545
Wojciech Nawrocki merged pull requests adding Lean.Data.Html, a type of HTML forests aimed at authoring HTML, with a renderer to String, plus HTML-like syntax and an elaborator into that type. Separately, Emilio Jesús Gallego Arias added optional VIR support and a small Lean-to-JavaScript client example on Lean 4.35 to Verso Blueprint.
Checked against: lean4#14935lean4#15002verso-blueprint#491
A merged Lean pull request adds backward.grind.normalizer, which switches grind to the Sym.simp-based normalizer when set to false (the default behavior is unchanged). Related changes add grind_norm, a debugging tactic whose check mode runs both normalizers and fails when results differ, and fix negation-pushing rewrites that had been dead code since #9271.
Checked against: lean4#15464lean4#15375lean4#15378
In Lean, an asynchronously elaborated theorem's exported info in a module is now available as soon as its signature is, instead of after its proof is elaborated. A second change stops modules from exporting constants such as foo.eq_1 realized only inside a proof, so such proofs no longer trigger downstream rebuilds.
Checked against: lean4#15559lean4#15563
A merged pull request by Jason Reed adds a Publish button to the project summary when a workbench-publication.json file configures Verso builds. Clicking it runs a Verso build and serves the result on a route extending the project URL. A follow-up makes publications create temporary directories in roughly the same way as tracked commands.
Checked against: lean-workbench#139lean-workbench#149
A Mathlib pull request by Kim Morrison adds a supply-chain audit step to the hourly update_dependencies.yml workflow, posting diffs, high-risk files touched and suspicious added lines for each changed dependency. The diffs come from paranoid-lake-update, which uses bare clones and git only, so nothing from upstream is executed.
Checked against: mathlib4#43911