Package metadataLean library
Analysis
A Lean companion to Analysis I
Declarations not yet indexedLean 4.29.0-rc8
Pinned Reservoir package record · checked 2026-07-25
Lean package
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.
636 of 636 projects
Package metadataLean library
ryu
Converts floating point numbers to decimal strings
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
mil
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
Lean package
Package metadataProof corpus
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Declarations not yet indexedLean 4.29.0-rc8
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
glimpseOfLean
An introduction to theorem proving in Lean for the impatient.
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
aesop
White-box automation for Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
verso
Lean documentation authoring tool
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Game
Natural Number Game
Declarations not yet indexedLean 4.23.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
smt
Tactics for discharging Lean goals into SMT solvers.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
veil
A verifier for automated and interactive proofs about transition systems.
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
formalising-mathematics-2024
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
Lean package
Package metadataLean library
compfiles
Catalog Of Math Problems Formalized In Lean
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
REPL
A simple REPL for Lean 4, returning information about errors and sorries.
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
llmlean
LLMs + Lean, on your laptop or in the cloud
Declarations not yet indexedLean 4.23.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
auto
Experiments on automation for Lean
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package