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.

26 of 636 projects

Clear search

Exact source indexedLean library

Iris-Lean

A Lean port of the Iris higher-order concurrent separation-logic framework.

19 indexed declarationsLean 4.32.1

Curated repository record · checked 2026-07-25

abstract lang completenessbig opco psetConcurrency

Exact source indexedProof corpus

Con(NF)

A completed formalization of the difficult part of the consistency proof for Quine's New Foundations set theory.

7 indexed declarationsLean 4.21.0-rc3

Curated repository record · checked 2026-07-25

base permconclusionsconsistencyflex approx

Exact source indexedLean library

Foundation

A formal metatheory library covering axiomatic systems, syntax, semantics, proof theory, and incompleteness.

31 indexed declarationsLean 4.32.1

Curated repository record · checked 2026-07-25

basicchurchcounter modelfirst

Exact source indexedProof corpus

Harder-Narasimhan

A formalization of Harder-Narasimhan filtrations and related results for vector bundles.

75 indexed declarationsLean 4.31.0

Curated repository record · checked 2026-07-25

Algebraic geometrycategory theorycommutative algebradedekind mac neille completion

Exact source indexedLean library

quantumInfo

Quantum information theory in Lean 4

115 indexed declarationsLean 4.28.0

Pinned Reservoir package record · checked 2026-07-25

braketbundledcapacitydistribution

Exact source indexedLean library

debate

Formalizing stochastic doubly-efficient debate

52 indexed declarationsLean 4.8.0

Pinned Reservoir package record · checked 2026-07-25

arithbasicbasicschernoff

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

Exact source indexedProof corpus

PDE

PDE Lean formalization

41 indexed declarationsLean 4.30.0

Pinned Reservoir package record · checked 2026-07-25

analysisheat kernelheat solutionheat solution property