Latest Lean Stable:
leanprover/lean4:v4.33.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 abec794 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 9f5ee77 builds on the old leanprover/lean4:v4.27.0formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 071d16b builds on the recent leanprover/lean4:v4.34.0-rc1FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit 476d92a builds on the recent leanprover/lean4:v4.33.0PhyslibA project to digitalise results from physics into Lean.
- Commit 809bb39 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 4e4c28d builds on the recent leanprover/lean4:v4.33.0-rc1LeanFrontierA Lean 4 library of machine-generated, kernel-verified mathematics.
- Commit d2230ee builds on the recent leanprover/lean4:v4.34.0-rc1sendov
- 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 f53f842 builds on the recent leanprover/lean4:v4.32.1SumDiffProof
- 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
Recently Updated
- Commit c9b2273 builds on the recent leanprover/lean4:v4.34.0-rc1Blake3Lean4 bindings to Blake3
- Commit 365531d 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 abec794 builds on the recent leanprover/lean4:v4.34.0-rc1mathlibThe math library of Lean 4
- Commit ed29cc9 builds on the recent leanprover/lean4:v4.34.0-rc1TNLeanTensor-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 eead15f builds on the old leanprover/lean4:v4.30.0-rc2 after
lake updateEvmAsm - Commit 476d92a builds on the recent leanprover/lean4:v4.33.0PhyslibA project to digitalise results from physics into Lean.
- Commit 809bb39 builds on the recent leanprover/lean4:v4.34.0-rc1cslibThe Lean Computer Science Library (CSLib)
- Commit 07da422 builds on the old leanprover/lean4:v4.5.0formalising-mathematics-2024Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
- Commit 071d16b builds on the recent leanprover/lean4:v4.34.0-rc1FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit d57c8e1 builds on the old leanprover/lean4:v4.31.0ArklibFormally Verified Arguments of Knowledge in Lean