Reservoir 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 f541cd9 builds on the recent leanprover/lean4:v4.21.0-rc3
mathlib
The math library of Lean 4
Commit 2b2d590 builds on the recent leanprover/lean4:v4.21.0-rc3
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 8624132 builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 7fc314d builds on the recent leanprover/lean4:v4.21.0-rc3
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 902b97d builds on the recent leanprover/lean4:v4.21.0-rc3
paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
scilean
Scientific computing in Lean 4
Commit f1ba144 builds on the recent leanprover/lean4:v4.20.1
equational_theories
A project to map out the relations between different equational theories of Magmas.
Commit d12fdad builds on the recent leanprover/lean4:v4.21.0-rc3
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 1b1abe6 builds on the recent leanprover/lean4:v4.21.0-rc3
aesop
White-box automation for Lean 4
Newly Created Commit b1b92c7 builds on the recent leanprover/lean4:v4.21.0-rc3
cslib
Lean library for Computer Science
Commit 98153df fails to build on leanprover/lean4:v4.21.0-rc3
tactic-programming-beginner-guide
Beginner's guide to Tactic Programming in Lean
Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
analysis
A Lean companion to Analysis I
Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
Lie
A classification theorem in Lean of solvable Lie algebras of dimension zero to three
Commit 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
mini-redis
An implementation of mini-redis in Lean 4
Commit 7351fae builds on the old leanprover/lean4:v4.18.0
verina
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Commit 9f0f43c builds on the recent leanprover/lean4:v4.21.0-rc3
SemicircleLaw
Formalization of Wigner's Semicircle Law in Lean
Commit 7087b15 fails to build on leanprover/lean4:v4.21.0-rc3
lie-classification
Classification of Lie algebras in Lean
Commit 8624132 builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit b8d0cec builds on the old leanprover/lean4:v4.19.0
bruhat-tits
A formalisation of the Bruhat-Tits tree in Lean4
Recently Updated Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
SSA
A minimal development of SSA theory
Commit 8624132 builds on the old leanprover/lean4:v4.17.0
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Commit 528ee45 builds on the recent leanprover/lean4:v4.20.1
Clean
Lean circuit DSL
Commit 3df8b7c builds on the recent leanprover/lean4:v4.21.0-rc3
Heights
An attempt at formalizing the theory of heights in Lean
Commit 4e76d20 builds on the recent leanprover/lean4:v4.20.0
PrimeNumberTheoremAnd
blueprint for prime number theorem and more
Commit e08b4a8 builds on the recent leanprover/lean4:v4.21.0-rc3
veil
A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.
Commit 76be179 builds on the recent leanprover/lean4:v4.21.0-rc3
verso
Lean documentation authoring tool
Commit f541cd9 builds on the recent leanprover/lean4:v4.21.0-rc3
mathlib
The math library of Lean 4
Commit 99ffeee builds on the old leanprover/lean4:v4.18.0
ix
a zero-knowledge proof-carrying code platform for Lean 4
Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
KLR
A formalization of ML kernel languages