Best resources to learnFormal Proof Assistants (Lean)

Study sheet

Proof assistants check mathematics by computer. You will learn Lean and dependent type theory, formalising definitions and theorems, and how the mathlib community is building a verified library of mathematics.

5 resources · Reviewed Oct 2026 · How we curate

Level

Language

Type

Sort

🎓Courses(1)

course

Formalising Mathematics (Imperial College London course)

Imperial College London's undergraduate course on formalising mathematics in Lean 4 and Mathlib. It provides graded exercise sheets on logic, sets, functions, groups, limits, topology and more, with a tactics handbook, and runs locally or in-browser via Codespaces or Gitpod.

intermediate🇬🇧

📚Books(3)

book

Theorem Proving in Lean 4

Official Lean 4 text on the underlying logic. It covers dependent type theory, propositions as types, quantifiers, equality, inductive types, structures, type classes, tactics, well-founded recursion, and the axioms Lean adds, with how they affect computation. This is the primary source for the dependent type theory part of the topic. It complements Mathematics in Lean, which focuses on practice rather than foundations.

advanced🇬🇧

book

Mathematics in Lean

Free, continuously updated Lean 4 and Mathlib textbook with exercise files. Its 13 chapters run from logic, sets and functions through elementary number theory, structures, groups and rings, linear algebra, topology, differential calculus, and integration and measure theory.

intermediate🇬🇧

book

The Mechanics of Proof

Free online introduction-to-proofs textbook that pairs each argument with a Lean 4 formalisation. It covers computation, parity, divisibility, modular arithmetic, induction, functions, sets and relations, with a tactic index. Written for Fordham's Math 2001.

beginner🇬🇧

🌐Websites(1)

website

Natural Number Game (Lean 4)

Browser-based puzzle game in which you build the natural numbers from Peano's axioms and prove addition, multiplication and ordering facts in Lean 4, one tactic at a time. It needs no installation and is the usual first contact with Lean.

beginner🇬🇧

Share this topic

More in Mathematical Logic

See all 13 topics in Mathematical Logic →

Frequently Asked Questions

What are the best free resources to learn Formal Proof Assistants (Lean)?

Dantes has curated 5 resources for Formal Proof Assistants (Lean), including 3 books, 1 courses, 1 websites. All resources are hand-picked for quality — no algorithmic filler. Browse the full list above to find the format that works best for you.

Is Formal Proof Assistants (Lean) hard to learn?

Formal Proof Assistants (Lean) is approachable at the beginner level — there are resources here specifically for those starting from scratch. As you progress, intermediate and advanced material is also available to take your skills further.

What types of Formal Proof Assistants (Lean) learning resources are available on Dantes?

For Formal Proof Assistants (Lean), Dantes has curated 3 books, 1 courses, 1 websites. Each resource type serves a different learning style: videos and YouTube for visual learners, books for depth, courses for structured progression, and websites for quick reference.

How does Dantes select Formal Proof Assistants (Lean) resources?

Dantes is an algorithm-free learning directory. Resources are hand-curated based on quality, accuracy, and usefulness — not engagement metrics or paid placements. The goal is to surface the best learning material for Formal Proof Assistants (Lean), whether it's a free YouTube series, a classic textbook, or an open courseware from a top university.

Go deeper

Test your understanding of Formal Proof Assistants (Lean)

Explain it out loud. An AI tutor listens and asks questions that expose gaps you didn't know you had.