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.

636 of 636 projects

Package metadataLean library

printiest

A pretty printer for Lean 4

Declarations not yet indexedLean 4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Lurk.lean

A Lean 4 implementation of the Lurk Language for recursive zkSNARKS

Declarations not yet indexedLean nightly-2023-01-10

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

exchangeability

Formalization of exchangeability and three proofs of de Finetti's theorem in Lean 4, following Probabilistic Symmetries and Invariance Principles by Olav Kallenberg

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Lean2Dk

WIP translation from Lean to Dedukti

Declarations not yet indexedLean 4.22.0-rc4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

Formal2024

Course repository for GlaMS - Formalising Mathematics in Lean (2024)

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Formalisation Mathematics
Package metadataProof corpus

lean-groebner

Lean4 formalization of Gröbner basis (WIP)

Declarations not yet indexedLean nightly-2023-06-10

Pinned Reservoir package record · checked 2026-07-25

Groebner Basis
Package metadataLean library

CardanoLedgerApi

Cardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

qdt

Query-based Dependent Type Elaborator

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

Calculemus2

Proof exercises in Lean4 and Isabelle/HOL

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Http

Basic HTTP definitions and parsing for Lean

Declarations not yet indexedLean 4.5.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

ttfpi

"Type Theory and Formal Proof: An Introduction" book formalization in Lean

Declarations not yet indexedLean 4.13.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

optisat

Formally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

E GraphEquality SaturationVerification
Package metadataLean library

hex

Verified computational algebra in Lean 4: aggregator for the released hex libraries

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

TenCert

Verified tensor compilation in Lean

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Lie

A classification theorem in Lean of solvable Lie algebras of dimension zero to three

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

EulerProducts

An attempt at formalizing facts on Euler products in Lean

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

tabular-types

Proofs for Extensible Data Types with Ad-Hoc Polymorphism

Declarations not yet indexedLean 4.17.0

Pinned Reservoir package record · checked 2026-07-25

Lean package