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 a03ab30 builds on the recent leanprover/lean4:v4.22.0-rc3
mathlib
The math library of Lean 4
Commit 7714b4f builds on the recent leanprover/lean4:v4.22.0-rc2
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 12904fc builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 9feced6 builds on the recent leanprover/lean4:v4.22.0-rc2
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 902b97d builds on the recent leanprover/lean4:v4.22.0-rc2
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 3cabaef builds on the recent leanprover/lean4:v4.22.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 79a3546 builds on the recent leanprover/lean4:v4.21.0
PhysLean
A project to digitalise results from physics into Lean.
Newly Created Commit 71a283a builds on the recent leanprover/lean4:v4.22.0-rc2
Numbers
An introduction to numbers
Commit 3125b8a builds on the recent leanprover/lean4:v4.21.0-rc3
cslib
Lean library for Computer Science
Commit a2d4eab fails to build on leanprover/lean4:v4.22.0-rc2
tactic-programming-beginner-guide
Beginner's guide to Tactic Programming in Lean
Commit 1bdab83 builds on the recent leanprover/lean4:v4.22.0-rc2
haskell-spec
Formal specification of the Haskell Language Report
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 7351fae 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 6c99d80 builds on the recent leanprover/lean4:v4.22.0-rc2
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Commit 7087b15 fails to build on leanprover/lean4:v4.22.0-rc2
lie-classification
Classification of Lie algebras in Lean
Recently Updated Commit a03ab30 builds on the recent leanprover/lean4:v4.22.0-rc3
mathlib
The math library of Lean 4
Commit f5f81cd builds on the recent leanprover/lean4:v4.20.1
Clean
Lean circuit DSL
Commit 13c9ccb builds on the old leanprover/lean4:v4.19.0-rc2
Seymour
This project is about formally verifying Seymour's decomposition theorem for regular matroids.
Commit 4182d4d builds on the recent leanprover/lean4:v4.21.0
Toric
Formalisation of toric varieties in Lean 4
Commit 1e08a0e fails to build on leanprover/lean4:v4.22.0-rc3
verso-manual
The Lean reference manual
Commit 163ea67 builds on the recent leanprover/lean4:v4.22.0-rc2
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 559fd52 builds on the old leanprover/lean4:v4.18.0
trestle
Commit ae14d73 fails to build on leanprover/lean4:v4.22.0-rc2
HopfieldNet
Commit 7e8c7aa builds on the old leanprover/lean4:v4.16.0-rc1
lean-regex
Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I