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

Iwasawalib

Formalization of Iwasawa Theory in LꓱꓯN (tentative)

Declarations not yet indexedLean 4.30.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

logic-formalization

Formalize "Logic Notes" by Lou van den Dries in Lean

Declarations not yet indexedLean 4.20.0-rc5

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

AharoniKorman

Disproof of the Aharoni–Korman conjecture

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

violet

A programming language, half theorem prover

Declarations not yet indexedLean 4.2.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

bonnAnalysis

repository for the collaborative formalization seminar in Analysis in Bonn

Declarations not yet indexedLean 4.10.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

DeBruijnSSA

A formalization of SSA in Lean 4

Declarations not yet indexedLean 4.15.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

PCF

A formalization of PCF theory in lean

Declarations not yet indexedLean 4.18.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

M1F-explained

A computer formalisation of parts of Martin Liebeck's book "a concise introduction to pure mathematics"

Declarations not yet indexedLean nightly-2023-08-05

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Uniq

Static Uniqueness Analysis for the Lean 4 Theorem Prover

Declarations not yet indexedLean nightly-2023-01-14

Pinned Reservoir package record · checked 2026-07-25

Linear TypesUniqueness Types
Package metadataProof corpus

quasi-borel-spaces

A formalization of Quasi-Borel Spaces in Lean 4

Declarations not yet indexedLean 4.28.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

cryptography

Lean 4 programming language and theorem prover cryptography experiments

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

FormaleSystemeInLean

LEAN4 formalization of the undergraduate lecture "Formale Systeme" at TU Dresden (WIP)

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

NeuralNetworks

Formalization of Neural Networks in Lean 4

Declarations not yet indexedLean 4.24.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

provenance

Lean4 formalization of some provenance notions

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

kolmogorov_extension4

Lean formalization of the Kolmogorov extension theorem

Declarations not yet indexedLean 4.31.0

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 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 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