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 b202b86 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 7be1a35 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 f7c20d3 builds on the recent leanprover/lean4:v4.15.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 74dffd1 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 43bcb19 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 15d646d 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 dcae236 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
Commit c5d60b8 builds on the recent leanprover/lean4:v4.15.0-rc1
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Recently Updated Commit b202b86 builds on the recent leanprover/lean4:v4.15.0-rc1
mathlib
The math library of Lean 4
Commit 9cb42e1 builds on the old leanprover/lean4:v4.13.0
sampcert
SampCert : Verified Differential Privacy
Commit 588a32a builds on the recent leanprover/lean4:v4.15.0-rc1
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 8743a5c builds on the recent leanprover/lean4:v4.15.0-rc1
pumping_cfg
Commit dbb5545 fails to build on leanprover/lean4:v4.15.0-rc1
verso-manual
Commit 59b6839 builds on the recent leanprover/lean4:v4.15.0-rc1
ConNF
A formal consistency proof of Quine's set theory New Foundations
Commit d9f20f5 builds on the old leanprover/lean4:nightly-2023-01-10
yatima
A zero-knowledge Lean4 compiler and kernel
Commit dcae236 fails to build on leanprover/lean4:v4.15.0-rc1
verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Commit 8267c2a builds on the recent leanprover/lean4:v4.15.0-rc1
SSA
A minimal development of SSA theory
Commit 1e87fd7 builds on the recent leanprover/lean4:v4.15.0-rc1
tryAtEachStep
Try a tactic at each step in a Lean proof.