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 df255e2 builds on the recent leanprover/lean4:v4.15.0-rc1
mathlib
The math library of Lean 4
Commit 1c84b5b builds on the recent leanprover/lean4:v4.15.0-rc1
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 8216cd9 builds on the recent leanprover/lean4:v4.15.0-rc1
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 466e162 builds on the recent leanprover/lean4:v4.15.0-rc1
scilean
Scientific computing in Lean 4
Commit 8325355 builds on the recent leanprover/lean4:v4.15.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 5fb74b7 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 f007bfe 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 59e4e66 builds on the recent leanprover/lean4:v4.15.0-rc1
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 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 e7147ca builds on the recent leanprover/lean4:v4.15.0-rc1
NodeGraph
Commit 854b051 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 656070c builds on the recent leanprover/lean4:v4.15.0-rc1
borel_det
Commit 30ea6c4 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.
Recently Updated Commit df255e2 builds on the recent leanprover/lean4:v4.15.0-rc1
mathlib
The math library of Lean 4
Commit 22b918e builds on the recent leanprover/lean4:v4.15.0-rc1
verbose
Natural language tactics to teach mathematics using Lean 4
Commit f007bfe 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 84ad8f7 builds on the recent leanprover/lean4:v4.15.0-rc1
aegis
Verify Cairo contracts in Lean 4
Commit 98d13bc builds on the recent leanprover/lean4:v4.15.0-rc1
egg
A (WIP) equality saturation tactic for Lean based on egg.
Commit e898801 builds on the recent leanprover/lean4:v4.15.0-rc1
Lean by Example
プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。
Commit 5fb74b7 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 e1d9b71 builds on the recent leanprover/lean4:v4.15.0-rc1
compfiles
Catalog Of Math Problems Formalized In Lean
Commit 0d7e8b6 builds on the recent leanprover/lean4:v4.15.0-rc1
mdgen
Tool to generate markdown files from lean files.
Commit 3a42110 builds on the recent leanprover/lean4:v4.15.0-rc1
Seymour
This project is about formally verifying Seymour's decomposition theorem for regular matroids.