Package metadataProof corpus
Lie
A classification theorem in Lean of solvable Lie algebras of dimension zero to three
Declarations not yet indexedLean 4.19.0
Pinned Reservoir package record · checked 2026-07-25
Math
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.
134 of 636 projects
Clear searchPackage metadataProof corpus
EconCSLib
AI-assisted Lean formalization for Economics and Computation research
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
bruhat-tits
A formalisation of the Bruhat-Tits tree in Lean4
Declarations not yet indexedLean 4.19.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
incompleteness
Formalize Incompleness Theorem Related Results
Declarations not yet indexedLean 4.16.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
MathProbabilityRandom Matrix Theory
Package metadataProof corpus
phi-confluence
Proof of 𝜑-calculus confluence in Lean4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
HadwigerNelson
Hadwiger-Nelson Problem Formalization in Lean 4
Declarations not yet indexedLean nightly-2024-07-11
Pinned Reservoir package record · checked 2026-07-25
Lean package
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
Package metadataProof corpus
kolmogorov_complexity
Formalization of Algorithmic Information Theory in Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
PersistentDecomp
Formalizing the Structure Theorem for Persistence Modules
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
chip-firing-with-lean
A formalization of chip-firing games and the Riemann-Roch theorem for graphs using the Lean 4 theorem prover.
Declarations not yet indexedLean 4.31.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
GameTheory
Formalization of Game Theory in Lean4
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Game TheoryMath
Package metadataProof corpus
reactor-model
A Lean-based formalization of the Reactor model.
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
CliffordProject
Lean formalization of the structure theorem for the single-qudit Clifford group
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Weights
Formalization in Lean4 of some results in "Minimization of hypersurfaces" by A.-S. Elsenhans and myself
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
Kaplansky4
Proof of Kaplanski criterion for being a UFD in Lean4
Declarations not yet indexedLean 4.26.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
complexitylib
Formalization of complexity theory
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
sensitivity
Lean 4 formalization of the Sensitivity Conjecture (Huang 2019)
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math