Package metadataLean library
Game
Natural Number Game
Declarations not yet indexedLean 4.23.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.
433 of 636 projects
Clear searchPackage 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 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 library
Clean
Lean circuit DSL
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
doc-gen4
Document Generator for Lean 4
Declarations not yet indexedLean 4.32.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Loom
Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
yatima
A zero-knowledge Lean4 compiler and kernel
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
render
A simple raytracer written in Lean 4
Declarations not yet indexedLean 4.8.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Raytracing
Package metadataLean library
verbose
Natural language tactics to teach mathematics using Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lib
LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.
Declarations not yet indexedLean 4.19.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Exact source indexedLean library
quantumInfo
Quantum information theory in Lean 4
115 indexed declarationsLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
braketbundledcapacitydistribution
Package metadataLean library
verso-manual
The Lean reference manual
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ZeroToQED
From Zero to QED: An informal introduction to formality with Lean 4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Exact source indexedLean library
debate
Formalizing stochastic doubly-efficient debate
52 indexed declarationsLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
arithbasicbasicschernoff