Reservoir indexes, builds, and tests packages within the Lean and Lake ecosystem. If you wish to see your package here, ensure that it meets the Reservoir inclusion criteria .
Most Popular Commit 2642f52 builds on the recent leanprover/lean4:v4.21.0-rc3
mathlib
The math library of Lean 4
Commit 2b2d590 builds on the recent leanprover/lean4:v4.21.0-rc3
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 4665e8c builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 405fa59 builds on the recent leanprover/lean4:v4.21.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 902b97d builds on the recent leanprover/lean4:v4.21.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
scilean
Scientific computing in Lean 4
Commit 4de9edc builds on the recent leanprover/lean4:v4.20.1
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 5e6a775 builds on the recent leanprover/lean4:v4.21.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit c3a19fa builds on the recent leanprover/lean4:v4.21.0-rc3
aesop
White-box automation for Lean 4
Newly Created Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
Lie
A classification theorem in Lean of solvable Lie algebras of dimension zero to three
Commit 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
mini-redis
An implementation of mini-redis in Lean 4
Commit d3d5bbf builds on the old leanprover/lean4:v4.18.0
verina
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Commit 9f0f43c builds on the recent leanprover/lean4:v4.21.0-rc3
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Commit 7087b15 fails to build on leanprover/lean4:v4.21.0-rc3
lie-classification
Classification of Lie algebras in Lean
Commit 4665e8c builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit b8d0cec builds on the old leanprover/lean4:v4.19.0
bruhat-tits
A formalisation of the Bruhat-Tits tree in Lean4
Commit 90fd935 builds on the recent leanprover/lean4:v4.21.0-rc3
LeanPlot
Commit 52447ae builds on the recent leanprover/lean4:v4.20.0-rc5
logic-formalization
Formalize "Logic Notes" by Lou van den Dries in Lean
Recently Updated Commit a32c42e builds on the old leanprover/lean4:v4.18.0
ix
a zero-knowledge proof-carrying code platform for Lean 4
Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit a0a6806 builds on the recent leanprover/lean4:v4.21.0-rc3
carleson
A formalized proof of Carleson's theorem in Lean
Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
KLR
A formalization of ML kernel languages
Commit 2642f52 builds on the recent leanprover/lean4:v4.21.0-rc3
mathlib
The math library of Lean 4
Commit 5e6a775 builds on the recent leanprover/lean4:v4.21.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 405fa59 builds on the recent leanprover/lean4:v4.21.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit fb52bde builds on the recent leanprover/lean4:v4.21.0-rc3
BirkhoffErgodicThm
A proof of Pointwise Birkhoff Ergodic Theorem in Lean
Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
SSA
A minimal development of SSA theory
Commit d4367e8 builds on the recent leanprover/lean4:v4.21.0-rc3
compfiles
Catalog Of Math Problems Formalized In Lean