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.

636 of 636 projects

Package metadataProof corpus

OSforGFF

A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

AgreeToDisagree

Lean formalizations of the paper "We Can't Agree to Disagree, Formally: Aumann's Theorem and Assumption Accounting in Lean"

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

importGraph

Tools to analyse and visualise the import structure of Lean packages and their files.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

fp-lean

Floating Point Semantics Mechanization for Lean

Declarations not yet indexedLean nightly-2026-01-14

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

MRiscX

A certified RISC-V Interpreter with Hoare-logic in Lean

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

SHerLOC

A StableHLO analyzer in Lean

Declarations not yet indexedLean 4.20.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

aegis

Verify Cairo contracts in Lean 4

Declarations not yet indexedLean 4.20.0-rc5

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

TNLean

Lean 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

polya-enumeration-theorem

A Lean 4 formalization of Pólya enumeration theorem.

Declarations not yet indexedLean 4.14.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

LeanDoomed

Simple Raycasting Example in Lean4 using SDL3

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanMySQL

A MySQL API for Lean 4

Declarations not yet indexedLean nightly-2022-03-09

Pinned Reservoir package record · checked 2026-07-25

Mysql
Package metadataLean library

NumLean

A Lean 4 package for heavy numerical computations

Declarations not yet indexedLean nightly-2022-01-15

Pinned Reservoir package record · checked 2026-07-25

Matrix
Package metadataProof corpus

FoML

Lean Formalization of Generalization Error Bound by Rademacher Complexity

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Regex

A PCRE2 compatible regular expression engine written in Lean 4.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Erdos870

Erdős Problem #870: paper and sorry-free, axiom-clean Lean 4 formalization.

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

putnam_like

Lean formalizations of Putnam-like problems

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean_eff

LeanEff is a small Lean 4 extensible-effects library

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

stage2-judge

This repository hosts the SAIR Mathematics Distillation Challenge: Equational Theories Stage 2, providing Lean 4 problem sets, judging tools, and submission harnesses for generating machine-checkable proof certificates.

Declarations not yet indexedLean 4.30.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package