Package metadataLean library
special-numbers
Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)
Declarations not yet indexedLean 4.15.0
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 metadataProof corpus
KummerCriterion
Proof of Kummer's criterion for regularity of a prime in Lean
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
swaps-perm
Mathematically defines of permutations of arrays and proves related theorems
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Distributed2Coloring
2-Coloring Cycles in One Round: Formalization in Lean 4
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lean-test
lean4 unit testing framework
Declarations not yet indexedLean 4.25.2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
bitmap
Lean 4 bitmap utilities with PNG encode/decode support, plus a small widget for visualization.
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
BitmapGraphicsImagePng
Package metadataLean library
ForestIPM
📦 R package - Bayesian hierarchical Integral Projection Model (IPM) for forest trees in eastern North America
Declarations not yet indexedLean 4.29.0-rc8
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
ChandraFurstLipton
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FormalRV
Formal resource verification of Shor's algorithm.
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ac-library
ac-library for lean4
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
mathmatic_in_elementary_number_th
IMO题目的形式化2个题
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
Logos_Library
Lean verified Science.
Declarations not yet indexedLean 4
Pinned Reservoir package record · checked 2026-07-25
Dirac EquationHeisenbergQuantum MechanicsRelativity
Package metadataLean library
loadTerms
Testing dynamic term loading in Lean 4.
Declarations not yet indexedLean stable
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
safeIdx
Type-safe indexing library.
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
Quave
Quantum Hoare Logic Lean 4 - A quantum program verification tool
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
HexLuthor
Lean 4 hex color syntax with inline VS Code color preview
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
lean-autograd
Automatic differentiation in Lean following JAX's autodidax tutorial
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanDidax2
Pedagogical autodiff library in Lean 4 with forward/reverse modes and vectorization
Declarations not yet indexedLean nightly-2025-03-09
Pinned Reservoir package record · checked 2026-07-25
Lean package