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

math654

Homework and lecture notes from Math 654, Fall 2022

Declarations not yet indexedLean 4.27.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

SHSLib

Stochastic Hybrid Systems core definitions formalized in Lean

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

FormalizationMathStochastic Hybrid Systems
Package metadataLean library

lean4-project

A minimal Lean 4 development environment using VSCode DevContainer.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

Monad

Notes for the category theory class I'm teaching at MIT (Jan 2026)

Declarations not yet indexedLean 4.29.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Iterator

In this repository, I work on the Lean iterator library that is supposed to become part of the standard library.

Declarations not yet indexedLean 4.20.0-rc5

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

bppl

Probabilistic Separation Logic

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

FATE-H

The FATE-H (Formal Algebra Theorem Evaluation-Hard) benchmark.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Crypto

Implementation of various cryptographic functions in Lean4

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

CryptographyElliptic Curves
Package metadataLean library

Hoare

Hoare Logic in Lean

Declarations not yet indexedLean 4.22.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

FMCn_Lean

Repositório destinado às práticas de Lean4 da Monitoria de FMCn.

Declarations not yet indexedLean stable

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

crup

A Checker for RUP proofs written in Lean 4

Declarations not yet indexedLean 4.3.0

Pinned Reservoir package record · checked 2026-07-25

RupSat
Package metadataLean library

http-client

A Curl wrapper written in Lean 4 to be used as a http-client in lean 4 projects

Declarations not yet indexedLean 4.25.2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

mathmatic_in_elementary_number_th

初等数论讲义的形式化证明 by lean4

Declarations not yet indexedLean 4.24.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataProof corpus

lean-glfw

C bindings and marshalling to use GLFW and OpenGL from the lean4 theorem prover

Declarations not yet indexedLean nightly-2022-02-21

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

sgc

Lean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems

Declarations not yet indexedLean 4.25.2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

curljson

curljson: a small Lean4 library to fetch JSON with libCurl

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

MasterDiss

Proving the main theorem of polytopes using Lean 4

Declarations not yet indexedLean 4.7.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

ec-tate-lean

Elliptic curve algorithm verification project built on mathib4

Declarations not yet indexedLean nightly-2023-08-19

Pinned Reservoir package record · checked 2026-07-25

Lean package