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 84e433e 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 bb71146 builds on the recent leanprover/lean4:v4.34.0-rc2FLTOngoing 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 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
- Commit 6ac1d73 builds on the old leanprover/lean4:v4.33.0eggshellLocal memory for Codex. Reuse work across chats without LLM calls to organize it.
- Commit 38f5a43 builds on the old leanprover/lean4:v4.33.0langlibEsoteric Programming Languages, Formally
- Commit 4e79656 builds on the old leanprover/lean4:v4.33.0FsFormalPalomar-ready Lean formalization of an improved Furstenberg-Sarkozy lower bound
Recently Updated
- Commit 9779958 fails to build on leanprover/lean4:v4.33.1GroupApproximation
- 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 4e1d20f builds on the recent leanprover/lean4:v4.34.0-rc1InfinityCosmosA blueprint for a formalization of infinity-cosmos theory in Lean.
- Commit e636fae 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 24984cb builds on the recent leanprover/lean4:v4.33.1formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit bea16dc builds on the recent leanprover/lean4:v4.34.0VCVioMachine-checked cryptographic proofs in Lean, built on Mathlib: oracle computations, probability semantics, program logic, and lattice- and hash-based schemes.
- Commit 71f031e builds on the recent leanprover/lean4:v4.34.0SFLDevelopment repo for translating Software Foundations to Lean
- Commit 34e0fb3 builds on the old leanprover/lean4:v4.33.0ApportionmentlibFormal verification of apportionment theory.
- Commit 583c61c builds on the old leanprover/lean4:v4.30.0-rc2btc-verifiedVerified Bitcoin protocol components in Lean 4 — serialization, txids, and merkle commitments checked against real mainnet blocks.
- Commit 3746b7b builds on the old leanprover/lean4:v4.25.0tCSlibLean 4 Theoretical Computer Science Library