Package metadataLean library
LeanTeX_Mathlib
LeanTeX pretty printers for mathlib
Declarations not yet indexedLean 4.18.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.
433 of 636 projects
Clear searchPackage metadataLean library
protobuf
protobuf implementation for Lean 4
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-semver
Semantic Versioning in Lean4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
PolyFun
Lean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean2sexp
Convert Lean .olean files to s-expressions
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
juvix-lean
Juvix Lean library for compiler run verification
Declarations not yet indexedLean 4.19.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
Blake3
Lean4 bindings to Blake3
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Leanduction
Generate good induction principles on nested inductive types
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
tamago
Common EVM smart contracts similar to solady/solmate, formally verified using Tama + Verity
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
filter-game
Lean 4 version of the filter game.
Declarations not yet indexedLean 4.28.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
FormalizeWithTest
Autoformalization of coding problems, verified with test cases
Declarations not yet indexedLean 4.13.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
QuantumLogicalFramework
quantum genesis constructive possibilist quantum logical synthesis
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
SuperTensor
Verified tensor graph optimization in Lean 4: constructive soundness proofs + equality saturation + verified extraction via e-graph↔circuit bijection + multi-target code generation.
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
redisLean
Lean bindings for redis/hiredis
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean_snakebird
An implementation of Snakebird in Lean.
Declarations not yet indexedLean 4.8.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
BET
Project for "Machine-Checked Mathematics" at the Lorentz Center
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
detective
A Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanSerde
Type-safe serialization for Lean
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Lean package