Package metadataLean library
saturn
Experiments with SAT solvers with proofs in Lean 4
Declarations not yet indexedLean 4.8.0
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.
600 of 636 projects
Clear searchPackage metadataLean library
LeanArchitect
LeanArchitect extracts a blueprint directly from Lean source.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
tutorials4
Lean 4 tutorial files
Declarations not yet indexedLean 4.1.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
thales
TypeScript compiler and JavaScript engine in Lean
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanSAT
This package provides an interface and foundation for verified SAT reasoning
Declarations not yet indexedLean nightly-2024-08-02
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
problems
Formalization of the Millennium Problems in Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Http
🌐 | HTTP primitives for Lean 4
Declarations not yet indexedLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
RL-Theory
Towards Formalizing RL Theory
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
mathlib4-all-tactics
Markdown file of the list and explanations of all mathlib4 tactics
Declarations not yet indexedLean 4.0.0-rc4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
computableReal
computable implementation of real numbers in Lean4
Declarations not yet indexedLean 4.17.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
qpf
A WIP definitional (co)datatype package for Lean4
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Blaster
SMT-based reasoning core for Lean4
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-crypto
Cryptographic routines for the Lean 4 language
Declarations not yet indexedLean nightly-2023-04-20
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
KLR
A formalization of ML kernel languages
Declarations not yet indexedLean 4.23.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proven-zk
A support library for working with zero knowledge cryptography in Lean 4.
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
leansqlite
SQLite bindings for Lean
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
DatabaseFfiSqlite
Package metadataLean library
Wasm.lean
A WebAssembly implementation in Lean4
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
WasmWebassembly
Package metadataProof corpus
FelConjecture
Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Math