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.

433 of 636 projects

Clear search
Package metadataLean library

VirasoroProject

Lean project on the Virasoro algebra (2-cohomology of the Witt algebra, definition of the Virasoro algebra, ...)

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

runwai_project

COMS 6998 (Fall 2025): Refinement-typed DSL for certified AIR constraints and lookups

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-machines-examples

Example specifications for the Lean Machines modelling framework

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

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

DimensionalAnalysis

Formally-verified dimensional analysis in Lean

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

NumpySpec

numpy -> lean 4 through ai

Declarations not yet indexedLean nightly

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

HighDimProb

Lean 4 formalizations for high-dimensional probability, random matrices, concentration inequalities, and matrix Bernstein bounds.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

bottcher

Verified computation of the Mandelbrot set Böttcher series

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

CBPV

Lean 4 mechanization of assorted CBPV metatheory.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Game

An interactive game introducing the concept of a filter.

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package