Beyond Mathlib
Browse 636 source-backed Lean ecosystem records from curated repositories and a pinned Reservoir snapshot. Exact Therefore declaration coverage is labelled separately from package and repository discovery.
Reservoir index b6ac225af74c backs 600 directory records. Provider metadata is discovery evidence, not proof verification or authorship.
34 of 636 projects
Clear searchA Lean companion with definitions, examples, theorem statements, and exercises from Category Theory in Context.
Declarations not yet indexedLean 4.24.0-rc1
Curated repository record · checked 2026-07-25
The user home repository for the Mathematics in Lean tutorial.
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
Declarations not yet indexedLean 4.5.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Tutorial on neural theorem proving
Declarations not yet indexedLean nightly-2023-06-10
Pinned Reservoir package record · checked 2026-07-25
Course notes for Formalising Mathematics 2026
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
数学系のためのLean勉強会
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Beginner's guide to Tactic Programming in Lean
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
A game introducing proofs, dependent type theory, and Lean prepared for a first year seminar course at Johns Hopkins in Fall 2025.
Declarations not yet indexedLean 4.23.0
Pinned Reservoir package record · checked 2026-07-25
Lean 4 tutorial files
Declarations not yet indexedLean 4.1.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Bonn Lean course for winter 24/25
Declarations not yet indexedLean 4.13.0-rc3
Pinned Reservoir package record · checked 2026-07-25
A game for learning Lean 4 where a cute little smart-elf joins you on your exploration of the Leaniverse.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Teaching Material for Course on Formalization Summer Semester 2025 at Uni Greifswald
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Formalisms Every Computer Scientist Should Know (course at ISTA)
Declarations not yet indexedLean 4.2.0-rc1
Pinned Reservoir package record · checked 2026-07-25
This is the repository for the course "Formalizing Analysis of Algorithms", Autumn 2025.
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Eric'sW26 Course on Lean
Declarations not yet indexedLean 4.28.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Code for the course "Proofs and Programs", January 2025, IISc
Declarations not yet indexedLean 4.19.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Aeneas tutorial for ICFP
Declarations not yet indexedLean 4.11.0-rc2
Pinned Reservoir package record · checked 2026-07-25