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

imo

Lean formalizations of IMO problem statements

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4checker

Replay the Environment for a given Lean module, ensuring that all declarations are accepted by the kernel.

Declarations not yet indexedLean 4.29.0-rc8

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanSearchClient

Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

software-foundations-lean

📚 (WIP) Rewriting Software Foundations in Lean 4

Declarations not yet indexedLean 4.21.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

zkLeanEcosystem

zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

Declarations not yet indexedLean 4.25.2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

rust-lean-models

Lean models of Rust libraries

Declarations not yet indexedLean 4.11.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanMachineLearning

The Lean Machine Learning Library

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

haskell-spec

Formal specification of the Haskell Language Report

Declarations not yet indexedLean 4.22.0-rc4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

leancolls

WIP collections library for Lean 4

Declarations not yet indexedLean 4.13.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

VerifiedCompiler

A toy example of a verified compiler.

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

raylib

Raylib bindings for Lean4

Declarations not yet indexedLean pr-release-8152

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

SafeVerify

Leanstral's fork of SafeVerify, which we use for code agent training and as part of our evaluation stack.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

proofNet-lean4

ProofNet dataset ported into Lean 4

Declarations not yet indexedLean 4.20.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

wasm

Formalising the WASM spec in Lean

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ray

Formalizing results about the Mandelbrot set in Lean

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-machines

a Lean4 framework for the modeling and refinement of stateful systems

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

human-eval-lean

Hand-written verified Lean solutions for the HumanEval benchmark

Declarations not yet indexedLean nightly-2026-03-27

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lentil

(at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package