Package metadataLean library
AddCombi
The sublibrary of Mathlib dedicated to additive combinatorics
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Additive CombinatoricsMath
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
Cookbook
A cookbook for Metaprogramming in Lean4 containing code snippets to help you code!
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-linq
Type-safe, deeply-embedded SQL query DSL for Lean 4 - LINQ-style pipelines and query! comprehensions compiling to parameterized SQL for SQLite, PostgreSQL, and SQL Server
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
DatabaseDslLinqSql
Package metadataLean library
DateTime
DateTime package for Lean 4
Declarations not yet indexedLean 4.5.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
leanses
Lean lens implementation with custom notation.
Declarations not yet indexedLean nightly-2025-06-05
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proof_zk_recovery_ci
ZK recovery contract: design, audits, and prototyping (private)
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
UnicodeBasic
Basic Unicode support for Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Unicode
Package metadataLean library
lean-yjs
Lean-Yjs: Formal Verification of Yjs Integration Algorithm
Declarations not yet indexedLean 4.26.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
quantumlib
A Quantum Computing Library in LEAN
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
monoid.space
Learn pure math with agda :rocket:
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Abstract AlgebraAgdaCategory TheoryType Theory
Package metadataProof corpus
IMO
Suggested conventions and examples for Lean formalization of IMO problem statements
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean99
These are Lean translations of Ninety-Nine Haskell Problems (WIP)
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
pdl
Tableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
fecssk
Formalisms Every Computer Scientist Should Know (course at ISTA)
Declarations not yet indexedLean 4.2.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
plonky3-example
A framework for extracting and formally verifying constraint systems from the Plonky3 zkDSL in Lean.
Declarations not yet indexedLean 4.23.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
shannon-entropy
A formalization of Shannon's seminal 1948 paper defining entropy.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
FAA2025
This is the repository for the course "Formalizing Analysis of Algorithms", Autumn 2025.
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
partax
Lean 4 library of tools for parsing and compiling syntax and parser definitions.
Declarations not yet indexedLean 4.3.0
Pinned Reservoir package record · checked 2026-07-25
Lean package