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 49f1292 builds on the recent leanprover/lean4:v4.15.0-rc1
mathlib
The math library of Lean 4
Commit f6a3f14 builds on the old leanprover/lean4:v4.11.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit e2b76ee builds on the recent leanprover/lean4:v4.15.0-rc1
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 1ddfae2 builds on the recent leanprover/lean4:v4.14.0-rc3
scilean
Scientific computing in Lean 4
Commit cc6ed6e builds on the recent leanprover/lean4:v4.15.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 2bce504 builds on the recent leanprover/lean4:v4.14.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 9e583ef builds on the recent leanprover/lean4:v4.15.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 3f28838 builds on the old leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit a4a08d9 builds on the recent leanprover/lean4:v4.15.0-rc1
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.15.0-rc1
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit e7147ca builds on the recent leanprover/lean4:v4.15.0-rc1
NodeGraph
Commit f6ad835 builds on the recent leanprover/lean4:v4.15.0-rc1
partial-combinatory-algebras
A Lean 4 formalization of partial combinatory algebras.
Commit 2470c19 builds on the recent leanprover/lean4:v4.15.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.15.0-rc1
order-pq
Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.
Commit d963baa builds on the recent leanprover/lean4:v4.14.0-rc3
borel_det
Commit 3052ee0 fails to build on leanprover/lean4:v4.15.0-rc1
verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Commit 8e5cb8d builds on the recent leanprover/lean4:v4.15.0-rc1
plausible
Commit 8e24b93 builds on the old 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 old leanprover/lean4:v4.13.0-rc4
Seminar
Past contents of Lean Seminars in Bonn
Recently Updated Commit 49f1292 builds on the recent leanprover/lean4:v4.15.0-rc1
mathlib
The math library of Lean 4
Commit b3cbb53 builds on the recent leanprover/lean4:v4.15.0-rc1
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 3a76c82 builds on the recent leanprover/lean4:v4.15.0-rc1
HepLean
A project to digitalise results from high energy physics into Lean.
Commit 93b486a builds on the recent leanprover/lean4:v4.15.0-rc1
egg
A (WIP) equality saturation tactic for Lean based on egg.
Commit 3052ee0 fails to build on leanprover/lean4:v4.15.0-rc1
verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Commit fbfdecb builds on the recent leanprover/lean4:v4.15.0-rc1
LeanCamCombi
Formalisation of the Cambridge Part II and Part III courses Graph Theory, Combinatorics, Extremal and Probabilistic Combinatorics in Lean
Commit 6c97759 builds on the recent leanprover/lean4:v4.15.0-rc1
pumping_cfg
Commit 171ae3e builds on the recent leanprover/lean4:v4.15.0-rc1
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets
Commit 6101a4b builds on the recent leanprover/lean4:v4.15.0-rc1
PrimeNumberTheoremAnd
blueprint for prime number theorem and more
Commit 5c4673a builds on the recent leanprover/lean4:v4.15.0-rc1
Regex