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

vqc_in_lean

(WIP) Lean 4 port of the Verified Quantum Computing. Developed as a personal learning project to deepen understanding of quantum computing concepts and formal verification.

Declarations not yet indexedLean 4.15.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

CliffordProject

Lean formalization of the structure theorem for the single-qudit Clifford group

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Weights

Formalization in Lean4 of some results in "Minimization of hypersurfaces" by A.-S. Elsenhans and myself

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

lie-classification

Classification of Lie algebras in Lean

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

flappy

A flappy bird clone in Lean

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Kaplansky4

Proof of Kaplanski criterion for being a UFD in Lean4

Declarations not yet indexedLean 4.26.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

ITP_course

An Interactive Theorem Proving course with Lean 4

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

complexitylib

Formalization of complexity theory

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

sensitivity

Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

DGAlgorithms

Distributed Graph Algorithms in Lean

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

GraphLib

This is the repository for graph algorithm design.

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

SardMoreira

Formalization of Moreira's version of Sard's Theorem

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

B

Higher-order encoder for B proof obligations to SMT-LIB 2.7

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ZFLean

A practical framework for set-theoretical development in Lean

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

order-p-q

Lean formalisation of the classification of the groups of order p * q where p and q are prime numbers.

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

Frucht

Formalization of Frucht's theorem in Lean

Declarations not yet indexedLean 4.29.0-rc4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Colorized

🌈 | A Lean 4 library designed to enhance terminal output with vibrant ANSI escape sequences.

Declarations not yet indexedLean stable

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

vizagrams

A visualization library for Lean

Declarations not yet indexedLean 4.20.0-rc5

Pinned Reservoir package record · checked 2026-07-25

Lean package