therefore
Sign up
Open navigation

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 search
Package metadataLean tool

lean-slides

A tool to auto-generate and render slides from Markdown comments in the Lean editor.

Declarations not yet indexedLean 4.29.0-rc6

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

interval

Conservative floating point interval arithmetic in Lean

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

MathFin

Formally verified mathematical finance in Lean 4. Black–Scholes/Greeks/PDE, Itô calculus, FTAP/Girsanov, CRR→BS convergence, Merton jump-diffusion.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

graphiti

Verified graph rewriting (for dataflow circuits).

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Clawristotle

OpenClaw-style theorem proving

Declarations not yet indexedLean 4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

cvc5

A Foreign Function Interface (FFI) to cvc5 solver in Lean.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

leaff

Leaff is a diff tool for Lean environments

Declarations not yet indexedLean 4.11.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

IMOSLLean4

Formalization of IMO shortlist problems in Lean 4

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

leanSpec

Program Specification in Lean 4

Declarations not yet indexedLean 4.5.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Dependent TypesFormal Specification
Package metadataLean library

ItaLean

Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025.

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

mdgen

Tool to generate markdown files from lean files.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

CliMarkdown
Package metadataProof corpus

lean4-analysis-tao

Formalization of "Analysis I" by Terence Tao

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

SDL

SDL2 bindings for lean

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4-mlir

Lean specification of neural architectures with verified IREE codegen.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Quantum

Lean formalization of the theory of quantum information and quantum computation

Declarations not yet indexedLean 4.29.0-rc6

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

json-schema

Lean 4 JSON Schema library - types, validation, correctness proofs, and deriving handlers

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanLJ

Lennard Jones in Lean

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

socket

sockets for Lean 4

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Lean package