Package metadataLean library
FormalBook
Formalizing "Proofs from THE BOOK"
Declarations not yet indexedLean 4.27.0-rc1
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
alloy
Write C shims from within Lean code.
Declarations not yet indexedLean 4.21.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
Parser
Parser Combinator Library for Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ix
a zero-knowledge proof-carrying code platform for Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
GroundZero
Ground Zero: Lean 4 HoTT Library
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LSpec
A Testing Framework for Lean
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
risc0-lean4
A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover
Declarations not yet indexedLean nightly-2022-12-23
Pinned Reservoir package record · checked 2026-07-25
Risc0Zero KnowledgeZk StarkZkvm
Package metadataLean library
expdb
Exponent pair database
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
soma-workspace
⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
verina
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
maze
maze game encoded in Lean 4 syntax
Declarations not yet indexedLean 4.22.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LemmaScript
verification toolchain for TypeScript (Tech Preview)
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
Game
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 package
Package metadataLean tool
leanInk
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Declarations not yet indexedLean 4.6.0-rc1
Pinned Reservoir package record · checked 2026-07-25
AlectryonInteractive Theorem ProvingVisualization
Package metadataLean library
Game
RealAnalysisGame
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Velvet
An auto-active verifier embedded into Lean
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FormalSnarksProject
A formal verification of Linear PCP SNARKs.
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Math