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.

600 of 636 projects

Clear search
Package metadataProof corpus

IsTranscendentalPi

Formalization in Lean of the transcendence of π.

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

tCSlib

Lean 4 Theoretical Computer Science Library

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

LeanLion

Code for Singapore Workshop on Formal Proofs and Lean

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanUtils

Lean scripts for indexing sorries and verifying proofs

Declarations not yet indexedLean 4.17.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

numbers

Arbitrary Bit-Length Integers in Lean

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

morpho-verity

Formal verification of Morpho Blue lending protocol using Verity (Lean 4)

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mrdi

An interface between Lean4 and Oscar.

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

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

ennreal-arith

Arithmetic tactics for extended non-negative real numbers (ENNReal)

Declarations not yet indexedLean 4.22.0-rc3

Pinned Reservoir package record · checked 2026-07-25

ArithmeticENNRealProbabilityTactics
Package metadataLean library

MiscYD

Miscellaneous projects I am working on in Lean

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Additive CombinatoricsCombinatoricsConvex GeometryMath
Package metadataLean library

LogicQ

An IR language for fault-tolerant quantum programming

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

m2r-group-7

Classifying Groups of Order up to 31 in Lean 4 - Imperial Maths Year 2 Research Project Group 7 - 2026

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

advents

Advent of Code

Declarations not yet indexedLean 4.26.0-rc2

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

huffman

Huffman coding in Lean 4 with a formal optimality proof and Unix pack/unpack (.z) compatibility.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

CompressionFormal VerificationHuffmanPack
Package metadataLean library

delphin

The Lean port of PyDelphin, a library to integrate DELPH-IN toolsets

Declarations not yet indexedLean 4.12.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

VerificationDemo

A temporary repository

Declarations not yet indexedLean 4.13.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

interest

Interest: a Lean library for financial mathematics

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package