Latest Lean Stable:
leanprover/lean4:v4.32.2Reservoir 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 375d54d builds on the recent leanprover/lean4:v4.33.0-rc1mathlibThe math library of Lean 4
- Commit 6afb3e3 builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.33.0-rc1ryuConverts floating point numbers to decimal strings
- Commit 2458f73 builds on the recent leanprover/lean4:v4.33.0-rc1 after
lake updateLeanCopilotLLMs as Copilots for Theorem Proving in Lean - Commit 85f8637 builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 2ab8ff6 builds on the recent leanprover/lean4:v4.33.0-rc1FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit 6565c07 builds on the recent leanprover/lean4:v4.32.0PhyslibA project to digitalise results from physics into Lean.
- Commit 81a3ad8 builds on the recent leanprover/lean4:v4.33.0-rc1cslibThe Lean Computer Science Library (CSLib)
- Commit dd6d752 builds on the old leanprover/lean4:v4.30.0milThe user home repository for the Mathematics in Lean tutorial.
- Commit 7e276a2 builds on the old leanprover/lean4:v4.29.1equational_theoriesA project to map out the relations between different equational theories of Magmas.
Newly Created
- Commit a4ca5ad fails to build on leanprover/lean4:v4.32.1Calculus_21An Universe for Mitar —— Classical Calculus
- Commit f8a851a builds on the recent leanprover/lean4:v4.32.2proofnet-irVerified proof-geometry IR experiments for AI-guided theorem proving in Lean 4
- Commit a2fc5bd fails to build on leanprover/lean4:v4.32.1ProbabilityApproximationLean 4 and Mathlib formalization of nonuniform Berry–Esseen bounds and Bentkus's multivariate Gaussian approximation over convex sets.
- Commit 8f2ee54 builds on the recent leanprover/lean4:v4.32.0pacioliA verified core of accounting mechanics in Lean 4, paired with curated accounting judgment in the Open Knowledge Format (OKF).
- Commit 7f3b754 builds on the old leanprover/lean4:v4.31.0domain-theoryA Lean Library for Domain Theory
- Commit 0291784 fails to build on leanprover/lean4:v4.32.1SHSLibStochastic Hybrid Systems core definitions formalized in Lean
- Commit c196b63 fails to build on leanprover/lean4:v4.32.1SeibergWittenThe Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions
- Commit 0a4ec3a builds on the recent leanprover/lean4:v4.33.0-rc1Quantum4LeanVerified quantum computing in Lean 4 with FFI bridge to Apple Silicon (Metal 3). Full NISQ stack, dependent types, formal circuit verification, and mathematical translators to Hamiltonians for autonomous AI.
- Commit 7998024 builds on the old leanprover/lean4:v4.31.0lean-linqType-safe, deeply-embedded SQL query DSL for Lean 4 — LINQ-style pipelines and query! comprehensions compiling to parameterized SQL for SQLite, PostgreSQL, and SQL Server
- Commit fb9c583 builds on the old leanprover/lean4:v4.29.1SafeVerifyLeanstral's fork of SafeVerify, which we use for code agent training and as part of our evaluation stack.
Recently Updated
- Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after
lake updateEvmAsm - Commit a50233d builds on the recent leanprover/lean4:v4.33.0-rc1PrimeCertFormal prime certificates in Lean 4
- Commit 3db6bba builds on the recent leanprover/lean4:v4.33.0-rc1TauCetiAn AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
- Commit 9607a14 builds on the recent leanprover/lean4:v4.32.0TNLeanLean 4 formalization of the Fundamental Theorem of Matrix Product States (arXiv:2011.12127)
- Commit 5f9eadf builds on the old leanprover/lean4:v4.31.0 after
lake updateapc-optimizer - Commit 2964499 builds on the recent leanprover/lean4:v4.32.0PolyFunLean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols
- Commit 1925179 builds on the recent leanprover/lean4:v4.32.0VCVioA Lean library for machine-checked cryptographic proofs.
- Commit 4f38fcb builds on the old leanprover/lean4:v4.27.0BHigher-order encoder for B proof obligations to SMT-LIB 2.7
- Commit a3d8c67 fails to build on leanprover/lean4:v4.33.0-rc1GameTheoryFormalization of Game Theory in Lean4
- Commit cfbdccd builds on the recent leanprover/lean4:v4.32.0lean4-mlirLean specification of neural architectures with verified IREE codegen.