Package metadataLean library
Http.lean
Basic Http functionality in Lean (unfinished)
Declarations not yet indexedLean nightly-2022-09-11
Pinned Reservoir package record · checked 2026-07-25
Http
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 metadataProof corpus
AharoniKorman
Disproof of the Aharoni–Korman conjecture
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
violet
A programming language, half theorem prover
Declarations not yet indexedLean 4.2.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
bonnAnalysis
repository for the collaborative formalization seminar in Analysis in Bonn
Declarations not yet indexedLean 4.10.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ray-series
Power series arithmetic in Lean
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
DeBruijnSSA
A formalization of SSA in Lean 4
Declarations not yet indexedLean 4.15.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
pteffects
Effect monads with specifications (DIjkstra Monads) in Lean 4
Declarations not yet indexedLean 4.3.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Hex
Verified computational algebra in Lean 4 - polynomial factoring, LLL, and friends
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
LeanW26
Eric'sW26 Course on Lean
Declarations not yet indexedLean 4.28.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
duality
Duality theory in linear optimization and its extensions
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
many-sorted-model-theory
A lean repository for building many-sorted logic, with a view towards model theory of valued fields
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataTeaching project
PfsProgs25
Code for the course "Proofs and Programs", January 2025, IISc
Declarations not yet indexedLean 4.19.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
leansi
Leansi is a Lean Library for terminal formatting.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
PCF
A formalization of PCF theory in lean
Declarations not yet indexedLean 4.18.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
kimina
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
tutorial
Aeneas tutorial for ICFP
Declarations not yet indexedLean 4.11.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-subst
Lean4 library for substitution inspired by autosubst
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
viper
A Python environment manager built in Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package