Latest Lean Stable:
leanprover/lean4:v4.34.1Reservoir 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 282fbb8 builds on the recent leanprover/lean4:v4.35.0-rc3mathlibThe 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 2c165a0 builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.35.0-rc3ryuConverts floating point numbers to decimal strings
- Commit a303359 builds on the recent leanprover/lean4:v4.34.1LeanCopilotLLMs as Copilots for Theorem Proving in Lean
- Commit df3f12d builds on the recent leanprover/lean4:v4.33.1formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit f6c6a2f builds on the recent leanprover/lean4:v4.35.0-rc3FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit da58032 builds on the recent leanprover/lean4:v4.34.1PhyslibA project to digitalise results from physics into Lean.
- Commit 8c41993 builds on the recent leanprover/lean4:v4.35.0-rc3cslibThe 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 c24e9fc builds on the recent leanprover/lean4:v4.34.0-rc2SpivakCalculusMichael Spivak's Calculus formalized in Lean 4: every theorem and every problem of all 30 chapters and 9 appendices, in both the 3rd and 4th editions
- Commit 4d55691 builds on the recent leanprover/lean4:v4.35.0-rc1MovingSofaAutoformalization of Baek's solution to the moving sofa problem: the Gerver sofa is optimal
- 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 7b5d69c fails to build on leanprover/lean4:v4.34.1JoltBytecodeFormal Verification Of Jolt zk-VM
- Commit 57c142d builds on the recent leanprover/lean4:v4.34.1waterfallSmall, 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).
Recently Updated
- Commit 772f650 builds on the recent leanprover/lean4:v4.35.0-rc3TNLeanTensor-network theory, formalized in Lean 4: the fundamental theorem of matrix product states, canonical forms, parent Hamiltonians, matrix-product density operators, and projected entangled pair states, building on the QICLean quantum-information library
- Commit 2aede42 builds on the old leanprover/lean4:v4.30.0-rc2LiveLeanTriathlon
- Commit d09de25 builds on the old leanprover/lean4:v4.26.0FormalisingMathematics2026Course notes for Formalising Mathematics 2026
- Commit c82f7fd builds on the recent leanprover/lean4:v4.35.0-rc3TauCetiAn AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
- Commit 38f34ff 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 a6d0d94 builds on the recent leanprover/lean4:v4.35.0-rc3HexDevelopment monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex
- Commit 2c165a0 builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 727e4d2 builds on the old leanprover/lean4:v4.31.0 after
lake updateGameNatural Number Game - Commit b1bbb21 builds on the recent leanprover/lean4:v4.34.0-rc2hexVerified computational algebra in Lean 4: aggregator for the released hex libraries
- Commit e520539 builds on the recent leanprover/lean4:v4.34.0lean4-mlirLean specification of neural architectures with verified GPU codegen.