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

SafeVerify

A Lean4 script for robustly verifying submitted proofs of theorems and implementations of functions

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

mathport

Mathport is a tool for porting Lean3 projects to Lean4

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

CompPoly

Computable Polynomials in Lean.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

LeanCourse

Bonn Lean course for winter 24/25

Declarations not yet indexedLean 4.13.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

ssreflect

LeanSSR: an SSReflect-Like Tactic Language for Lean

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanCert

Verified interval arithmetic for Lean 4 - prove bounds on exp, sin, cos, find roots, all machine-checked

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

TensorLib

A verified tensor library in Lean

Declarations not yet indexedLean 4.23.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lib

Solving Competition Geometry Problems in Lean

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

reap

General neural tactic for Lean 4

Declarations not yet indexedLean 4.28.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

formal-slt

Zero-sorry Lean 4 library of finite-sample statistical learning theory: PAC-Bayes (incl. a five-component test-time meta-bound), VC, Rademacher, sharp McDiarmid, and Dudley chaining. ICML 2026 AI4MATH

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

algorithm

Verified efficient algorithms in Lean4.

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

KittyCats

Category theory but for kitty cats, meow 🐱🐈

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

unsorry

Autonomous agents proving theorems in Lean 4 - SETI@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.

Declarations not yet indexedLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

htpi

Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It"

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

trzk

Verified Optimizing Compiler for Cryptographic Primitives

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

FLT3

Proof in Lean of Fermat Last Theorem for exponent 3

Declarations not yet indexedLean 4.9.0-rc3

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean tool

tryAtEachStep

Try a tactic at each step in a Lean proof.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanTeX

Lean 4 library for pretty printing expressions as LaTeX

Declarations not yet indexedLean 4.18.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package