Package metadataProof corpus
EconCSLib
AI-assisted Lean formalization for Economics and Computation research
Declarations not yet indexedLean 4.30.0-rc2
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
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 tool
leansec
Total parser combinators library for Lean4
Declarations not yet indexedLean 4.20.0-rc5
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
pnP2023
Code and source for website for the course "Proofs and Programs", January 2023, Indian Institute of Science
Declarations not yet indexedLean 4.7.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 metadataProof corpus
bruhat-tits
A formalisation of the Bruhat-Tits tree in Lean4
Declarations not yet indexedLean 4.19.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
incompleteness
Formalize Incompleness Theorem Related Results
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
MathProbabilityRandom Matrix Theory
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