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 metadataLean library

evmSmith

A framework for AI systems to write EVM bytecode and prove it safe, built on NethermindEth/EVMYulLean.

Declarations not yet indexedLean 4.22.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Megaparsec.lean

Lean 4 port of Megaparsec

Declarations not yet indexedLean 4.0.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4export

Plain-text declaration export for Lean 4

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Chess

Chess in Lean 4

Declarations not yet indexedLean 4.15.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

imo

Lean formalizations of IMO problem statements

Declarations not yet indexedLean 4.27.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

lean4checker

Replay the Environment for a given Lean module, ensuring that all declarations are accepted by the kernel.

Declarations not yet indexedLean 4.29.0-rc8

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Rubik

Lean 4 formalization of Rubik's cubes

Declarations not yet indexedLean 4.17.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataTeaching project

Game

A game for learning Lean 4 where a cute little smart-elf joins you on your exploration of the Leaniverse.

Declarations not yet indexedLean 4.31.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanSearchClient

Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

software-foundations-lean

📚 (WIP) Rewriting Software Foundations in Lean 4

Declarations not yet indexedLean 4.21.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

zkLeanEcosystem

zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements

Declarations not yet indexedLean 4.25.2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

rust-lean-models

Lean models of Rust libraries

Declarations not yet indexedLean 4.11.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

groebner

Formalization of Gröbner basis theory in Lean4 (WIP)

Declarations not yet indexedLean 4.29.0-rc8

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

LeanMachineLearning

The Lean Machine Learning Library

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

haskell-spec

Formal specification of the Haskell Language Report

Declarations not yet indexedLean 4.22.0-rc4

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

leancolls

WIP collections library for Lean 4

Declarations not yet indexedLean 4.13.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

VerifiedCompiler

A toy example of a verified compiler.

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Exact source indexedProof corpus

DeGiorgi

Lean 4 formalization of De Giorgi-Nash-Moser theory

146 indexed declarationsLean 4.29.0-rc6

Pinned Reservoir package record · checked 2026-07-25

analysisapproximationball extensionball scaling