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

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

hax

Hax Lean library (automatically generated from cryspen/hax)

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

KrafftSieve

Formal Verification of the Krafft Geometry and the Additive Sieve Architecture

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

algebra

Algebra library for Lean 4

Declarations not yet indexedLean 4.29.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

logic

Logic Library for Lean 4

Declarations not yet indexedLean 4.29.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

sard

Work towards a general version of Sard's theorem in Lean 4

Declarations not yet indexedLean 4.12.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

FATE-M

The FATE-M (Formal Algebra Theorem Evaluation - Medium) benchmark.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

galeShapley

Formalization in Lean of some results related to stable matchings and the Gale-Shapley algorithm

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

LAGinLean

Questions related to Imperial College's Linear Algebra and Groups course running in November and December 2024.

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

proofs

random proofs in lean 4

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanML

Formally verified machine learning in Lean 4.

Declarations not yet indexedLean 4.30.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Calculemus2_es

Ejercicios de demostración con Lean4 e Isabelle/HOL.

Declarations not yet indexedLean 4.15.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package