🧮Lean 4 — Proof Engineering

Bibliothèque

17 sources primaires et références sélectionnées.

Official hub

Learn LeanLean FRO — Official map of core books, reference material, games, tools, and search services. — Use this as the canonical entry point when the ecosystem changes.

Book

Functional Programming in LeanDavid Thrane Christiansen / Lean FRO — Programming-first treatment of data, type classes, monads, dependent types, proofs, and performance. — Primary backbone for the programmer track.Theorem Proving in Lean 4Lean FRO / Lean community — Foundations, proof terms, tactics, inductive types, recursion, structures, type classes, and axioms. — Primary conceptual backbone for theorem proving.

Reference

Lean Language ReferenceLean FRO — Precise, versioned reference for syntax, type system, tactics, runtime, IO, macros, and build tools. — Consult after a tutorial gives intuition and exact behavior matters.

Book + exercises

Mathematics in LeanJeremy Avigad and Patrick Massot — Tactic-based mathematical formalization from logic and sets through algebra, topology, calculus, and measure. — Primary backbone for the mathematician track.Metaprogramming in Lean 4Lean community — Expressions, MetaM, syntax, macros, elaboration, DSLs, tactic implementation, and pretty-printing. — Core text for extending Lean and writing automation.

API reference

Mathlib API DocumentationLean community — Generated documentation for Mathlib, Lean, Std, Batteries, Lake, and related packages. — The authoritative place to inspect declarations and module structure.

Interactive tool

Lean 4 Web PlaygroundLean community — Server-backed editor for small Lean snippets with an InfoView-style experience. — Real verification without a local install; use local projects for serious development.

Game

Natural Number GameLean community — A gamified introduction to proof tactics through elementary arithmetic on natural numbers. — Fastest low-friction introduction to interactive proof construction.

Tool manual

Lean 4 VS Code Extension ManualLean FRO / contributors — Projects, InfoView, diagnostics, theorem search, version management, and editor workflows. — Professional fluency depends on using the editor feedback loop well.

Declaration search

LoogleLean community — Searches declarations by names, constants, subexpressions, and type shapes. — Best when you know the formal shape of the theorem you need.

Semantic search

LeanExploreLean community — Natural-language and hybrid semantic search over major Lean libraries. — Useful when you know the mathematical or programming idea but not its Lean name.

Book + package

How To Prove It With LeanDaniel Velleman — A gentle bridge from informal proof techniques to Lean. — Good remedial path when mathematical proof construction itself is unfamiliar.

Textbook

Logic and ProofJeremy Avigad et al. — Classical logic, natural deduction, first-order logic, axiomatic reasoning, and Lean exercises. — Background path for learners who need explicit logic foundations.

Research paper

The Lean 4 Theorem Prover and Programming LanguageLeonardo de Moura and Sebastian Ullrich — System overview of Lean 4, extensibility, typeclass resolution, macros, and functional-but-in-place execution. — Concise architectural context for advanced users.

Curated guide

Learning Lean 4Lean community — Community-maintained guide to books, games, teaching material, metaprogramming, foundations, and events. — A broad inventory of mature and emerging learning material.

Contributor guide

Contributing to MathlibLean community — Workflow, style, naming, review, and contribution expectations for Mathlib. — The practical bridge from learner to ecosystem contributor.