The State of Lean

Abstract: 2025 has been a transformative year for Lean. We released 12 versions (4.15–4.26), landing thousands of changes across proof automation, the compiler, tooling, website, documentation, and the standard library. The grind tactic shipped with SMT-style automation and interactive proof search. The new compiler replaced the old one, closing long-standing issues and setting the foundation for future optimizations. Lake gained remote caching and a local artifact cache. The language server became significantly faster (3.5× autocomplete speedup), added signature help, and introduced module hierarchy navigation. We released the module system, coinductive predicates, and a monadic verification framework (mvcgen). The standard library expanded substantially with iterators, async primitives, and hundreds of new lemmas. We launched a new website and published the Lean Language Reference, both built with Verso. This keynote summarizes these accomplishments and outlines our priorities for 2026.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026