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 3b462da 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 14f2585 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 ca76287 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 343197d 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 768a134 builds on the recent leanprover/lean4:v4.8.0-rc1
FLT3
Proof in Lean of Fermat Last Theorem for exponent 3
Recently Updated Commit 41e16d8 builds on the recent leanprover/lean4:v4.8.0-rc1
flt-regular
Fermat's Last Theorem for regular primes
Commit 3b462da builds on the recent leanprover/lean4:v4.8.0-rc1
mathlib
The math library of Lean 4
Commit 1428bd0 builds on the recent leanprover/lean4:v4.7.0
verso
Lean documentation authoring tool
Commit 0538403 builds on the recent leanprover/lean4:v4.8.0-rc1 after lake update
vcsp
General-Valued Constraint Satisfaction Problems — playground for experiments preceding my contribution to Mathlib
Commit daac07d builds on the recent leanprover/lean4:v4.7.0
subverso
Commit 14f2585 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 3acd391 builds on the recent leanprover/lean4:v4.8.0-rc1
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Commit 4a7e255 builds on the recent leanprover/lean4:v4.8.0-rc1
mathport
Mathport is a tool for porting Lean3 projects to Lean4
Commit b83f1d6 builds on the recent leanprover/lean4:v4.7.0
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Commit 1b702d2 builds on the recent leanprover/lean4:v4.8.0-rc1
proofwidgets
Helper toolkit for creating your own Lean 4 UserWidgets