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

proven-zk

A support library for working with zero knowledge cryptography in Lean 4.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

leansqlite

SQLite bindings for Lean

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

DatabaseFfiSqlite
Package metadataLean library

Wasm.lean

A WebAssembly implementation in Lean4

Declarations not yet indexedLean nightly-2023-01-10

Pinned Reservoir package record · checked 2026-07-25

WasmWebassembly
Package metadataLean library

SafeVerify

A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

CompPoly

Computable Polynomials in Lean.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanCert

Verified interval arithmetic for Lean 4 - prove bounds on exp, sin, cos, find roots, all machine-checked

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

TensorLib

A verified tensor library in Lean

Declarations not yet indexedLean 4.23.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lib

Solving Competition Geometry Problems in Lean

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

formal-slt

Zero-sorry Lean 4 library of finite-sample statistical learning theory: PAC-Bayes (incl. a five-component test-time meta-bound), VC, Rademacher, sharp McDiarmid, and Dudley chaining. ICML 2026 AI4MATH

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

algorithm

Verified efficient algorithms in Lean4.

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

KittyCats

Category theory but for kitty cats, meow 🐱🐈

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

htpi

Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It"

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

trzk

Verified Optimizing Compiler for Cryptographic Primitives

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanTeX

Lean 4 library for pretty printing expressions as LaTeX

Declarations not yet indexedLean 4.18.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

evmSmith

A framework for AI systems to write EVM bytecode and prove it safe, built on NethermindEth/EVMYulLean.

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Megaparsec.lean

Lean 4 port of Megaparsec

Declarations not yet indexedLean 4.0.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4export

Plain-text declaration export for Lean 4

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Chess

Chess in Lean 4

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Lean package