batteries
The "batteries included" extended library for the Lean programming language and theorem prover
of 227 packages depending on leanprover-community/batteries
1-20Sort by
Package Name
b-mehta/ABCExceptionsuses
v4.21.0-rc3
Exceptions to the ABC conjecture in LeanYaelDillies/AddCombiuses
v4.20.0
The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatoricsadomani/adventsuses
f46c044
Advent of Codelindy-labs/aegisuses
78e1181
Verify Cairo contracts in Lean 4leanprover-community/aesopuses
v4.21.0-rc3
White-box automation for Lean 4fgdorais/algebrauses
a684854
Algebra library for Lean 4FR-vdash-bot/algorithmuses
a84fc2b
Verified efficient algorithms in Lean4.jsm28/AMuses
5e6a775
Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)dwrensha/animateuses
v4.18.0
tool for turning Lean proofs into Blender animationsFormalizedFormalLogic/arithmetizationuses
80520e5
Formalization of Arithmetization of Mathematics/MetamathematicsVerified-zkEVM/Arklibuses
v4.21.0-rc3
Formally Verified Arguments of Knowledge in LeanJobPetrovcic/ArtinWedderburnuses
44e2d2e
A formalized proof of Artin-Wedderburn theorem in Lean4Bergschaf/banach_tarskiuses
d2b1546
eshelyaron/bdduses
5e6a775
Binary Decision Diagrams in Lean 4mseri/BETuses
dc72dcd
Project for "Machine-Checked Mathematics" at the Lorentz Centerestradilua/BirkhoffErgodicThmuses
c8a3a7f
A proof of Pointwise Birkhoff Ergodic Theorem in Leanfpvandoorn/bonnAnalysisuses
dc4a6b1
repository for the collaborative formalization seminar in Analysis in Bonnroos-j/BooleanFunuses
v4.16.0-rc2
Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.sven-manthe/borel_detuses
4f7258c
RemyDegenne/BrownianMotionuses
43d0460
Construction of a Brownian Motion in Lean