Weekly
News about Lean, the theorem prover and programming language.
The leanprover/leansqlite library bundles SQLite and adds interpolated strings that expand to prepared statements, plus iterators over query result rows. A Zulip user, pandaman, shared LeanToDo, an experiment in building a web application with Lean that uses leansqlite for its database and Verso for HTML templating.
Checked against: leanprover/leansqliteleanprover.zulipchat.com
The change lets the module system, in cooperation with the linker, keep tactics used only in proofs out of the final native binary. A simple example using meta import Lean shrinks from 130MB to 1.7MB. As a breaking change, importModules (loadExts := true) must now be preceded by enableInitializersExecution.
Checked against: lean4#12016
Gavin Mendel-Gleason reports that opencode, GPT-5.2 and lean-lsp-mcp produced a provably correct citation streaming program for a RAG answering system in two hours with no interventions. Gavin Mendel-Gleason argues that LLMs increase software generation faster than software understanding, and calls the approach vericoding (vibe-coding using programme verification).
Checked against: LinkedIn post
In a LinkedIn post, Stan Fedotov argues the field is "moving towards automated verification in most domains," while noting Lean is "only useful when the standard library supports your field." In one paper, only a somewhat elementary part of the proof was verified in Lean, while the authors proved the deeper parts.
Checked against: LinkedIn post
Lean now identifies instance parameters by type using isClass? instead of binder syntax, dsimp no longer simplifies instances by default, and isDefEq no longer raises transparency to .default for implicit arguments, a change the PR calls very disruptive. Old behavior is available through backward.* options, and the PRs cite problems in Mathlib.
Checked against: lean4#12172lean4#12195lean4#12179
Willem Vanhulle is putting together a TUI (a terminal-only user interface) for Lean4 users, built with Ratatui. The TUI has several display modes with different display styles for on-going mathematical proof development, and documentation is available.
Checked against: LinkedIn post
Leo de Moura, Chief Architect of the Lean FRO, reviewed 2025 at Lean Together in January 2026: 12 releases, a new compiler fully implemented in Lean, and the grind proof-automation tactic. The talk also said 2026 will be the last year with significant changes to the language and standard library.
Checked against: slides (pdf)
A new benchmark in the lean4 test suite, described as a synthetic benchmark from the Lean@Google Hackathon, compares a MetaM tactic solution with SymM solutions, including a "SymM Solution + reusing simplifier cache" variant, on generated command sequences of up to 700 iterations, also timing kernel checking.
Checked against: leanprover/lean4
A Proofs and Intuitions post walks through Velvet, a verifier embedded in Lean as a library and developed by VERSE Lab. Velvet discharges most proof obligations with SMT solvers (such as Z3 and cvc5) and tactics like grind, then leaves the rest for interactive proof. In the example, Claude Code and Harmonic's Aristotle each finished the remaining proof.
Checked against: proofsandintuitions.net
Yann Fleureau announced Numina-Lean-Agent, an open-source agentic framework for autoformalization and theorem proving using generic AI models. The announcement reports 12/12 on Putnam 2025 and a formalization of the "Effective Brascamp-Lieb inequalities" research paper, more than 90% of it AI-generated.
Checked against: LinkedIn post
Three merged Lean 4 pull requests by Leo de Moura extend Sym.simp: a simplification procedure evaluating ground terms of builtin numeric types such as Nat, Int and BitVec n, support for conditional rewriting rules, and offset terms, essential for equational theorems of functions that pattern match on natural numbers.
Checked against: lean4#12031lean4#12033lean4#12053
Alexandre Rademaker says the course is probably the first Lean course taught in Portugal and is an official World Logic Day 2026 event. It uses The Hitchhiker's Guide to Logical Verification and is partly supported by Atlas Computing via a Schmidt Sciences grant.
Checked against: LinkedIn post
In a LinkedIn post, Martin Ciupa recaps the conversation, in which Terence Tao calls automating formalization (turning ordinary math into proof-assistant-checked form) the near-term change, stresses formal verification over trusting AI blindly, and highlights Lean-style autocomplete that fills a line or two at a time.
Checked against: LinkedIn post
AxiomProver, an autonomous AI theorem prover built by Axiom, solved 12 out of 12 problems from the Putnam Competition, 8 of them within the strict exam time limit, producing formal proofs in Lean. One combinatorial step in Problem A5 required 2,054 lines of formal proof.
Checked against: LinkedIn post
A pull request by Sebastian Ullrich bundles all Init module files into a single file with cross-sharing, reducing cumulative size from 325MB to 264MB and openat calls for import Init on Linux from about 2000 to about 80. The pull request is still open.
Checked against: lean4#11965
A Hacker News thread on the claim that Erdos problem #728 "was solved more or less autonomously by AI" drew 619 points and 363 comments. A Harmonic employee said Aristotle, the company's system, can translate an informal English proof into Lean, and commenters debated how to check that a theorem statement is formalized correctly.
Checked against: news.ycombinator.com
Lean Together is an annual meeting for users, developers, and fans of the Lean programming language and theorem prover, covering formalized mathematics, software verification, infrastructure, and outreach. The meeting is open to everyone without cost, and talks will be recorded with speakers' permission and posted to the leanprover community YouTube channel.
Checked against: leanprover-community.github.io
A merged Lean pull request by Leo de Moura improves the proof term produced by mkFunext, which Sym.simp uses when simplifying lambda expressions. For a 200-lambda benchmark, kernel checking time fell from 148.681 ms to 6.903 ms, and the approach will later come to Meta.simp.
Checked against: lean4#11932
The Lean Together 2026 schedule includes a mix of casual and more formal presentations, with talks running around four hours each day and staggered start times for different time zones. Recordings of all talks are on the Lean community YouTube channel.
Checked against: leanprover-community.github.io
A merged Lean 4 pull request by Leo de Moura adds performance comparison tests between the new SymM monad and the standard MetaM for intros/apply operations. Results show a 10-20x speedup, rising from 10.8x at size 1000 to 22.0x at size 6000.
Checked against: lean4#11838leanprover/lean4
Math, Inc. posted a full conversation in which Fields medalist Terry Tao sits down with Math Inc's @jessemhan and @jdlichtman to discuss the future of mathematics. Terry Tao says this style of writing proofs shows the inputs and outputs of a proof more clearly and predicts that "the definition of a mathematician will broaden."
Checked against: @mathematics_inc on X
Logical Intelligence posted on X an AI-generated, formally verified compiler from λ-calculus to CPS, written in Lean4. The post explains formal verification as code that comes with a mathematical proof, checked by the computer, that it works correctly in all cases, not just the ones tested.
Checked against: @logic_int on X