Package metadataTeaching project
ntptutorial
Tutorial on neural theorem proving
Declarations not yet indexedLean nightly-2023-06-10
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
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 metadataProof corpus
llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
Declarations not yet indexedLean 4.1.0
Pinned Reservoir package record · checked 2026-07-25
LlmTheorem Proving
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 tool
loogle
Mathlib search tool
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
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 tool
Canonical
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
matrix_cookbook
The matrix cookbook, proved in the Lean theorem prover
Declarations not yet indexedLean 4.22.0-rc4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
jixia
A static analysis tool for Lean 4.
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
FormalisingMathematics2026
Course notes for Formalising Mathematics 2026
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
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