Displaying 1-20 of 216 packages depending on leanprover-community/batteries
Sort by
  1. b-mehta/ABCExceptionsusesv4.21.0-rc1

    Exceptions to the ABC conjecture in Lean
  2. adomani/adventsusesf46c044

    Advent of Code
  3. lindy-labs/aegisuses78e1181

    Verify Cairo contracts in Lean 4
  4. leanprover-community/aesopusesv4.21.0-rc3

    White-box automation for Lean 4
  5. fgdorais/algebrausesv4.20.0

    Algebra library for Lean 4
  6. FR-vdash-bot/algorithmusesa84fc2b

    Verified efficient algorithms in Lean4.
  7. jsm28/AMuses9207957

    Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)
  8. teorth/analysisusesv4.20.0

    A Lean companion to Analysis I
  9. dwrensha/animateusesv4.18.0

    tool for turning Lean proofs into Blender animations
  10. FormalizedFormalLogic/arithmetizationuses80520e5

    Formalization of Arithmetization of Mathematics/Metamathematics
  11. Verified-zkEVM/Arklibusesv4.21.0-rc3

    Formally Verified Arguments of Knowledge in Lean
  12. eshelyaron/bdduses233a67f

    Binary Decision Diagrams in Lean 4
  13. mseri/BETusesdc72dcd

    Project for "Machine-Checked Mathematics" at the Lorentz Center
  14. estradilua/BirkhoffErgodicThmusesc8a3a7f

    A proof of Pointwise Birkhoff Ergodic Theorem in Lean
  15. fpvandoorn/bonnAnalysisusesdc4a6b1

    repository for the collaborative formalization seminar in Analysis in Bonn
  16. roos-j/BooleanFunusesv4.16.0-rc2

    Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.
  17. RemyDegenne/BrownianMotionusesv4.21.0-rc2

    Construction of a Brownian Motion in Lean
  18. chrisflav/bruhat-titsusesv4.19.0

    A formalisation of the Bruhat-Tits tree in Lean4