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.

134 of 636 projects

Clear search
Package metadataProof corpus

rMT4

The Riemann mapping theorem

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

ConvolutedProofs

Absurdly sophisticated proofs of simple mathematical facts in Lean 4

Declarations not yet indexedLean 4.22.0-rc4

Pinned Reservoir package record · checked 2026-07-25

FormalizationLean4MathProof
Package metadataProof corpus

SHSLib

Stochastic Hybrid Systems core definitions formalized in Lean

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

FormalizationMathStochastic Hybrid Systems
Package metadataProof corpus

FATE-H

The FATE-H (Formal Algebra Theorem Evaluation-Hard) benchmark.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

lean-glfw

C bindings and marshalling to use GLFW and OpenGL from the lean4 theorem prover

Declarations not yet indexedLean nightly-2022-02-21

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

MasterDiss

Proving the main theorem of polytopes using Lean 4

Declarations not yet indexedLean 4.7.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
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 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 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 metadataProof corpus

KummerCriterion

Proof of Kummer's criterion for regularity of a prime in Lean

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Distributed2Coloring

2-Coloring Cycles in One Round: Formalization in Lean 4

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

ChandraFurstLipton

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

sard

Work towards a general version of Sard's theorem in Lean 4

Declarations not yet indexedLean 4.12.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

FATE-M

The FATE-M (Formal Algebra Theorem Evaluation - Medium) benchmark.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

galeShapley

Formalization in Lean of some results related to stable matchings and the Gale-Shapley algorithm

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

SmullyanKnightsAndKnaves

Formalization and solution of knights and knaves puzzles in lean 4

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

CSE290Q

CSE 290Q: Topics in Interactive Theorem Provers

Declarations not yet indexedLean 4.18.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math