Latest Lean Stable:
leanprover/lean4:v4.28.0Reservoir 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 815dd04 builds on the recent leanprover/lean4:v4.29.0-rc6mathlibThe math library of Lean 4
- Commit 3d91ad1 builds on the old leanprover/lean4:v4.20.0analysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.29.0-rc6ryuConverts floating point numbers to decimal strings
- Commit bbecd66 builds on the recent leanprover/lean4:v4.29.0-rc6 after
lake updateLeanCopilotLLMs as Copilots for Theorem Proving in Lean - Commit fd086a7 builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 002a19b builds on the recent leanprover/lean4:v4.28.0FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit c1cdc44 builds on the recent leanprover/lean4:v4.28.0PhysLeanA project to digitalise results from physics into Lean.
- Commit fea2a7c builds on the recent leanprover/lean4:v4.29.0-rc6 after
lake updatepaperproofLean theorem proving interface which feels like pen-and-paper proofs. - Commit 4de9edc builds on the old leanprover/lean4:v4.20.1equational_theoriesA project to map out the relations between different equational theories of Magmas.
- Commit 2bf0e10 builds on the old leanprover/lean4:v4.21.0milThe user home repository for the Mathematics in Lean tutorial.
Newly Created
- Commit ebae19e builds on the recent 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.29.0-rc6LiterateLeanliterate programming for lean4
- Commit 6886b91 builds on the recent leanprover/lean4:v4.28.0shannon-entropyA formalization of Shannon's seminal 1948 paper defining entropy.
- Commit 1c76bd3 builds on the recent leanprover/lean4:v4.29.0-rc6lambdasat-leanFormally 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 recent leanprover/lean4:v4.28.0sensitivityLean 4 formalization of the Sensitivity Conjecture (Huang 2019)
- Commit 9dfee1c builds on the recent leanprover/lean4:v4.28.0LeanServerVerified HTTPS server in Lean 4 — TLS 1.3, HTTP/2, QUIC, WebSocket, gRPC — 914 machine-checked theorems, zero sorry. Pure library available (LeanServerPure).
- Commit aa04b54 builds on the recent leanprover/lean4:v4.28.0Distributed2Coloring2-Coloring Cycles in One Round: Formalization in Lean 4
- Commit 9a61202 builds on the old leanprover/lean4:v4.24.0VelvetAn auto-active verifier embedded into Lean
- Commit 24c8d36 builds on the recent leanprover/lean4:v4.29.0-rc6 after
lake updateamo-leanVerified Optimizing Compiler for Cryptographic Primitives - Commit c3d7547 builds on the recent leanprover/lean4:v4.28.0-rc1OSforGFFA Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
Recently Updated
- Commit 815dd04 builds on the recent leanprover/lean4:v4.29.0-rc6mathlibThe math library of Lean 4
- Commit 8598cb4 builds on the old leanprover/lean4:v4.8.0-rc1 after
lake updateprintiestA pretty printer for Lean 4 - Commit c3d7547 builds on the recent leanprover/lean4:v4.28.0-rc1OSforGFFA Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
- Commit c336170 builds on the recent leanprover/lean4:v4.29.0-rc6aesopWhite-box automation for Lean 4
- Commit e757ea2 builds on the recent leanprover/lean4:v4.28.0PrimeNumberTheoremAndBlueprint for the PNT+ Project
- Commit 3a5bc7a builds on the old leanprover/lean4:v4.25.2sgcLean 4 library characterizing the algebraic structure of metastability and consolidation in stochastic systems
- Commit ab68a1a builds on the recent leanprover/lean4:v4.29.0-rc6VDFormalizing Value Distribution Theory
- Commit ec9f423 builds on the recent leanprover/lean4:v4.28.0BrownianMotionConstruction of a Brownian Motion in Lean
- Commit f63184a builds on the old leanprover/lean4:v4.26.0leanaideTools based on AI for helping with Lean 4
- Commit 02509f4 builds on the old leanprover/lean4:v4.25.2Curve25519DalekVerifying curve25519-dalek using Lean