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

special-numbers

Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

KummerCriterion

Proof of Kummer's criterion for regularity of a prime in Lean

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

swaps-perm

Mathematically defines of permutations of arrays and proves related theorems

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Distributed2Coloring

2-Coloring Cycles in One Round: Formalization in Lean 4

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

lean-test

lean4 unit testing framework

Declarations not yet indexedLean 4.25.2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

bitmap

Lean 4 bitmap utilities with PNG encode/decode support, plus a small widget for visualization.

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

BitmapGraphicsImagePng
Package metadataLean library

ForestIPM

📦 R package - Bayesian hierarchical Integral Projection Model (IPM) for forest trees in eastern North America

Declarations not yet indexedLean 4.29.0-rc8

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

ChandraFurstLipton

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

FormalRV

Formal resource verification of Shor's algorithm.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ac-library

ac-library for lean4

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mathmatic_in_elementary_number_th

IMO题目的形式化2个题

Declarations not yet indexedLean 4.24.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Logos_Library

Lean verified Science.

Declarations not yet indexedLean 4

Pinned Reservoir package record · checked 2026-07-25

Dirac EquationHeisenbergQuantum MechanicsRelativity
Package metadataLean library

loadTerms

Testing dynamic term loading in Lean 4.

Declarations not yet indexedLean stable

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

safeIdx

Type-safe indexing library.

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

Quave

Quantum Hoare Logic Lean 4 - A quantum program verification tool

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

HexLuthor

Lean 4 hex color syntax with inline VS Code color preview

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

lean-autograd

Automatic differentiation in Lean following JAX's autodidax tutorial

Declarations not yet indexedLean nightly

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanDidax2

Pedagogical autodiff library in Lean 4 with forward/reverse modes and vectorization

Declarations not yet indexedLean nightly-2025-03-09

Pinned Reservoir package record · checked 2026-07-25

Lean package