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

imscrbgrmr-lean

A 12-primitive measurement apparatus for the structural type of any system - 17,280,000-address Crystal of Types

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

event-structures

Formalisation of some facts about event structures and reversibility

Declarations not yet indexedLean 4.28.1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

ForbiddenMatrix

Formalisation of forbidden matrix theory

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

CombinatoricsExtremal CombinatoricsForbidden Matrix TheoryMath
Package metadataLean library

sigma

Formal verification of knowledge soundness for Generalized Bulletproofs

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanServer

Verified HTTPS server in Lean 4 - TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC - 914 machine-checked theorems, zero sorry. Pure library available (LeanServerPure).

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

NormalForms

Executable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

LeanMathlibNormal Forms