Latest Lean Stable:
leanprover/lean4:v4.30.0-rc2Reservoir 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 dddc142 builds on the recent leanprover/lean4:v4.30.0-rc2mathlibThe math library of Lean 4
- Commit 801fd1b builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.30.0-rc2ryuConverts floating point numbers to decimal strings
- Commit bbecd66 builds on the recent leanprover/lean4:v4.30.0-rc2 after
lake updateLeanCopilotLLMs as Copilots for Theorem Proving in Lean - Commit b78e12e builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 1f76653 builds on the recent leanprover/lean4:v4.30.0-rc2FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit 4ef4cb5 builds on the recent leanprover/lean4:v4.29.1PhyslibA project to digitalise results from physics into Lean.
- Commit c944afd builds on the old leanprover/lean4:v4.29.0-rc8paperproofLean theorem proving interface which feels like pen-and-paper proofs.
- Commit b99c0e4 builds on the old leanprover/lean4:v4.20.1equational_theoriesA project to map out the relations between different equational theories of Magmas.
- Commit f908775 builds on the recent leanprover/lean4:v4.30.0-rc2cslibThe Lean Computer Science Library (CSLib)
Newly Created
- Commit 4305eae builds on the old leanprover/lean4:v4.28.0langlibLibrary for formal language theory in Lean 4
- Commit efaa113 builds on the old leanprover/lean4:v4.28.0FormalQualBench
- Commit 74f0266 builds on the old leanprover/lean4:v4.29.0AlgoleanAlgorithms and Complexity Library using the lightweight query combinator framework called "Prog"
- Commit 9abf4dc builds on the old leanprover/lean4:v4.27.0leslie
- Commit e90c69c builds on the old leanprover/lean4:v4.28.0NormalFormsExecutable Hermite and Smith Normal Forms in Lean 4 over Euclidean Domains, with a PID bridge to mathlib.
- Commit 5088a7b builds on the recent leanprover/lean4:v4.30.0-rc2LiterateLeanliterate programming for lean4
- Commit 18c12de builds on the old leanprover/lean4:v4.28.0CookbookA cookbook for Metaprogramming in Lean4 containing code snippets to help you code!
- Commit 6886b91 builds on the old leanprover/lean4:v4.28.0shannon-entropyA formalization of Shannon's seminal 1948 paper defining entropy.
- Commit 0439a64 builds on the recent leanprover/lean4:v4.30.0-rc2optisatFormally verified equality saturation engine in Lean 4, parameterized by typeclasses. OptiSat provides a domain-agnostic e-graph with 248 theorems
- Commit 9d2cff4 builds on the old leanprover/lean4:v4.28.0sensitivityLean 4 formalization of the Sensitivity Conjecture (Huang 2019)
Recently Updated
- Commit e1d6beb builds on the recent leanprover/lean4:v4.29.1Strata
- Commit 7f8b132 builds on the recent leanprover/lean4:v4.30.0-rc2 after
lake updateEvmAsm - Commit 978ec8a builds on the old leanprover/lean4:v4.29.0iris-leanLean 4 port of Iris, a higher-order concurrent separation logic framework
- Commit 22274a0 builds on the old leanprover/lean4:v4.29.0SpherePackingA Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
- Commit 7d1d823 builds on the old leanprover/lean4:v4.29.0smtTactics for discharging Lean goals into SMT solvers.
- Commit 3bf0d94 builds on the old leanprover/lean4:v4.29.0clapImplementation of the Clap language for ZK Circuits in the Lean proof-assistant
- Commit 801fd1b builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit f908775 builds on the recent leanprover/lean4:v4.30.0-rc2cslibThe Lean Computer Science Library (CSLib)
- Commit 2994616 builds on the old leanprover/lean4:v4.29.0ixa zero-knowledge proof-carrying code platform for Lean 4
- Commit bc67776 builds on the recent leanprover/lean4:v4.30.0-rc2soma-workspace⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.