Package metadataProof corpus
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Declarations not yet indexedLean 4.29.0-rc8
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.
134 of 636 projects
Clear searchPackage metadataProof corpus
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Declarations not yet indexedLean 4.33.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
glimpseOfLean
An introduction to theorem proving in Lean for the impatient.
Declarations not yet indexedLean 4.27.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
llmstep
llmstep: [L]LM proofstep suggestions in Lean 4.
Declarations not yet indexedLean 4.1.0
Pinned Reservoir package record · checked 2026-07-25
LlmTheorem Proving
Package metadataProof corpus
matrix_cookbook
The matrix cookbook, proved in the Lean theorem prover
Declarations not yet indexedLean 4.22.0-rc4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Project
A template for blueprint-driven formalization projects in Lean.
Declarations not yet indexedLean 4.28.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
risc0-lean4
A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover
Declarations not yet indexedLean nightly-2022-12-23
Pinned Reservoir package record · checked 2026-07-25
Risc0Zero KnowledgeZk StarkZkvm
Package metadataProof corpus
problems
Formalization of the Millennium Problems in Lean 4
Declarations not yet indexedLean 4.31.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
KLR
A formalization of ML kernel languages
Declarations not yet indexedLean 4.23.0
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
FelConjecture
Lean formalizations for the paper "Fel's conjecture on syzigies of numerical semigroups"
Declarations not yet indexedLean 4.26.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
unsorry
Autonomous agents proving theorems in Lean 4 - SETI@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.
Declarations not yet indexedLean 4.30.0
Pinned Reservoir package record · checked 2026-07-25
Math
Package metadataProof corpus
FLT3
Proof in Lean of Fermat Last Theorem for exponent 3
Declarations not yet indexedLean 4.9.0-rc3
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
Rubik
Lean 4 formalization of Rubik's cubes
Declarations not yet indexedLean 4.17.0-rc1
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
groebner
Formalization of Gröbner basis theory in Lean4 (WIP)
Declarations not yet indexedLean 4.29.0-rc8
Pinned Reservoir package record · checked 2026-07-25
Math
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
Package metadataProof corpus
Clawristotle
OpenClaw-style theorem proving
Declarations not yet indexedLean 4
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
IMOSLLean4
Formalization of IMO shortlist problems in Lean 4
Declarations not yet indexedLean 4.30.0-rc2
Pinned Reservoir package record · checked 2026-07-25
Lean package
Package metadataProof corpus
lean4-analysis-tao
Formalization of "Analysis I" by Terence Tao
Declarations not yet indexedLean 4.29.0
Pinned Reservoir package record · checked 2026-07-25
Lean package