All things Lean

References for Lean.

I’m tentatively teaching a course on Lean and math formalization in Fall 2027. This is a page to dump various resources for future use. I used to do this a lot in the past but things have been changing so fast that it has been hard to keep up.

Learning Lean

Resource	What it is
Mathematics in Lean	A tactic-focused course for mathematicians, with exercises, built on Mathlib.
Theorem Proving in Lean 4	The official foundations text: dependent type theory, propositions and proofs, inductive types and tactics.
Lean Game Server	Interactive games for learning Lean, including the Natural Number Game.
Lean 4 Web	Lean in the browser, with nothing to install.

Tools

Resource	What it is
Loogle	Search Lean and Mathlib definitions and theorems by type signature or pattern. (source)
LeanSearch, LeanExplore	Search Lean libraries in natural language, which helps when you don’t yet know the Lean name.
Verso	A platform for writing documents, books, course materials and websites in Lean.
Paperproof	A VS Code extension that shows a Lean proof as a tree, closer to a pen-and-paper proof. Probably most useful for beginners.
leanblueprint	Plan a formalization as a LaTeX blueprint, with a dependency graph linked to the Lean declarations. The standard way to organize a group project. (LeanArchitect generates blueprint data from the Lean code itself.)

AI and Lean

Resource	What it is
LeanDojo	Open-source toolkits, data and benchmarks for machine learning on Lean. (paper)
Lean Copilot	LLM-based proof suggestions and premise search inside Lean.
lean-lsp-mcp	A Model Context Protocol server that gives AI coding agents access to Lean’s goals, diagnostics and search.
REPL, Pantograph	Machine-to-machine interfaces to Lean, which AI tools build on to run proofs and inspect a project.
lean4-skills	Claude Code skills for AI-assisted formalization of your own project, with a draft, prove, review, refactor workflow and autonomy levels from interactive to fully autonomous.
Tau Ceti	A Lean library downstream of Mathlib, written and reviewed largely by AI, with humans setting roadmaps and review rubrics. (repository)
Aristotle	Harmonic’s Lean prover, which can be called from an agent to fill in lemmas. Access is limited.
Kimina-Prover	A Lean 4 theorem-proving model from Project Numina and Moonshot AI, trained with reinforcement learning.
DeepSeek-Prover-V2	Open-weight Lean 4 provers (7B and 671B) that break a problem into subgoals and prove each one.

Projects and examples

Resource	What it is
Lean community projects	A list of ongoing formalization projects.
Formal Conjectures	Google DeepMind’s collection of formalized statements of open conjectures, a source of ambitious project ideas.
The Equational Theories Project	A large collaborative project led by Terence Tao that settled over 22 million implications between equational laws of magmas, all formalized in Lean.
The Stacks Project	The Stacks Project, formalized in Lean by AxiomMath.
Rubik’s cube in Lean	A proof that there are \(2^{12} \times 3^{8} \times 8! \times 11!\) Rubik’s cube positions, verified in Lean.