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

socket

sockets for Lean 4

Declarations not yet indexedLean 4.19.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 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 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 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
Package metadataLean library

LeanPlot

Interactive React-powered charting library for Lean 4 in VS Code's infoview

Declarations not yet indexedLean 4.32.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LatticeTriangle

Lean formalizations for the paper "On the paucity of lattice triangles"

Declarations not yet indexedLean 4.26.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

stlc

Simply Typed Lambda Calculus with de Bruijn indices

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Zklib

deprecated, use Verified-zkEVM repository instead

Declarations not yet indexedLean 4.15.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean-loris

Experiments with some ways of automating reasoning in lean 4

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package