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 74ac4b5 builds on the recent leanprover/lean4:v4.20.0
mathlib
The math library of Lean 4
Commit 8c91154 builds on the recent leanprover/lean4:v4.20.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 152f1b4 builds on the recent leanprover/lean4:v4.20.0-rc5
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 7f9ec4e builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 164b8db builds on the recent leanprover/lean4:v4.20.0
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the old leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit 1c29672 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 7779c23 builds on the recent leanprover/lean4:v4.20.0
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 233a67f builds on the recent leanprover/lean4:v4.20.0-rc5
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit c548baa builds on the recent leanprover/lean4:v4.20.0
aesop
White-box automation for Lean 4
Newly Created Commit 1c29672 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 5ec9f03 builds on the old leanprover/lean4-pr-releases:pr-release-8003
mini-redis
An implementation of mini-redis in Lean 4
Commit 6866f29 builds on the old leanprover/lean4:v4.18.0
verina
Commit d1d2a02 builds on the recent leanprover/lean4:v4.20.0
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Commit 7f9ec4e 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.20.0
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
Commit 156e3b2 builds on the recent leanprover/lean4:v4.20.0
rupert
Formalization of the Rupert Problem for convex polyhedra.
Recently Updated Commit 74ac4b5 builds on the recent leanprover/lean4:v4.20.0
mathlib
The math library of Lean 4
Commit 1c29672 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 7f4d327 builds on the old leanprover/lean4:v4.19.0
Clean
Lean circuit DSL
Commit b8b19c7 builds on the recent leanprover/lean4:v4.20.0
carleson
A formalized proof of Carleson's theorem in Lean
Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
SSA
A minimal development of SSA theory
Commit 152f1b4 builds on the recent leanprover/lean4:v4.20.0-rc5
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 989b94b builds on the recent leanprover/lean4:v4.20.0-rc5
ABCExceptions
Exceptions to the ABC conjecture in Lean
Commit 7f9ec4e builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 7518aca builds on the recent leanprover/lean4:v4.20.0
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets
Commit 233a67f builds on the recent leanprover/lean4:v4.20.0-rc5
batteries
The "batteries included" extended library for the Lean programming language and theorem prover