Latest Lean Stable:
leanprover/lean4:v4.34.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 83b9f16 builds on the recent leanprover/lean4:v4.35.0-rc1mathlibThe math library of Lean 4
- Commit f9e8bc5 builds on the recent leanprover/lean4:v4.34.0-rc2NavierStokesAndEulerLean certificates accompanying Navier-Stokes and Euler results
- Commit 245b2e1 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.0ryuConverts floating point numbers to decimal strings
- Commit a303359 builds on the recent leanprover/lean4:v4.34.0LeanCopilotLLMs as Copilots for Theorem Proving in Lean
- Commit 24984cb builds on the recent leanprover/lean4:v4.33.1formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 4342055 builds on the recent leanprover/lean4:v4.34.0FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit 891d597 builds on the old leanprover/lean4:v4.33.0PhyslibA project to digitalise results from physics into Lean.
- Commit 41094e5 builds on the recent leanprover/lean4:v4.35.0-rc2cslibThe 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.
Newly Created
- Commit 035e9b0 fails to build on leanprover/lean4:v4.34.0nsLeanLean 4 proof that Naslund's Conjecture 13 fails at q = 3: square-difference-free subsets of F_3[T] past 3^(3n/4)
- Commit c0a7d9f fails to build on leanprover/lean4:v4.34.0xRayLeanLean proofs of constructive binary X-ray families, counting bounds, and an extension theorem
- Commit c235f7c builds on the recent leanprover/lean4:v4.34.0waterfallSmall, configurable proof search for inductive Lean goals
- Commit f9e8bc5 builds on the recent leanprover/lean4:v4.34.0-rc2NavierStokesAndEulerLean certificates accompanying Navier-Stokes and Euler results
- Commit a26427e builds on the old leanprover/lean4:v4.32.0-rc1kakeya
- Commit 9ecf082 builds on the old leanprover/lean4:v4.30.0pcfAlephOmega4A Lean 4 formalization of the PCF bound 2^aleph_omega < aleph_(omega_4) under the strong-limit hypothesis.
- Commit 09b97db builds on the old leanprover/lean4:v4.33.0-rc1goldbachA Lean 4 formalization of Chen's theorem (Goldbach 1+2).
- Commit c02708a builds on the old leanprover/lean4:v4.28.0Erdos548Lean 4 Erdős problem #548 (Erdős–Sós conjecture): proof, found by GPT-6 Astra in the FrontierMath Erdős benchmark
- Commit ed6ab14 builds on the recent leanprover/lean4:v4.34.0-rc2dLean
- Commit 0296972 fails to build on leanprover/lean4:v4.34.0-rc2LocalComplexGeometryFoundational theorems in local complex-analytic geometry formalized in Lean 4
Recently Updated
- Commit cad9de3 builds on the recent leanprover/lean4:v4.34.0-rc2TauCetiAn AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
- Commit 1aec8a7 builds on the old leanprover/lean4:v4.29.1equational_theoriesA project to map out the relations between different equational theories of Magmas.
- Commit 7d02726 builds on the recent leanprover/lean4:v4.34.0PolyFunLean 4 library for polynomial functors, interaction trees, and frameworks for modeling interactive and effectful protocols
- Commit b364d45 builds on the recent leanprover/lean4:v4.34.0linglibA Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
- Commit c235f7c builds on the recent leanprover/lean4:v4.34.0waterfallSmall, configurable proof search for inductive Lean goals
- Commit 83b9f16 builds on the recent leanprover/lean4:v4.35.0-rc1mathlibThe math library of Lean 4
- Commit 41094e5 builds on the recent leanprover/lean4:v4.35.0-rc2cslibThe Lean Computer Science Library (CSLib)
- Commit 0803c2f builds on the old leanprover/lean4:v4.33.0PrimeCertFormal prime certificates in Lean 4
- Commit 66b3ce5 builds on the old leanprover/lean4:v4.18.0verinaVerina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
- Commit 6eee2ec builds on the recent leanprover/lean4:v4.34.0sparkleA type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.