The Lean Language Reference

The Lean Language Reference

Table of Contents

1.	Introduction
2.	Elaboration and Compilation
3.	Interacting with Lean
4.	The Type System
5.	Source Files and Modules
6.	Namespaces and Sections
7.	Definitions
8.	Axioms
9.	Attributes
10.	Terms
11.	Type Classes
12.	Coercions
13.	Tactic Proofs
14.	Functors, Monads and `do`-Notation
15.	IO
16.	The Simplifier
17.	The `grind` tactic
18.	The `mvcgen` tactic
19.	Basic Propositions
20.	Basic Types
21.	Notations and Macros
22.	Run-Time Code
23.	Build Tools and Distribution
	Error Explanations
	The Module System
	Release Notes
	Supported Platforms
	Index

Release Notes

	Lean 4.26.0-rc1 (2025-11-19)
	Lean 4.25.1 (2025-11-18)
	Lean 4.25.0 (2025-11-14)
	Lean 4.24.0 (2025-10-14)
	Lean 4.23.0 (2025-09-15)
	Lean 4.22.0 (2025-08-14)
	Lean 4.21.0 (2025-06-30)
	Lean 4.20.0 (2025-06-02)
	Lean 4.19.0 (2025-05-01)
	Lean 4.18.0 (2025-04-02)
	Lean 4.17.0 (2025-03-03)
	Lean 4.16.0 (2025-02-03)
	Lean 4.15.0 (2025-01-04)
	Lean 4.14.0 (2024-12-02)
	Lean 4.13.0 (2024-11-01)
	Lean 4.12.0 (2024-10-01)
	Lean 4.11.0 (2024-09-02)
	Lean 4.10.0 (2024-07-31)
	Lean 4.9.0 (2024-07-01)
	Lean 4.8.0 (2024-06-05)
	Lean 4.7.0 (2024-04-03)
	Lean 4.6.0 (2024-02-29)
	Lean 4.5.0 (2024-02-01)
	Lean 4.4.0 (2023-12-31)
	Lean 4.3.0 (2023-11-30)
	Lean 4.2.0 (2023-10-31)
	Lean 4.1.0 (2023-09-26)
	Lean 4.0.0 (2023-09-08)
	Lean 4.0.0-m5 (2022-08-22)
	Lean 4.0.0-m4 (2022-03-27)
	Lean 4.0.0-m3 (2022-01-31)
	Lean 4.0.0-m2 (2021-03-02)
	Lean 4.0.0-m1 (2021-01-04)

Lean 4.25.1 (2025-11-18)

Source Code
Report Issues

←Lean 4.26.0-rc1 (2025-11-19)Lean 4.25.0 (2025-11-14)→

Lean 4.25.1 (2025-11-18)🔗

Lean v4.25.1 is a bug fix release fixing a caching problem in lake, affecting certain downstream dependencies of ProofWidgets4.

←Lean 4.26.0-rc1 (2025-11-19)Lean 4.25.0 (2025-11-14)→