Latest Lean Stable:
leanprover/lean4:v4.33.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 ffa6ef0 builds on the recent leanprover/lean4:v4.34.0-rc1mathlibThe math library of Lean 4
- Commit 8f9e0fc builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.34.0-rc1ryuConverts floating point numbers to decimal strings
- Commit 2458f73 builds on the recent leanprover/lean4:v4.34.0-rc1 after
lake updateLeanCopilotLLMs as Copilots for Theorem Proving in Lean - Commit 4010c1f builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit e99f167 builds on the recent leanprover/lean4:v4.34.0-rc1FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit ef9a592 builds on the recent leanprover/lean4:v4.33.0PhyslibA project to digitalise results from physics into Lean.
- Commit f5c73b0 builds on the recent leanprover/lean4:v4.34.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 54edcda 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 0d2b3b5 builds on the recent leanprover/lean4:v4.32.1gonzalgoWrite out the declaration graph of a Lean environment, statement dependencies kept apart from proof dependencies, so you can find what a theorem actually rests on.
- Commit 4d305b9 builds on the recent leanprover/lean4:v4.32.1lean-teeLean-specified zkTEE: measured guest execution, hashed receipts, lean-grpc APIs
- Commit 0887548 builds on the recent leanprover/lean4:v4.32.1lean-grpcPure Lean 4 gRPC stack (HTTP/2 + HPACK + gRPC) on Std.Async
- Commit 07ed6f9 builds on the recent leanprover/lean4:v4.33.0-rc1AutoGeneralizationKernel-checked theorem generalization for Lean
- 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 c789440 builds on the recent leanprover/lean4:v4.33.0-rc1descriptive-complexityDescriptive complexity in Lean 4: machine-model-free NP-completeness via first-order reductions, and the polynomial hierarchy via second-order alternation
- 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 old 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 5c667c3 builds on the recent leanprover/lean4:v4.32.2domain-theoryA Lean Library for Domain Theory
Recently Updated
- Commit eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after
lake updateEvmAsm - Commit 2f0965a builds on the recent leanprover/lean4:v4.33.0-rc1OSforGFFA Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms
- Commit af390ae builds on the old leanprover/lean4:v4.23.0TensorLibA verified tensor library in Lean
- Commit 293ba18 builds on the old leanprover/lean4:v4.24.0-rc1 after
lake updatelean-machinesa Lean4 framework for the modeling and refinement of stateful systems - Commit 9ea9174 builds on the recent leanprover/lean4:v4.33.0-rc1foamgeometry of hospitality
- Commit 70c3d23 builds on the recent leanprover/lean4:v4.34.0-rc1TauCetiAn AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
- Commit 4cb02d4 builds on the recent leanprover/lean4:v4.33.0linglibA Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
- Commit 11cf8f4 builds on the old leanprover/lean4:v4.30.0-rc2GraphLibThis is the repository for graph algorithm design.
- Commit bd78196 builds on the old leanprover/lean4:v4.29.1ixa zero-knowledge proof-carrying code platform for Lean 4
- Commit 978ec8a builds on the old leanprover/lean4:v4.29.0iris-leanLean 4 port of Iris, a higher-order concurrent separation logic framework