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

MetaExamples

Examples using MetaProgramming for writing tactics etc.

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Game

Make/Encode some basic logic puzzles

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

regexderiv

Proofs written in Lean4 for the core katydid validation algorithm

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

RustFFI.lean

Template for Lean<->Rust FFI

Declarations not yet indexedLean nightly-2022-12-08

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

FloatSpec

Formally Verified Float Implementation with lean4

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ast_export

AST export from Lean 4

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Noperthedron

The Noperthedron does not have Rupert Property: a proof in Lean4

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

AddCombi

The sublibrary of Mathlib dedicated to additive combinatorics

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Additive CombinatoricsMath
Package metadataLean library

Cookbook

A cookbook for Metaprogramming in Lean4 containing code snippets to help you code!

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-linq

Type-safe, deeply-embedded SQL query DSL for Lean 4 - LINQ-style pipelines and query! comprehensions compiling to parameterized SQL for SQLite, PostgreSQL, and SQL Server

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

DatabaseDslLinqSql
Package metadataLean library

DateTime

DateTime package for Lean 4

Declarations not yet indexedLean 4.5.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

leanses

Lean lens implementation with custom notation.

Declarations not yet indexedLean nightly-2025-06-05

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

proof_zk_recovery_ci

ZK recovery contract: design, audits, and prototyping (private)

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

UnicodeBasic

Basic Unicode support for Lean 4

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Unicode
Package metadataLean library

lean-yjs

Lean-Yjs: Formal Verification of Yjs Integration Algorithm

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

quantumlib

A Quantum Computing Library in LEAN

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

monoid.space

Learn pure math with agda :rocket:

Declarations not yet indexedLean 4.24.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Abstract AlgebraAgdaCategory TheoryType Theory
Package metadataLean library

lean99

These are Lean translations of Ninety-Nine Haskell Problems (WIP)

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package