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

DimensionalAnalysis

Formally-verified dimensional analysis in Lean

Declarations not yet indexedLean 4.23.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

NumpySpec

numpy -> lean 4 through ai

Declarations not yet indexedLean nightly

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

HighDimProb

Lean 4 formalizations for high-dimensional probability, random matrices, concentration inequalities, and matrix Bernstein bounds.

Declarations not yet indexedLean 4.29.1

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

bottcher

Verified computation of the Mandelbrot set Böttcher series

Declarations not yet indexedLean 4.26.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

CBPV

Lean 4 mechanization of assorted CBPV metatheory.

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

Game

An interactive game introducing the concept of a filter.

Declarations not yet indexedLean 4.7.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

eocia-lean

Essentials of Compilation: An Incremental Approach in Lean 4

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

leanproject

GitHub repository for the seminar on Computer-assisted mathematics held at the University of Heidelberg during the Summer Semester of 2024.

Declarations not yet indexedLean 4.10.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Computer Algebra SystemFormalizationMathematicsSage
Package metadataLean library

GL

Craig interpolation for GL in Lean

Declarations not yet indexedLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

Heights

An attempt at formalizing the theory of heights in Lean

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

ExistentialRules

This repo contains formalizations around Existential Rules (aka. Tuple-Generating Dependencies) with disjunctions and the Chase algorithm. Mostly this will be about (basics of) my own formal works.

Declarations not yet indexedLean 4.32.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

LeanRPC

Serve Lean 4 functions as RPC methods over HTTP

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataLean library

paranoia

Lean 4 proof verification without reference

Declarations not yet indexedLean 4.25.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

MCMC

Formalization of Markov Chain Monte Carlo in Lean 4

Declarations not yet indexedLean 4.29.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

Redhill

A formalisation of the disproof of Ramaekers's conjecture

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

CHANGE

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

Declarations not yet indexedLean 4.24.0

Pinned Reservoir package record · checked 2026-07-25

Lean package
Package metadataProof corpus

BooleanFun

Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.

Declarations not yet indexedLean 4.16.0-rc2

Pinned Reservoir package record · checked 2026-07-25

Math
Package metadataLean library

import-all

This script can check and auto-generate import statements in a lean4 repository.

Declarations not yet indexedLean 4.33.0-rc1

Pinned Reservoir package record · checked 2026-07-25

Lean package