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.

433 of 636 projects

Clear search
Package metadataLean library

llm

Interfacing with Large Language Models (remote and local) from Lean.

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Hesper

Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accelerated matrix ops, and cross-platform support (Metal/Vulkan/D3D12). Build provably correct GPU compute and ML inference engines.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-eval

Comparator-based Lean formal mathematics eval

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

readLean

How to read Lean

Declarations not yet indexedLean 4.12.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanCat

Lean4 benchmark on 1 category.

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Vericoding

tools and benchmarks for verified coding

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

raylean

Lean4 bindings for raylib

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mathlib4-help

List of the output of #help command of mathlib4, including list of all tactics, commands...etc

Declarations not yet indexedLean 4.33.0-rc1

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 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 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 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 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