Package metadataLean library
hax
Hax Lean library (automatically generated from cryspen/hax)
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
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
KrafftSieve
Formal Verification of the Krafft Geometry and the Additive Sieve Architecture
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
algebra
Algebra library for Lean 4
Declarations not yet indexedLean 4.29.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
logic
Logic Library for Lean 4
Declarations not yet indexedLean 4.29.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proofs
random proofs in lean 4
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanML
Formally verified machine learning in Lean 4.
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Calculemus2_es
Ejercicios de demostración con Lean4 e Isabelle/HOL.
Declarations not yet indexedLean 4.15.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lint-llm-proofs
Lean 4 linters for LLM-generated proof patterns
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
EllipticCurve
Towards a general definition of elliptic curve over schemes
Declarations not yet indexedLean 4.25.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
LeanBook
Notes on the Foundations of Lean
Declarations not yet indexedLean 4.19.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Declarations not yet indexedLean 4.15.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LPBackendSoplexFFI
LPBackend adapter for kim-em/soplex-ffi. Priority 10 (FFI band). The native backend kim-em/soplex defaults to.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
WadrayVerification
Verification of the Wadray library
Declarations not yet indexedLean 4.9.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Gossip
Verified Results about Gossip protocols in Lean 4
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
thue
Semi-Thue systems a.k.a. string rewriting systems
Declarations not yet indexedLean nightly-2023-07-12
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
archimedes
Don't disturb my circle!
Declarations not yet indexedLean 4.25.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
pphi2
Construction of phi^4_2 quantum field theory in Lean 4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
SeibergWitten
The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package