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

Quantum

Lean formalization of the theory of quantum information and quantum computation

Declarations not yet indexedLean 4.29.0-rc6

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

OSforGFF

A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

AgreeToDisagree

Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

TNLean

Lean 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

polya-enumeration-theorem

A Lean 4 formalization of Pólya enumeration theorem.

Declarations not yet indexedLean 4.14.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

FoML

Lean Formalization of Generalization Error Bound by Rademacher Complexity

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Erdos870

Erdős Problem #870: paper and sorry-free, axiom-clean Lean 4 formalization.

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Prismriver

(Mirror) A Music formalization library and DSL in Lean 4

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

traat

Lean formalization of selected lemmas from "Term Rewriting and All That"

Declarations not yet indexedLean 4.30.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

rupert

Formalization of the Rupert Problem for convex polyhedra.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

mA4N1

MA4N1 Theorem Proving with Lean

Declarations not yet indexedLean 4.24.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

IMO

Suggested conventions and examples for Lean formalization of IMO problem statements

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

shannon-entropy

A formalization of Shannon's seminal 1948 paper defining entropy.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

real-closed-field

Formalisation of the theory of real closed fields in Lean 4.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

AlgebraMath
Package metadataProof corpus

AM

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

clt

Central limit theorem in Lean

Declarations not yet indexedLean 4.29.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

partial-combinatory-algebras

A Lean 4 formalization of partial combinatory algebras.

Declarations not yet indexedLean 4.15.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

arithmetization

Formalization of Arithmetization of Mathematics/Metamathematics

Declarations not yet indexedLean 4.17.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package