Learn Lean
Core documentation
Functional Programming in Lean (FPIL) is the main resource for programmers who want to learn Lean. It assumes a background in programming, but no prior knowledge of functional programming is needed.
Theorem Proving in Lean (TPIL) is designed to teach you to develop and verify proofs in Lean and covers dependent type theory, automated proof methods, and Lean-specific features for interactive theorem proving.
Mathematics in Lean (MIL) is the main resource for mathematicians who want to learn mathematical formalization through interactive, tactic-based theorem proving using Lean's Mathlib library.
The Lean Language Reference is a comprehensive, precise description of Lean: a reference work in which all aspects of Lean are clearly specified, and demonstrated through succinct examples.
Further reading
The Mathlib API reference - Includes reference information for Lean core, the Lean standard library, Mathlib, and other critical Lean packages.
The Hitchhiker's Guide to Logical Verification - Originally designed as a companion text for a graduate-level course on interactive theorem proving at Vrije Universiteit Amsterdam.
Logic and Proof - A textbook teaching the basics of classical logic, such as propositional logic, first order logic, natural deduction and axiomatic reasoning, using Lean.
The Mechanics of Proof - Originally written as a companion text to the course Math2001 at Fordham University, it teaches the basics of mathematical reasoning to students of mathematics using Lean.
Lean 4 VS Code extension manual - Describes how to interact with Lean 4 using the most the VS Code extension.
Interactive Games and Tutorials
The Natural Number Game - A gamified introduction to mathematical proof that introduces Lean 4 concepts through a purpose-built Lean 4 dialect.
The Lean Game Server - A collection of games similar to the Natural Number Game.
Resources
Loogle! - A Lean and Mathlib search tool for finding definitions and lemmas, available on the web, via CLI or through IDE extensions.
LeanExplore - A natural language search engine for Lean declarations, indexing commonly used Lean libraries.
LeanSearch - A Mathlib search engine for finding tactics and theorems via natural language queries.
LeanDojo - A tool for data extraction and interacting with Lean programmatically.
REPL - An interactive Read-Eval-Print Loop (REPL) for Lean intended for machine-to-machine interaction and AI applications.
Pantograph - A machine-to-machine interaction system that provides interfaces to execute proofs, construct expressions, and examine the symbol list of a Lean project for machine learning.
Lean4Web - A web-based version of Lean that allows you to run Lean code directly in your browser.
How to cite Lean
Lean 4
To cite Lean 4 please reference The Lean 4 Theorem Prover and Programming Language published in CADE-28 - The 28th International Conference on Automated Deduction. PDF
Lean 3
To cite Lean 3 please reference The Lean Theorem Prover (System Description) published in Lecture Notes in Computer Science. PDF.