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
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
LeanTeX_Mathlib
LeanTeX pretty printers for mathlib
Declarations not yet indexedLean 4.18.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package 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 metadataProof corpus
phi-confluence
Proof of 𝜑-calculus confluence in Lean4
Declarations not yet indexedLean 4.30.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 metadataTeaching project
mk-exercise
Simple and intuitive tool to manage exercises in textbooks written in Lean.
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
HadwigerNelson
Hadwiger-Nelson Problem Formalization in Lean 4
Declarations not yet indexedLean nightly-2024-07-11
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
Exact source indexedProof corpus
PDE
PDE Lean formalization
41 indexed declarationsLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
analysisheat kernelheat solutionheat solution property
Package metadataProof corpus
kolmogorov_complexity
Formalization of Algorithmic Information Theory in Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Math
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 metadataTeaching project
formalising-mathematics
Course on theorem proving with Lean
Declarations not yet indexedLean 4.16.0
Pinned Reservoir package record · checked 2026-07-25
Lean package