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 b4b5d9c builds on the recent leanprover/lean4:v4.20.0-rc5
mathlib
The math library of Lean 4
Commit 1b09b3a builds on the recent leanprover/lean4:v4.20.0-rc5
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit ed64c74 builds on the recent leanprover/lean4:v4.20.0-rc5
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 2c9cad0 builds on the recent leanprover/lean4:v4.20.0-rc5
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the old leanprover/lean4:v4.15.0
scilean
Scientific computing in Lean 4
Commit 5da0888 builds on the old leanprover/lean4:v4.14.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 78e1181 builds on the recent leanprover/lean4:v4.20.0-rc5
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 9264d54 builds on the recent leanprover/lean4:v4.20.0-rc5
aesop
White-box automation for Lean 4
Commit 731400d builds on the recent leanprover/lean4:v4.20.0-rc5
lean4-metaprogramming-book
Commit 4905eec builds on the recent leanprover/lean4:v4.19.0
PhysLean
A project to digitalise results from physics into Lean.
Newly Created Commit b8d0cec builds on the recent leanprover/lean4:v4.19.0
bruhat-tits
A formalisation of the Bruhat-Tits tree in Lean4
Commit b833cd0 builds on the recent leanprover/lean4:v4.20.0-rc5
LeanPlot
Commit 7d1df03 builds on the recent leanprover/lean4:v4.19.0
logic-formalization
Formalize "Logic Notes" by Lou van den Dries in Lean
Commit de41335 builds on the recent leanprover/lean4:v4.20.0-rc5
rupert
Formalization of the Rupert Problem for convex polyhedra.
Commit 393965a builds on the recent leanprover/lean4:v4.20.0-rc5
groebner
Formalization of Gröbner basis theory in Lean4 (WIP)
Commit 25e29d1 builds on the recent leanprover/lean4:v4.20.0-rc5
kimina
A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
Commit 64de71c builds on the recent leanprover/lean4:v4.20.0-rc5
cryptolib
The cryptography library of Lean 4
Commit 26048ed builds on the recent leanprover/lean4:v4.20.0-rc5
Canonical
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Commit ba62894 builds on the recent leanprover/lean4:v4.20.0-rc5
STIR
SC: Ethereum - zk(E)VM Verification - STIR Lean Blueprint
Commit 7f3bdba builds on the recent leanprover/lean4:v4.20.0-rc5
Iterator
In this repository, I work on the Lean iterator library that is supposed to become part of the standard library.
Recently Updated Commit b4b5d9c builds on the recent leanprover/lean4:v4.20.0-rc5
mathlib
The math library of Lean 4
Commit 5da0888 builds on the old leanprover/lean4:v4.14.0-rc3
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit 2720e10 builds on the recent leanprover/lean4:v4.20.0-rc5
BrownianMotion
Construction of a Brownian Motion in Lean
Commit 4905eec builds on the recent leanprover/lean4:v4.19.0
PhysLean
A project to digitalise results from physics into Lean.
Commit 0d81cbe builds on the recent leanprover/lean4:v4.20.0-rc5
Toric
Formalisation of toric varieties in Lean 4
Commit 78e1181 builds on the recent leanprover/lean4:v4.20.0-rc5
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit f8a573f builds on the recent leanprover/lean4:v4.20.0-rc5
verso
Lean documentation authoring tool
Commit 98b12d9 builds on the recent leanprover/lean4:v4.20.0-rc2
smt
Tactics for discharging Lean goals into SMT solvers.
Commit be80d31 builds on the old leanprover/lean4:v4.18.0
Duper
Commit 13c9ccb builds on the recent leanprover/lean4:v4.19.0-rc2
Seymour
This project is about formally verifying Seymour's decomposition theorem for regular matroids.