Package metadataLean library
discretion
Utilities for formalizing programming languages in Lean 4, along with other tidbits
Declarations not yet indexedLean 4.20.0-rc5
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.
600 of 636 projects
Clear searchPackage metadataProof corpus
ArtinWedderburn
A formalized proof of Artin-Wedderburn theorem in Lean4
Declarations not yet indexedLean 4.14.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataTeaching project
msri2023_graphs
Repository for graph theory & combinatorics group at the MSRI Lean summer school
Declarations not yet indexedLean nightly-2023-06-10
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
pol
Proof of Lean: Formalizing Blockchain Fundamentals in Lean
Declarations not yet indexedLean 4.22.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
sos
A Lean 4 sum-of-squares tactic for nonlinear real arithmetic.
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
MathReal ArithmeticSoftware VerificationTactic
Package metadataLean library
Dcc
The dependently-typed combinator calculus (DCC).
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
foam
geometry of hospitality
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Koch
Koch 2D snowflake generator for 4D Golf
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
HigherCategoryTheory
A formal verification project based on the work by Enric Cosme Llópez on "Higher-order categories".
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
Game
Abstract Algebra Game
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
legendre_QF
Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
SpectralPositivity
Perron-Frobenius, Jentzsch theorem, and matrix/operator positivity in Lean 4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
langlib
Library for formal language theory in Lean 4
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
pacioli
A verified core of accounting mechanics in Lean 4, paired with curated accounting judgment in the Open Knowledge Format (OKF).
Declarations not yet indexedLean 4.32.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Symm
Formalization of a new data structure: Dashed-Monoids
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
lean4-base64
RFC 4648 Base64 encoding and decoding for Lean 4
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
OrdvecFormalization
Lean 4 formalization of finite Bayes-threshold optimality for OrdVec overlap models.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
SDG
Synthetic Differential Geometry in Lean
Declarations not yet indexedLean 4.30.0-rc2-less-choice
Pinned Reservoir package record · checked 2026-07-25
Lean package