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

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

Leantix

Lean 4 port of the Golitex typesetting system for LaTeX-like document processing

Declarations not yet indexedLean nightly-2025-06-09

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

MusicNotation

Pure functional music notation system in Lean 4 with Unicode visualization

Declarations not yet indexedLean nightly-2025-03-30

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

tetraGray

General-relativistic raytracer in Lean 4 with geometric algebra for black hole visualization

Declarations not yet indexedLean nightly

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-stlc

Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-url

URL library for lean4 based on the whatwg url standard

Declarations not yet indexedLean 4.22.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

validator

Formally Verified Validator for Unsolvability Certificates for Automated Planning in Lean 4

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

PartitionPolynomial

Lean formalizations for the paper "Reciprocals of Partition Polynomials"

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math