Package metadataProof corpus
fineqs
Lean4 formalization with Artistotle of the arXiv paper 1906.11174
Declarations not yet indexedLean 4.24.0
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
VersionControl
A repository for participation in the LeanLang for Autonomy Hackathon held from April 17 to May 01, 2026 at Indian Institute of Science, organised by Emergence AI.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
ff
Plonky3 formal verification framework
Declarations not yet indexedLean 4.22.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
sp1-poc
Proof-of-Concept Verification Infrastructure for SP1 zk chips
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanSeminar
Construction of a flow equivalent forest from a flow matrix in Lean 4
Declarations not yet indexedLean 4.7.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
checkdecls
Tiny Lean library to check existence of declarations
Declarations not yet indexedLean 4.18.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanDirectoryBrowser
It is a windows folder explorer written in lean4 (using code-proxy).
Declarations not yet indexedLean stable
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
QuadraticIntegers
Formalising the Ring of Integers in Quadratic Fields in the Lean proof assistant.
Declarations not yet indexedLean 4.24.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
CdFormal
Lean 4 + Mathlib formalization of the Creative Determinant framework - 15 theorems proved with zero sorry, CI-enforced via lake build --wfail
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
mathmatic_in_elementary_number_th
elementary number theory
Declarations not yet indexedLean 4.24.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataLean library
LeanToolkit
A set of tools and extensions for Lean
Declarations not yet indexedLean stable
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Pigment
Terminal colors and styling for Lean 4
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
toy-verifier
Minimal static analysis based verifier for educational purpose
Declarations not yet indexedLean 4.25.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
LeanAideTools
Tools, specifically for running tactics in the background, with minimal dependencies
Declarations not yet indexedLean 4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
adele-ring_locally-compact
The proof that the adele ring of a number field is locally compact, formalised in Lean 4.
Declarations not yet indexedLean 4.10.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean tool
leaner
🪶 | A linter, formatter and whole-program dead code eliminator for Lean 4
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
Monlib
Formalising non-commutative graph theory in Lean
Declarations not yet indexedLean 4.21.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataLean library
SPG
A Lean 4 library for analyzing Spin Point Groups
Declarations not yet indexedLean 4.29.0-rc4
Pinned Reservoir package record · checked 2026-07-25
Lean package