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

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 tool

MutualInduction

A mutual induction tactic for Lean 4.

Declarations not yet indexedLean 4.32.0

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

llm

Interfacing with Large Language Models (remote and local) from Lean.

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Hesper

Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accelerated matrix ops, and cross-platform support (Metal/Vulkan/D3D12). Build provably correct GPU compute and ML inference engines.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-eval

Comparator-based Lean formal mathematics eval

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

readLean

How to read Lean

Declarations not yet indexedLean 4.12.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanCat

Lean4 benchmark on 1 category.

Declarations not yet indexedLean 4.19.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Vericoding

tools and benchmarks for verified coding

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

raylean

Lean4 bindings for raylib

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mathlib4-help

List of the output of #help command of mathlib4, including list of all tactics, commands...etc

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

lean2wasm

Tool for compiling Lean to WASM

Declarations not yet indexedLean 4.6.1

Pinned Reservoir package record · checked 2026-07-25

Wasm