Package metadataLean library
leanaide
Tools based on AI for helping with Lean 4
Declarations not yet indexedLean 4.28.0
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
plfl
Learn Lean 4 with PLFA proofs.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Putnam2025
Our solutions to Putnam 2025.
Declarations not yet indexedLean 4.21.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Intuitive, type-safe expression quotations for Lean 4.
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
CombinatorialGames
Combinatorial game library in Lean 4
Declarations not yet indexedLean 4.31.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
junk-theorems
A small collection of formally verified junk theorems provable in Lean4 + Mathlib.
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lnsym
Armv8 Native Code Symbolic Simulator in Lean
Declarations not yet indexedLean nightly-2024-10-07
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sampcert
SampCert : Verified Differential Privacy
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sparkle
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
evmyul
Executable formal model of the EVM and Yul in Lean 4.
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanTool
A "code intepreter" for Lean
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FormalBook
Formalizing "Proofs from THE BOOK"
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
alloy
Write C shims from within Lean code.
Declarations not yet indexedLean 4.21.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ix
a zero-knowledge proof-carrying code platform for Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
GroundZero
Ground Zero: Lean 4 HoTT Library
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LSpec
A Testing Framework for Lean
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
expdb
Exponent pair database
Declarations not yet indexedLean 4.27.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
pantograph
(Mirror) A Machine-to-Machine Interaction System for Lean 4
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package