Lean is a programming language designed as a proof assistant, for formally verifying software and mathematical theorems. It uses a dependent type system based on the Calculus of Inductive Constructions, similar to the older Rocq Prover.

Lean was first developed by Leonardo de Moura at Microsoft Research, where he released Lean1 in 2013. The current version is Lean4 (released in 2021 and backwards-incompatible with Lean3). It has gained substantial traction, first with the mathematics community, who have worked to encode much of modern mathematics into the library Mathlib, and then as a tool for use with LLMs. In 2023 work on the Lean project was moved into its own organization.