batteries
The "batteries included" extended library for the Lean programming language and theorem prover
of 181 packages depending on leanprover-community/batteries
1-20Sort by
Package Name
adomani/adventsuses
f46c044
Advent of Codelindy-labs/aegisuses
f523fcb
Verify Cairo contracts in Lean 4leanprover-community/aesopuses
v4.19.0-rc2
White-box automation for Lean 4fgdorais/algebrauses
f523fcb
Algebra library for Lean 4FR-vdash-bot/algorithmuses
a84fc2b
Verified efficient algorithms in Lean4.jsm28/AMuses
c509e87
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
v4.17.0
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
80520e5
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
v4.18.0
Formally Verified Arguments of Knowledge in LeanBergschaf/banach_tarskiuses
d2b1546
mseri/BETuses
dc72dcd
Project for "Machine-Checked Mathematics" at the Lorentz Centerfpvandoorn/bonnAnalysisuses
dc4a6b1
repository for the collaborative formalization seminar in Analysis in Bonnsven-manthe/borel_detuses
4f7258c
jaalonso/Calculemus2uses
f523fcb
Proof exercises in Lean4 and Isabelle/HOLjaalonso/Calculemus2_esuses
f007bfe
Ejercicios de demostración con Lean4 e Isabelle/HOL.fpvandoorn/carlesonuses
f523fcb
A formalized proof of Carleson's theorem in Leanknowsys/certifyingDataloguses
v4.17.0
A certified checker for Datalog entailments, written in LeanYaelDillies/ChandraFurstLiptonuses
v4.18.0
Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexitydwrensha/Chessuses
v4.15.0
Chess in Lean 4anlucia/chromatic_polynomialuses
dc167d2
Chromatic polynomial in Lean4