## batteries

The "batteries included" extended library for the Lean programming language and theorem prover

**1-20**of

**124**packages depending on

**leanprover-community/batteries**

Sort by

Package Name

### lindy-labs/aegisuses

`v4.10.0-rc2`

Verify Cairo contracts in Lean 4### leanprover-community/aesopuses

`fc871f7`

White-box automation for Lean 4### FR-vdash-bot/algorithmuses

`13f9b00`

Verified efficient algorithms in Lean4.### jsm28/AMuses

`2ce0037`

Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)### dwrensha/animateuses

`v4.11.0`

tool for turning Lean proofs into Blender animations### FormalizedFormalLogic/arithmetizationuses

`937cd32`

Formalization of Arithmetization of Mathematics/Metamathematics### mseri/BETuses

`34e690e`

Project for "Machine-Checked Mathematics" at the Lorentz Center### fpvandoorn/bonnAnalysisuses

`dc4a6b1`

repository for the collaborative formalization seminar in Analysis in Bonn### jaalonso/Calculemus2uses

`13f9b00`

Proof exercises in Lean4 and Isabelle/HOL### jaalonso/Calculemus2_esuses

`13f9b00`

Ejercicios de demostraciĆ³n con Lean4 e Isabelle/HOL.### fpvandoorn/carlesonuses

`v4.12.0`

A formalized proof of Carleson's theorem in Lean### knowsys/certifyingDataloguses

`v4.11.0`

A certified checker for Datalog entailments, written in Lean### YaelDillies/ChandraFurstLiptonuses

`46fed98`

Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity### anlucia/chromatic_polynomialuses

`dc167d2`

Chromatic polynomial in Lean4### RemyDegenne/cltuses

`6d5e1c8`

Central limit theorem in Lean### morganfshirley/CommCompuses

`46fed98`

Formalization of communication complexity in Lean### dwrensha/compfilesuses

`daf1ed9`

Catalog Of Math Problems Formalized In Lean### leanprover-community/ConNFuses

`v4.12.0`

A formal consistency proof of Quine's set theory New Foundations### T-Brick/controlflowuses

`v4.8.0`

A control flow graph library for Lean### optsuite/convexuses

`dc4a6b1`