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

curljson

curljson: a small Lean4 library to fetch JSON with libCurl

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ec-tate-lean

Elliptic curve algorithm verification project built on mathib4

Declarations not yet indexedLean nightly-2023-08-19

Pinned Reservoir package record · checked 2026-07-25

Lean package
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 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 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 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
Package metadataLean library

special-numbers

Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

swaps-perm

Mathematically defines of permutations of arrays and proves related theorems

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package