Package metadataProof corpus
leanFibredCategories
A Lean4 Formalization of Fibred Categories
Declarations not yet indexedLean 4.4.0-rc1
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.
636 of 636 projects
Package metadataLean library
quicksort
Implementation and Formal Verification of the Quicksort Algorithm
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
GinacLean
A work-in-progress Lean 4 binding to GiNaC
Declarations not yet indexedLean 4.8.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
MeanFourier
Formalisation of mean Fourier analysis in Lean 4
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Harmonic AnalysisMath
Package metadataLean library
lean4-ctypes
FFI for Lean 4
Declarations not yet indexedLean nightly-2023-11-21
Pinned Reservoir package record · checked 2026-07-25
Ffi
Package metadataLean library
AsciiPlot
ASCII/Unicode plotting library for Lean 4 with legends and braille rendering
Declarations not yet indexedLean nightly-2025-01-31
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
selbergSieve
A formalisation of the Selberg sieve in Lean 4
Declarations not yet indexedLean 4.7.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
chromatic_polynomial
Chromatic polynomial in Lean4
Declarations not yet indexedLean 4.11.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
OpenSSL.lean
OpenSSL bindings for Lean
Declarations not yet indexedLean nightly-2022-09-11
Pinned Reservoir package record · checked 2026-07-25
OpensslOpenssl Bindings
Package metadataLean library
LeanSha256
Pure-Lean SHA-256 reference implementation: NIST CAVP-validated, kernel-reducible, no FFI.
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
CryptographyFips 180 4Lean4Sha256
Package metadataLean library
extra
Supplements to the Lean 4 Standard Library
Declarations not yet indexedLean 4.29.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
LogicColloquiumTutorial
The Lean tutorial for Logic Colloquium 2023
Declarations not yet indexedLean nightly-2023-06-20
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Seminar
Past contents of Lean Seminars in Bonn
Declarations not yet indexedLean 4.13.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
workshop
Repo for the first BerLean workshop.
Declarations not yet indexedLean 4.12.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
mini-redis
An implementation of mini-redis in Lean 4
Declarations not yet indexedLean pr-release-8003
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
flare
Official implementation of "FLARE: Verifying MILP Reformulations with LLM-Based Formal Proof Synthesis"
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
webeditor
Helper tool for projects run in lean4web
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
test
SF.lean勉強会でigrepが書いたコードの記録
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package