Package metadataLean library
PrimeCert
Formal prime certificates in Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
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
sqlite
Sqlite3 bindings for lean4
Declarations not yet indexedLean 4.25.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
BibtexQuery
A simple command-line bibtex query utility written in Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
beam
Claude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ArtificialAlgorithms
Verified algorithms in Lean, implemented and proved by AIs
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
M1F-explained
A computer formalisation of parts of Martin Liebeck's book "a concise introduction to pure mathematics"
Declarations not yet indexedLean nightly-2023-08-05
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lithe
simple web service in lean4
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
VD
Formalizing Value Distribution Theory
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
circuitlib
A digital circuit verification library for Lean4
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
CircuitsElectricalHardware
Package metadataProof corpus
Uniq
Static Uniqueness Analysis for the Lean 4 Theorem Prover
Declarations not yet indexedLean nightly-2023-01-14
Pinned Reservoir package record · checked 2026-07-25
Linear TypesUniqueness Types
Package metadataLean library
FVIntmax
Formal verification of the Intmax protocol in Lean.
Declarations not yet indexedLean 4.14.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
TopSingleLayer
Formal Verification of Top Single Layer Encoding
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lFTCM2024
Repository for the conference LFTCM2024
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Lean Book
mdbook template for Lean project
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
MonomialOrderedPolynomial
Monomial ordered polynomial implementation in Lean4
Declarations not yet indexedLean 4.29.0-rc8
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
quasi-borel-spaces
A formalization of Quasi-Borel Spaces in Lean 4
Declarations not yet indexedLean 4.28.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lean-inf
Levi-Civita field implementation in Lean 4 for computing with infinities and infinitesimals.
Declarations not yet indexedLean 4.12.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proetale
Proétale cohomology in Lean
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Math