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

CatDG

Aspects of categorical differential geometry, formalised in lean 4.

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

miniF2F-lean4

miniF2F dataset ported into Lean 4

Declarations not yet indexedLean 4.6.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

RelationalAlgebra

University Master Thesis

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

lean-gccjit

libgccjit bindings for Lean4

Declarations not yet indexedLean 4.1.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

riddle-proofs

Riddles solved in Lean4 for educational purposes

Declarations not yet indexedLean 4.22.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

controlflow

A control flow graph library for Lean

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

automated_Theory_Construction

A prototype framework for automated theory construction in Lean 4.

Declarations not yet indexedLean 4.29.0-rc6

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

cryptolib

The cryptography library of Lean 4

Declarations not yet indexedLean 4.19.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Quantum4Lean

Verified quantum computing in Lean 4 with FFI bridge to Apple Silicon (Metal 3). Full NISQ stack, dependent types, formal circuit verification, and mathematical translators to Hamiltonians for autonomous AI.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

frieze_patterns

A project to formalise Coxeter's frieze patterns

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

aoc2022

Advent of Code 2022 solutions: Lean4

Declarations not yet indexedLean 4

Pinned Reservoir package record · checked 2026-07-25

Advent Of CodeAdvent Of Code 2022
Package metadataLean library

bignum

port of s2n-bignum to Lean

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Straume

State-of-the-art streams for Lean 4

Declarations not yet indexedLean 4.4.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

PartialRegularity

Lean formalizations for the paper "Almost all primes are partially regular"

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

time

Port of the haskell time library to Lean 4 and verification of date calculations

Declarations not yet indexedLean 4.20.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-redis

full featured async redis client for lean 4

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

UnicodeSkipListTable

A library to create and use Unicode tables based on the skip list data structure.

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

pod

Low level utils (single precision float, byte spans, unboxed vector, finalization callbacks, fixnums, deque, slotmap etc; implemented via ffi)

Declarations not yet indexedLean nightly-2026-06-29

Pinned Reservoir package record · checked 2026-07-25

Lean package