Displaying 1-20 of 176 packages depending on leanprover-community/LeanSearchClient
Sort by
  1. b-mehta/ABCExceptionsuses6c62474

    Exceptions to the ABC conjecture in Lean
  2. YaelDillies/AddCombiuses6c62474

    The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics
  3. lindy-labs/aegisuses2507836

    Verify Cairo contracts in Lean 4
  4. FR-vdash-bot/algorithmuses8d29bc2

    Verified efficient algorithms in Lean4.
  5. jsm28/AMuses6c62474

    Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)
  6. dwrensha/animateuses6c62474

    tool for turning Lean proofs into Blender animations
  7. FormalizedFormalLogic/arithmetizationuses0c169a0

    Formalization of Arithmetization of Mathematics/Metamathematics
  8. Verified-zkEVM/Arklibuses6c62474

    Formally Verified Arguments of Knowledge in Lean
  9. JobPetrovcic/ArtinWedderburnusesd7caecc

    A formalized proof of Artin-Wedderburn theorem in Lean4
  10. eshelyaron/bdduses6c62474

    Binary Decision Diagrams in Lean 4
  11. mseri/BETuses7bedaed

    Project for "Machine-Checked Mathematics" at the Lorentz Center
  12. estradilua/BirkhoffErgodicThmuses2507836

    A proof of Pointwise Birkhoff Ergodic Theorem in Lean
  13. roos-j/BooleanFunuses003ff45

    Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.
  14. RemyDegenne/BrownianMotionuses6c62474

    Construction of a Brownian Motion in Lean
  15. chrisflav/bruhat-titsuses2507836

    A formalisation of the Bruhat-Tits tree in Lean4
  16. jaalonso/Calculemus2uses6c62474

    Proof exercises in Lean4 and Isabelle/HOL
  17. jaalonso/Calculemus2_esuses003ff45

    Ejercicios de demostración con Lean4 e Isabelle/HOL.
  18. fpvandoorn/carlesonuses6c62474

    A formalized proof of Carleson's theorem in Lean