Weekly
News about Lean, the theorem prover and programming language.
Lake adds Dynlib.runtimeOnlyDeps, for transitive dependencies that should not be linked but must be preloaded when precompiling, plus an API for retrieving the complete set of core dynamic libraries. A third change lets custom build targets link shared libraries or executables from a module without copying the code in LeanExe.recBuildExe.
Checked against: lean4#14254lean4#14220lean4#14219lean4#14240
ArkLib, a project supported by the Ethereum Foundation, mechanizes the probabilistic security proofs that succinct non-interactive arguments of knowledge (SNARKs) depend on. It gives zk engineers and cryptography researchers machine-checked specifications and executable references for proof systems where a single soundness bug can be catastrophic.
Checked against: lean-lang.org
A merged pull request by David Thrane Christiansen adapts Lean's deferred docstring check mechanism to use the linter mechanism, replacing custom CI setup with an interface akin to environment linters and governed by the option linter.doc.deferred. In a breaking change, custom Verso docstring elements now use a two-constructor type.
Checked against: lean4#14206
Gwern Net's research proposal would measure coding LLM perplexity over growing codebase context to estimate scaling laws of predictability by language. The essay predicts Lean suffers from a very high constant but would have the best scaling exponent, and so would eventually cross over more popular languages such as Python.
Checked against: gwern.net
A merged pull request by Joachim Breitner makes Lean suggest try? output for empty by blocks, unsolved goals, and sorry tactics, gated by three options that default to off. It replaces the tactic.tryOnEmptyBy option from an earlier pull request with a different implementation.
Checked against: lean4#13830
In a post on X, Dwarkesh Patel described Grant's speculation that AIs could fork Mathlib, the Lean library of formalized math concepts and proofs, and build a "parallel math civilization." Dwarkesh Patel wrote that Lean guarantees any new conjectures would be logically valid, and that whether they would be interesting is another matter.
Checked against: @dwarkesh_sp on X
Mistral AI's documentation lists Leanstral 1.5, dated June 30, 2026, as an updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. The Apache 2.0 model has 119B total parameters (6.5B active) and a 256k context, though the page marks it deprecated with a deprecation date of 9/29/2026.
Checked against: docs.mistral.ai
A now-closed pull request adds stateful linters: command linters that thread state from one command to the next, so a linter can accumulate information across a file. A merged pull request adds a hint to the unusedVariables linter, suggesting to rename the unreferenced name with an underscore.
Checked against: lean4#14225lean4#14259
In a June 2026 talk, Leo de Moura (Senior Principal Applied Scientist, AWS, and Chief Architect, Lean FRO) described AWS projects built with Lean, including Cedar, a verified authorization policy language, SampCert, verified differential privacy, and Waimea, a tensor compiler for Trainium. The slides are written in Verso.
Checked against: leodemoura.github.io
A merged Lean pull request by Henrik Böving adds optional diagnostics, enabled via grind.ematch.diagnostics, that flag instances with many direct follow-up children and instances that participated in a large, transitive closure of follow-up instances. The metric is based on the cost heuristic of smt-scope, and thresholds are configurable.
Checked against: lean4#14118
A merged Lean pull request lets custom elements in Verso docstrings define their own Markdown rendering, which is used for LSP hovers and for legacy clients that don't directly support Verso. Example uses include including one docstring in another and showing all currently-available instances of a class.
Checked against: lean4#14115
Sebastian Graf merged pull requests renaming the experimental Sym-based mvcgen' tactic to vcgen, speeding up its matching, and adding a frames clause. A new @[frameproc] attribute lets a program type register how it frames a resource, so cost budgets, separation-logic footprints, and trace invariants frame through the same mechanism.
Checked against: lean4#14195lean4#14146lean4#14167lean4#14134
A merged pull request lets about 389 elab tests that use import Lean reuse one pre-built snapshot, cutting CPU time by 26.0% (2222 s to 1645 s), with CI test wall-clock speedups of about 10-40% depending on platform. Related pull requests speed up .olean and snapshot serialization, one cutting snapshot save time by about 28%.
Checked against: lean4#14077lean4#14109lean4#14122
Julia Markus Himmel added Float.Model, a pure Lean implementation of 64-bit floating-point numbers, and made Float a wrapper around it, so float operations are no longer opaque to the kernel while compiled code still uses native operations. Users can now prove 0.1 + 0.2 != 0.3 with rfl.
Checked against: juliahimmel.delean4#14079lean4#14091lean4#14110
Sebastian Graf merged a port of the experimental mvcgen' tactic to the new Std.Internal.Do meta theory, where loop invariants no longer restate the exceptional postcondition. A follow-up extracts a WP type class from WPMonad, enabling verification of deeply embedded languages, tested on an IMP language whose WP instance has no accompanying WPMonad.
Checked against: lean4#14080lean4#14015
Paul Reichert's merged pull request makes Lean compare metavariable types at implicit transparency instead of default, building on Kim Morrison's split of transparency into implicit and instances levels (merged on 2026-06-19). Some lemmas may stop applying in simp or grind; set_option backward.isDefEq.respectTransparency.types false restores the old behavior.
Checked against: lean4#13895lean4#13637
A merged pull request by Henrik Böving changes the m_imp field of lean_task to an atomic. get_task_state_core read m_imp to check whether a task had finished before taking the mutex, so that memory access was undefined behavior (UB).
Checked against: lean4#14108
Software Foundations, a series of textbooks on formal proof and foundations of programming languages formalized in Rocq, is being translated to Lean for Fall courses at Penn and elsewhere. Benjamin Pierce says the team is ready to add a few people, especially educators, and will need alpha-testers later in the summer.
Checked against: leanprover.zulipchat.com
A pull request by Mac Malone, merged into leanprover/lean4, has Lake deduplicate artifacts by their hash when uploading or downloading to the cache (for example in lake cache put or lake cache get). The change fixes possible errors when curl was asked to transfer to the same file or URL multiple times.
Checked against: lean4#14060
Lean 4.31.0 lands 305 changes, including while let loops in do blocks, a built-in Lake linting framework, stricter transparency handling in definitional-equality checking, and the experimental mvcgen' tactic, which can outperform mvcgen by over 100x on some synthetic benchmarks. The bundled toolchain moves from LLVM 19 to LLVM 22.
Checked against: v4.31.0 release noteslean4 v4.31.0
A merged Lean 4 pull request by Wojciech Różowski makes the cbv tactic available inside grind's interactive sym => mode. The tactic reduces the goal using call-by-value evaluation, supports at locations for hypotheses, and closes equation goals via refl when reduction finishes the proof.
Checked against: lean4#13971
Quanta Books published The Proof in the Code on June 9, 2026, in which Kevin Hartnett tells the story of the birth and rise of Lean, from a bug-checking program at Microsoft Research developed by Leo de Moura to its adoption by mathematicians and tech firms.
Checked against: amazon.com
Pull request leanprover/lean4#12030, "feat: link OpenSSL" by Sofia Rodrigues, was merged on 2026-06-05. The pull request was opened on 2026-01-16 and describes its change as linking OpenSSL.
Checked against: lean4#12030
Peter O'Hearn is hiring a postdoc in the Meta London office who will work closely with Peter O'Hearn and others in the new AI Verification team, collaborating across Meta Superintelligence Labs and possibly building on lean/CSLib, Iris-Lean and loom/velvet.
Checked against: LinkedIn post