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

Project

Structure in Prime Gaps - Formalized

Declarations not yet indexedLean 4.21.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

taleve

Formal model of stacker games in Lean

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Notes

Notes in PhysLean

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

versowebcomponents

A collection of reusable components from the Lean website designed build related sites with the same look and feel.

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

STIR

SC: Ethereum - zk(E)VM Verification - STIR Lean Blueprint

Declarations not yet indexedLean 4.19.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

BirkhoffErgodicThm

A proof of Pointwise Birkhoff Ergodic Theorem in Lean

Declarations not yet indexedLean 4.20.0-rc5

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

SumSq

Summing squares in Lean

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Real AlgebraType Theory
Package metadataLean library

Apportionmentlib

Formal verification of apportionment theory.

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

MathSocial Choice Theory
Package metadataLean library

metamath_prover

Demostrador de enunciados matemáticos con base Lean

Declarations not yet indexedLean 4.29.0-rc4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

CommComp

Formalization of communication complexity in Lean

Declarations not yet indexedLean 4.12.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

MarkovSemigroups

Markov semigroups, functional inequalities, and convergence to equilibrium in Lean 4

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

climber

LCF checks theorem construction; climber checks theory construction

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

reviser

LCF checks theorem construction; reviser checks belief revision

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

demazure

Demazure products and ASP permutations

Declarations not yet indexedLean 4.31.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

lean-rsa-project

A lean project on RSA encryption

Declarations not yet indexedLean nightly-2023-04-11

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanBisection

The Bisection method is the simplest numerical approximation approach in mathematics that applies to any continuous function on an interval where the value of the function changes sign from one-end-point of the interval to another

Declarations not yet indexedLean 4.30.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Hyper

Hyperreal Numbers in Lean 4

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Physicslib

Solving Hilbert's sixth problem in Lean

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package