Latest Lean Stable:
leanprover/lean4:v4.30.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 5027efb builds on the recent leanprover/lean4:v4.31.0-rc1mathlibThe math library of Lean 4
- Commit 5cadde6 builds on the old leanprover/lean4:v4.29.0-rc8AnalysisA Lean companion to Analysis I
- Commit 4c0618b fails to build on leanprover/lean4:v4.31.0-rc1ryuConverts floating point numbers to decimal strings
- Commit bbecd66 builds on the recent leanprover/lean4:v4.30.0 after
lake updateLeanCopilotLLMs as Copilots for Theorem Proving in Lean - Commit 69aa533 builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 05affa1 builds on the recent leanprover/lean4:v4.30.0FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit 696e55b builds on the recent leanprover/lean4:v4.29.1PhyslibA project to digitalise results from physics into Lean.
- Commit 2f677bf builds on the recent leanprover/lean4:v4.31.0-rc1cslibThe Lean Computer Science Library (CSLib)
- Commit f4a4a54 builds on the old leanprover/lean4:v4.28.0milThe user home repository for the Mathematics in Lean tutorial.
- Commit c944afd builds on the old leanprover/lean4:v4.29.0-rc8paperproofLean theorem proving interface which feels like pen-and-paper proofs.
Newly Created
- Commit b1660f7 builds on the recent leanprover/lean4:v4.30.0lean-redisfull feature async redis client for lean 4
- Commit 4b187f4 fails to build on leanprover/lean4:v4.31.0-rc1QuantumLean formalization of the theory of quantum information and quantum computation
- Commit 453f4fe builds on the recent leanprover/lean4:v4.31.0-rc1lean_effLeanEff is a small Lean 4 extensible-effects library
- Commit db6a2ac fails to build on leanprover/lean4:v4.31.0-rc1tamagoCommon EVM smart contracts similar to solady/solmate, formally verified using Tama + Verity
- Commit 2353ea9 builds on the recent leanprover/lean4:v4.30.0detectiveA Lean4 library to formalize and proof-check murder mysteries like Murdle, KnivesOut and Drishyam
- Commit 6805e23 builds on the recent leanprover/lean4:v4.30.0-rc2stage2-judgeThis repository hosts the SAIR Mathematics Distillation Challenge: Equational Theories Stage 2, providing Lean 4 problem sets, judging tools, and submission harnesses for generating machine-checkable proof certificates.
- Commit 0f95cbd fails to build on leanprover/lean4:v4.31.0-rc1VersionControlA repository for participation in the LeanLang for Autonomy Hackathon held from April 17 to May 01, 2026 at Indian Institute of Science, organised by Emergence AI.
- Commit 577e3eb builds on the old leanprover/lean4:v4.24.0CardanoLedgerApiCardano Ledger Api providing the necessary types and predicates to prove Plutus smart contracts with Blaster
- Commit e7049be builds on the old leanprover/lean4:v4.28.0langlibLibrary for formal language theory in Lean 4
- Commit 4c1b307 builds on the old leanprover/lean4:v4.29.0-rc6DeGiorgiLean 4 formalization of De Giorgi-Nash-Moser theory
Recently Updated
- Commit 978ec8a builds on the old leanprover/lean4:v4.29.0iris-leanLean 4 port of Iris, a higher-order concurrent separation logic framework
- Commit 712d164 builds on the recent leanprover/lean4:v4.30.0linglibA Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
- Commit 9f38cfe fails to build on leanprover/lean4:v4.31.0-rc1sumcheck
- Commit 69aa533 builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 428e643 builds on the recent leanprover/lean4:v4.31.0-rc1batteriesThe "batteries included" extended library for the Lean programming language and theorem prover
- Commit 5b918a9 builds on the recent leanprover/lean4:v4.31.0-rc1 after
lake updatelean4-mlirLLM-assisted Lean specification of neural architectures with IREE codegen. - Commit afbff7d builds on the old leanprover/lean4:v4.28.0pdlTableaux for Propositional Dynamic Logic in Lean 4 (WORK IN PROGRESS)
- Commit 67bff1e builds on the old leanprover/lean4:v4.29.0PrimeNumberTheoremAndBlueprint for the PNT+ Project
- Commit eead15f builds on the recent leanprover/lean4:v4.30.0-rc2 after
lake updateEvmAsm - Commit e7049be builds on the old leanprover/lean4:v4.28.0langlibLibrary for formal language theory in Lean 4