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 dd2e6e3 builds on the recent leanprover/lean4:v4.16.0-rc1
mathlib
The math library of Lean 4
Commit 3b9be01 builds on the recent leanprover/lean4:v4.16.0-rc1
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 8216cd9 builds on the recent leanprover/lean4:v4.16.0-rc1
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the recent leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit 35bb6ec builds on the recent leanprover/lean4:v4.16.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit e5aeb77 builds on the old leanprover/lean4:v4.14.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 03f408f builds on the recent leanprover/lean4:v4.16.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 59e4e66 builds on the recent leanprover/lean4:v4.16.0-rc1
lean4-metaprogramming-book
Commit 79402ad builds on the recent leanprover/lean4:v4.16.0-rc1
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.16.0-rc1
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 415892f builds on the recent leanprover/lean4:v4.15.0-rc1
vqc_in_lean
Lean 4 port of the Verified Quantum Computing. Developed as a personal learning project to deepen understanding of quantum computing concepts and formal verification.
Commit 8937ae0 builds on the recent leanprover/lean4:v4.15.0
leanblas
Bindings and specification for BLAS
Commit e7147ca builds on the recent leanprover/lean4:v4.16.0-rc1
NodeGraph
Commit 0a5a174 builds on the old leanprover/lean4:v4.14.0-rc2
special-numbers
Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)
Commit 9034b20 builds on the recent leanprover/lean4:v4.15.0
partial-combinatory-algebras
A Lean 4 formalization of partial combinatory algebras.
Commit 2470c19 builds on the recent leanprover/lean4:v4.16.0-rc1
CodeProofTheArena
Lean coding problem solving challenge website with proof verification
Commit 9f3241a builds on the recent leanprover/lean4:v4.15.0-rc1
remco-mul
Commit 4eb38e1 builds on the recent leanprover/lean4:v4.16.0-rc1
order-pq
Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
Commit 656070c builds on the recent leanprover/lean4:v4.15.0
borel_det
Commit 571ea7a fails to build on leanprover/lean4:v4.16.0-rc1
verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Recently Updated Commit fe5f2b3 builds on the recent leanprover/lean4:v4.16.0-rc1
lean-machines-examples
Example specifications for the Lean Machines modelling framework
Commit fb8ff21 builds on the recent leanprover/lean4:v4.16.0-rc1
verbose
Natural language tactics to teach mathematics using Lean 4
Commit dd2e6e3 builds on the recent leanprover/lean4:v4.16.0-rc1
mathlib
The math library of Lean 4
Commit 13b16c8 builds on the recent leanprover/lean4:v4.16.0-rc1
NKL
A formalization of the NKI ISA
Commit 4674876 builds on the recent leanprover/lean4:v4.16.0-rc1
SSA
A minimal development of SSA theory
Commit 151cbac builds on the recent leanprover/lean4:v4.16.0-rc1
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 386a3c6 builds on the recent leanprover/lean4:v4.15.0
carleson
A formalized proof of Carleson's theorem in Lean
Commit 0a5a174 builds on the old leanprover/lean4:v4.14.0-rc2
special-numbers
Special Numbers (Chapter 6 from Knuth's Concrete Mathematics)
Commit 03f408f builds on the recent leanprover/lean4:v4.16.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 6be93de builds on the recent leanprover/lean4:v4.16.0-rc1
sadol
Symbolic and Automatic Differentiation of Languages in Lean