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 6264905 builds on the recent leanprover/lean4:v4.13.0-rc4
mathlib
The math library of Lean 4
Commit 880f820 builds on the old leanprover/lean4:v4.11.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 992c4c8 builds on the recent leanprover/lean4:v4.13.0-rc4
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 0ebfd32 builds on the old leanprover/lean4:v4.11.0-rc2
scilean
Scientific computing in Lean 4
Commit dc72dcd builds on the recent leanprover/lean4:v4.13.0-rc4
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit aded09c builds on the recent leanprover/lean4:v4.13.0-rc4
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit a7fefe8 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit 9ac1294 builds on the recent leanprover/lean4:v4.13.0-rc4
aesop
White-box automation for Lean 4
Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 80f5638 builds on the recent leanprover/lean4:v4.13.0-rc4
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 83e4f2e fails to build on leanprover/lean4:v4.13.0-rc4
borel_det
Commit b5a2fa0 builds on the recent leanprover/lean4:v4.13.0-rc4
plausible
Commit 8e24b93 builds on the recent leanprover/lean4:v4.13.0-rc4
FMCn_Lean
Repositório destinado às práticas de Lean4 da Monitoria de FMCn.
Commit 5ae790f builds on the recent leanprover/lean4:v4.13.0-rc4
Seminar
Past contents of Lean Seminars in Bonn
Commit c5d60b8 builds on the recent leanprover/lean4:v4.13.0-rc4
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Commit b599f66 builds on the recent leanprover/lean4:v4.13.0-rc4
ExFormMathL4
Commit 28fec27 builds on the recent leanprover/lean4:v4.13.0-rc4
LeanCourse
Bonn Lean course for winter 24/25
Commit 8ddda84 builds on the recent leanprover/lean4:v4.13.0-rc4
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit d1d3854 builds on the recent leanprover/lean4:v4.13.0-rc4
TensorLib
A verified tensor library in Lean
Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc4
NewProject
Recently Updated Commit 6264905 builds on the recent leanprover/lean4:v4.13.0-rc4
mathlib
The math library of Lean 4
Commit 6e76106 builds on the recent leanprover/lean4:v4.13.0-rc4
SSA
A minimal development of SSA theory
Commit dc72dcd builds on the recent leanprover/lean4:v4.13.0-rc4
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit d12b9fe builds on the recent leanprover/lean4:v4.13.0-rc4
EulerProducts
An attempt at formalizing facts on Euler products in Lean
Commit ece13c9 builds on the recent leanprover/lean4:v4.13.0-rc4
LeanAPAP
Formalisation of the Kelley-Meka bound on Roth numbers
Commit 016d71a builds on the recent leanprover/lean4:v4.13.0-rc4
Zklib
A Library for Formally Verified Cryptographic Proof Systems
Commit 4221e41 builds on the recent leanprover/lean4:v4.13.0-rc4
AM
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)
Commit 0fc7fb9 builds on the recent leanprover/lean4:v4.13.0-rc4
hep_lean
A project to digitalise results from high energy physics into Lean.
Commit 0fc350a fails to build on leanprover/lean4:v4.13.0-rc4
raylean
Lean4 bindings for raylib
Commit b599f66 builds on the recent leanprover/lean4:v4.13.0-rc4
ExFormMathL4