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 5ce203e builds on the recent leanprover/lean4:v4.34.0-rc2mathlibThe math library of Lean 4
- Commit 2351317 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 94769d6 builds on the recent leanprover/lean4:v4.33.1formal_conjecturesA collection of formalized statements of conjectures in Lean.
- Commit 79af205 builds on the recent leanprover/lean4:v4.34.0-rc2FLTOngoing Lean formalisation of the proof of Fermat's Last Theorem
- Commit f6d7fe3 builds on the recent leanprover/lean4:v4.33.0PhyslibA project to digitalise results from physics into Lean.
- Commit 188072b builds on the recent leanprover/lean4:v4.34.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.
- Commit e5a88a1 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 61c3f56 builds on the recent leanprover/lean4:v4.33.1LeanFrontierA Lean 4 library of machine-generated, kernel-verified mathematics.
- Commit 1ddea92 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 6622b51 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 0aa1e08 builds on the recent leanprover/lean4:v4.33.1linglibA Lean 4 library for formal linguistics: semantics, syntax, pragmatics, morphology, phonology, and processing — formalized across competing frameworks for high interconnection density.
- Commit 3558cf2 builds on the recent leanprover/lean4:v4.34.0-rc2verso-manualThe Lean reference manual
- Commit 8088208 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 6f464a2 builds on the recent leanprover/lean4:v4.32.2formal-sltMachine-checked statistical learning theory in Lean 4: empirical-Bernstein and time-uniform PAC-Bayes, Markov risk, Rademacher/VC, and Dudley chaining.
- Commit b113044 builds on the recent leanprover/lean4:v4.34.0-rc2HexDevelopment monorepo for Hex: verified computational algebra in Lean 4 (polynomial factoring, LLL, and friends). Released aggregate: https://github.com/leanprover/hex
- Commit 9be0358 builds on the recent leanprover/lean4:v4.32.2lean4-mlirLean specification of neural architectures with verified GPU codegen.
- Commit bad3de9 builds on the old leanprover/lean4:v4.32.0SpherePackingA Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
- Commit a5fc584 builds on the recent leanprover/lean4:v4.34.0-rc1beamClaude/Codex skill and local workflow layer for efficient interaction with Lean 4 and Monte-Carlo Tree Search.
- Commit cee1a84 builds on the recent leanprover/lean4:v4.34.0-rc2AddCombiThe sublibrary of Mathlib dedicated to additive combinatorics