Package metadataLean library
QuantumLogicalFramework
quantum genesis constructive possibilist quantum logical synthesis
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.
600 of 636 projects
Clear searchPackage metadataTeaching project
regensburg-itp-school-2023
Materials for my lecture at the 2023 International School on Interactions of Proof Assistants and Mathematics in Regensburg
Declarations not yet indexedLean 4.0.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
SuperTensor
Verified tensor graph optimization in Lean 4: constructive soundness proofs + equality saturation + verified extraction via e-graph↔circuit bijection + multi-target code generation.
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
redisLean
Lean bindings for redis/hiredis
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean_snakebird
An implementation of Snakebird in Lean.
Declarations not yet indexedLean 4.8.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
BET
Project for "Machine-Checked Mathematics" at the Lorentz Center
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
detective
A Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam
Declarations not yet indexedLean 4.29.1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanSerde
Type-safe serialization for Lean
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
PersistentDecomp
Formalizing the Structure Theorem for Persistence Modules
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
CatDG
Aspects of categorical differential geometry, formalised in lean 4.
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
miniF2F-lean4
miniF2F dataset ported into Lean 4
Declarations not yet indexedLean 4.6.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
RelationalAlgebra
University Master Thesis
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
lean-gccjit
libgccjit bindings for Lean4
Declarations not yet indexedLean 4.1.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
lapis
✏️ | A cutting-edge, concurrent & performant Language Server Protocol (LSP) framework for Lean 4.
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
riddle-proofs
Riddles solved in Lean4 for educational purposes
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
controlflow
A control flow graph library for Lean
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
automated_Theory_Construction
A prototype framework for automated theory construction in Lean 4.
Declarations not yet indexedLean 4.29.0-rc6
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
cryptolib
The cryptography library of Lean 4
Declarations not yet indexedLean 4.19.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math