Package metadataTeaching project
Formal2024
Course repository for GlaMS - Formalising Mathematics in Lean (2024)
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Formalisation Mathematics
Beyond Mathlib
The Lean research ecosystem, in one directory.
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 searchPackage metadataTeaching project
Calculemus2
Proof exercises in Lean4 and Isabelle/HOL
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
pnP2023
Code and source for website for the course "Proofs and Programs", January 2023, Indian Institute of Science
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
mk-exercise
Simple and intuitive tool to manage exercises in textbooks written in Lean.
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
formalising-mathematics
Course on theorem proving with Lean
Declarations not yet indexedLean 4.16.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
regensburg-itp-school-2023
Materials for my lecture at the 2023 International School on Interactions of Proof Assistants and Mathematics in Regensburg
Declarations not yet indexedLean 4.0.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
HausdorffSchoolLean
Repository for the September 2023 Hausdorff School on Lean
Declarations not yet indexedLean 4.0.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
ITP_course
An Interactive Theorem Proving course with Lean 4
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataTeaching project
LogicColloquiumTutorial
The Lean tutorial for Logic Colloquium 2023
Declarations not yet indexedLean nightly-2023-06-20
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
workshop
Repo for the first BerLean workshop.
Declarations not yet indexedLean 4.12.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
msri2023_graphs
Repository for graph theory & combinatorics group at the MSRI Lean summer school
Declarations not yet indexedLean nightly-2023-06-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
LeanLion
Code for Singapore Workshop on Formal Proofs and Lean
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
Monad
Notes for the category theory class I'm teaching at MIT (Jan 2026)
Declarations not yet indexedLean 4.29.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataTeaching project
lean-autograd
Automatic differentiation in Lean following JAX's autodidax tutorial
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
LAGinLean
Questions related to Imperial College's Linear Algebra and Groups course running in November and December 2024.
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
ExtremeValueProject
A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package