Package metadataLean library
hex
Verified computational algebra in Lean 4: aggregator for the released hex libraries
Declarations not yet indexedLean 4.32.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.
433 of 636 projects
Clear searchPackage metadataLean library
TenCert
Verified tensor compilation in Lean
Declarations not yet indexedLean 4.19.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
chomsky
Port https://github.com/madvorak/grammars/ to Lean 4
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
EulerProducts
An attempt at formalizing facts on Euler products in Lean
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
tabular-types
Proofs for Extensible Data Types with Ad-Hoc Polymorphism
Declarations not yet indexedLean 4.17.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
flow
Reactive streams library for Lean 4 - Flow, SharedFlow, StateFlow, ProgramFlow, and ReactiveProgram
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
hale
Haskell-inspired libraries for Lean 4 with maximalist typing
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
HaskellHttpWarpWeb Server
Package metadataLean library
Ipld.lean
a Lean4 implementation of the IPLD format
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Poseidon.lean
A Lean 4 implementation of the Poseidon zkSNARK-friendly hash function
Declarations not yet indexedLean nightly-2023-01-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ZKSnark.lean
Declarations not yet indexedLean nightly-2022-06-14
Pinned Reservoir package record · checked 2026-07-25
Zk SnarksZkp
Package metadataLean library
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Declarations not yet indexedLean 4.13.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
json-schema
Json Schema lean implementation
Declarations not yet indexedLean 4.25.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanBridge
Link LMFDB and Lean
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
render
Verified renders of the Mandelbrot set
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
MillerRabin
Miller–Rabin primality test in Lean
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Game
Knights and Knaves Educational Game in Lean 4
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
RustFFI
An RDF Library for Lean4
Declarations not yet indexedLean 4.6.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
flean
Floating point numbers in lean. A replacement of Mathlib.Data.FP
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math