What's new in the Lean standard library

Abstract: The Lean standard library contains the basic concepts that underpin all Lean formalization and programming projects, like logical connectives and natural numbers. It also contains fundamental building blocks for writing real-world software in Lean, like high-quality implementations of data structures and primitives for parallel programming. In 2025, the Lean standard library team added many new features that are essential for building production-ready software in Lean. We will go over the new features and show how they make Lean an even more powerful tool for writing general-purpose (verified) software and, of course, metaprograms.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026