Package metadataLean library
LeanPlot
Interactive React-powered charting library for Lean 4 in VS Code's infoview
Declarations not yet indexedLean 4.32.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
LatticeTriangle
Lean formalizations for the paper "On the paucity of lattice triangles"
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
stlc
Simply Typed Lambda Calculus with de Bruijn indices
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Prismriver
(Mirror) A Music formalization library and DSL in Lean 4
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
Formalization_SoSe25
Teaching Material for Course on Formalization Summer Semester 2025 at Uni Greifswald
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Zklib
deprecated, use Verified-zkEVM repository instead
Declarations not yet indexedLean 4.15.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-loris
Experiments with some ways of automating reasoning in lean 4
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
MetaExamples
Examples using MetaProgramming for writing tactics etc.
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Game
Make/Encode some basic logic puzzles
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
traat
Lean formalization of selected lemmas from "Term Rewriting and All That"
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
rupert
Formalization of the Rupert Problem for convex polyhedra.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
regexderiv
Proofs written in Lean4 for the core katydid validation algorithm
Declarations not yet indexedLean 4.22.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
mA4N1
MA4N1 Theorem Proving with Lean
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
RustFFI.lean
Template for Lean<->Rust FFI
Declarations not yet indexedLean nightly-2022-12-08
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
FloatSpec
Formally Verified Float Implementation with lean4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ast_export
AST export from Lean 4
Declarations not yet indexedLean 4.10.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
ELFSage
A toy ELF parser/validator
Declarations not yet indexedLean nightly-2024-10-07
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Noperthedron
The Noperthedron does not have Rupert Property: a proof in Lean4
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package