Package metadataLean library
Leantix
Lean 4 port of the Golitex typesetting system for LaTeX-like document processing
Declarations not yet indexedLean nightly-2025-06-09
Pinned Reservoir package record · checked 2026-07-25
Lean package
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
MusicNotation
Pure functional music notation system in Lean 4 with Unicode visualization
Declarations not yet indexedLean nightly-2025-03-30
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
tetraGray
General-relativistic raytracer in Lean 4 with geometric algebra for black hole visualization
Declarations not yet indexedLean nightly
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-stlc
Lean4 mechanization of the simply typed lambda calculus and its metatheory including strong normalization
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean-url
URL library for lean4 based on the whatwg url standard
Declarations not yet indexedLean 4.22.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
validator
Formally Verified Validator for Unsolvability Certificates for Automated Planning in Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
PartitionPolynomial
Lean formalizations for the paper "Reciprocals of Partition Polynomials"
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
hax
Hax Lean library (automatically generated from cryspen/hax)
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
KrafftSieve
Formal Verification of the Krafft Geometry and the Additive Sieve Architecture
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
algebra
Algebra library for Lean 4
Declarations not yet indexedLean 4.29.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
logic
Logic Library for Lean 4
Declarations not yet indexedLean 4.29.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
sard
Work towards a general version of Sard's theorem in Lean 4
Declarations not yet indexedLean 4.12.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
FATE-M
The FATE-M (Formal Algebra Theorem Evaluation - Medium) benchmark.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
galeShapley
Formalization in Lean of some results related to stable matchings and the Gale-Shapley algorithm
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataTeaching project
LAGinLean
Questions related to Imperial College's Linear Algebra and Groups course running in November and December 2024.
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
proofs
random proofs in lean 4
Declarations not yet indexedLean 4.32.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanML
Formally verified machine learning in Lean 4.
Declarations not yet indexedLean 4.30.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Calculemus2_es
Ejercicios de demostración con Lean4 e Isabelle/HOL.
Declarations not yet indexedLean 4.15.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package