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 730684c builds on the recent leanprover/lean4:v4.8.0-rc1
mathlib
The math library of Lean 4
Commit b83f1d6 builds on the recent leanprover/lean4:v4.7.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 8ed7a39 builds on the recent leanprover/lean4:v4.8.0-rc1
examples
Lean theorem proving interface which feels like pen-and-paper proofs.
Commit af67d94 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
scilean
Scientific computing in Lean 4
Commit 914ad4f builds on the recent leanprover/lean4:v4.8.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit 4ffaf96 builds on the recent leanprover/lean4:v4.7.0
lean4-metaprogramming-book
Commit de11e0e builds on the recent leanprover/lean4:v4.8.0-rc1
aesop
White-box automation for Lean 4
Commit 80f5638 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
ntptutorial
Tutorial on neural theorem proving
Commit d45a2d3 builds on the recent leanprover/lean4:v4.8.0-rc1
render
A simple raytracer written in Lean 4
Commit 0340787 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
PrimeNumberTheoremAnd
blueprint for prime number theorem and more
Newly Created Commit ac65108 builds on the recent leanprover/lean4:v4.8.0-rc1
Koch
Koch 2D snowflake generator for 4D Golf
Commit 170d71b builds on the recent leanprover/lean4:v4.8.0-rc1
use-lean-standard-action-with-bare-project
Commit 507fb66 builds on the recent leanprover/lean4:v4.8.0-rc1
workshop
Repo for the first BerLean workshop.
Commit aed3615 builds on the recent leanprover/lean4:v4.8.0-rc1
quantumInfo
Quantum information theory in Lean 4
Commit 79dd747 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
bonnAnalysis
repository for the collaborative formalization seminar in Analysis in Bonn
Commit da7882c builds on the recent leanprover/lean4:v4.7.0
Game
Commit 2800f1a builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
llmlean
LLMs + Lean, on your laptop or in the cloud
Commit 0b5119f builds on the recent leanprover/lean4:v4.7.0
leansec
Total parser combinators library for Lean4
Commit d682996 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
LeanLion
Code for Singapore Workshop on Formal Proofs and Lean
Commit f78b1bf builds on the recent leanprover/lean4:v4.8.0-rc1
FLT3
Proof in Lean of Fermat Last Theorem for exponent 3
Recently Updated Commit 730684c builds on the recent leanprover/lean4:v4.8.0-rc1
mathlib
The math library of Lean 4
Commit d16d12c builds on the recent leanprover/lean4:v4.8.0-rc1
vcsp
General-Valued Constraint Satisfaction Problems — playground for experiments preceding my contribution to Mathlib
Commit ca1d756 builds on the recent leanprover/lean4:v4.8.0-rc1
verso
Lean documentation authoring tool
Commit aa1d3c1 builds on the recent leanprover/lean4:v4.8.0-rc1
subverso
Commit f78b1bf builds on the recent leanprover/lean4:v4.8.0-rc1
FLT3
Proof in Lean of Fermat Last Theorem for exponent 3
Commit f06dc4e builds on the recent leanprover/lean4:v4.8.0-rc1
BET
Project for "Machine-Checked Mathematics" at the Lorentz Center
Commit 914ad4f builds on the recent leanprover/lean4:v4.8.0-rc1
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
Commit d45a2d3 builds on the recent leanprover/lean4:v4.8.0-rc1
render
A simple raytracer written in Lean 4
Commit 4e0e53d builds on the recent leanprover/lean4:v4.8.0-rc1
mathport
Mathport is a tool for porting Lean3 projects to Lean4
Commit c2a2c0a builds on the recent leanprover/lean4:v4.7.0
auto
Experiments in automation for Lean