{{language|Lean
|exec=machine
|strength=strong
|safety=safe
|checking=both
|gc=yes
|LCT=yes
|site=https://lean-lang.org/}}
{{language programming paradigm|functional}}
{{language programming paradigm|dependent-types}}

'''Lean''' is a dependently typed programming language and proof assistant, similar to [[Rocq]] and [[Agda]]. It aims to bridge the gap between interactive and automated theorem proving by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.

As a proof assistant / theorem prover, Lean primarily benefits from Mathlib, a mechanized implementation of swaths of mathematics at the undergraduate and graduate level.

As a general-purpose programming language, Lean benefits from its use as a theorem prover, as several features developed for the purpose of theorem proving, such as its dependent types system and its syntax-rewriting macros, also find much utility outside their original theorem proving contexts.

Lean 4 is the current major version of the language, being a bootstrapped rewrite of the older (and different) Lean 3 system.

=== Citations ===

Frequently asked questions: https://lean-lang.org/faq/