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 3bf558f builds on the recent leanprover/lean4:v4.13.0-rc3
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-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 66ee02b builds on the old leanprover/lean4:v4.11.0-rc2
scilean
Scientific computing in Lean 4
Commit dd6b101 builds on the recent leanprover/lean4:v4.13.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 523aede builds on the recent leanprover/lean4:v4.13.0-rc3
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 b20a886 builds on the recent leanprover/lean4:v4.13.0-rc3
aesop
White-box automation for Lean 4
Commit b10a942 builds on the recent leanprover/lean4:v4.13.0-rc3
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-rc3
ntptutorial
Tutorial on neural theorem proving
Newly Created Commit 36cf0d0 builds on the recent leanprover/lean4:v4.13.0-rc3
LeanSudoku
Playing Sudoku in the Lean 4 proof assistant
Commit deb5895 builds on the recent leanprover/lean4:v4.13.0-rc3
ExFormMathL4
Commit a9062de builds on the recent leanprover/lean4:v4.13.0-rc3
LeanCourse
Bonn Lean course for winter 24/25
Commit b10a942 builds on the recent leanprover/lean4:v4.13.0-rc3
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-rc3
TensorLib
A verified tensor library in Lean
Commit e9e1de6 builds on the recent leanprover/lean4:v4.13.0-rc3
NewProject
Commit 16cd688 builds on the recent leanprover/lean4:v4.13.0-rc3
CommComp
Formalization of communication complexity in Lean
Commit 95d4f48 fails to build on leanprover/lean4:v4.13.0-rc3
rubik
Lean 4 formalization of Rubik's cubes
Commit 1020b88 builds on the recent leanprover/lean4:v4.13.0-rc3
MetaExamples
Examples using MetaProgramming for writing tactics etc.
Commit a8e927a builds on the old leanprover/lean4:v4.11.0-rc2
tutorial
Aeneas tutorial for ICFP
Recently Updated Commit 3bf558f builds on the recent leanprover/lean4:v4.13.0-rc3
mathlib
The math library of Lean 4
Commit e693406 builds on the recent leanprover/lean4:v4.13.0-rc3
verso
Lean documentation authoring tool
Commit bca30ea builds on the recent leanprover/lean4:v4.13.0-rc3
hep_lean
A project to digitalise results from high energy physics into Lean.
Commit b10a942 builds on the recent leanprover/lean4:v4.13.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 523aede builds on the recent leanprover/lean4:v4.13.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit a6972eb builds on the old leanprover/lean4:v4.7.0
Http
🌐 | HTTP primitives for Lean 4
Commit 290cd85 builds on the recent leanprover/lean4:v4.13.0-rc3
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 843e524 builds on the old leanprover/lean4:v4.10.0
test
SF.lean勉強会でigrepが書いたコードの記録
Commit 2393bfa builds on the recent leanprover/lean4:v4.13.0-rc3
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 9ff67d6 builds on the recent leanprover/lean4:v4.13.0-rc3
FormalBook
Formalizing "Proofs from THE BOOK"