Displaying 1-20 of 176 packages depending on leanprover-community/plausible
Sort by
  1. b-mehta/ABCExceptionsusesv4.21.0-rc3

    Exceptions to the ABC conjecture in Lean
  2. YaelDillies/AddCombiusesv4.21.0

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

    Verify Cairo contracts in Lean 4
  4. astrainfinita/algorithmusesv4.23.0-rc2

    Verified efficient algorithms in Lean4.
  5. jsm28/AMusesv4.22.0-rc4

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

    tool for turning Lean proofs into Blender animations
  7. FormalizedFormalLogic/arithmetizationusesv4.17.0-rc1

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

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

    A formalized proof of Artin-Wedderburn theorem in Lean4
  10. ctchou/AutomataTheoryusesv4.23.0-rc2

    Automata theory in Lean
  11. eshelyaron/bddusesv4.21.0-rc3

    Binary Decision Diagrams in Lean 4
  12. estradilua/BirkhoffErgodicThmusesv4.20.0-rc2

    A proof of Pointwise Birkhoff Ergodic Theorem in Lean
  13. roos-j/BooleanFunusesv4.16.0-rc1

    Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.
  14. sven-manthe/borel_detusesv4.19.0-rc2

  15. RemyDegenne/BrownianMotionusesv4.22.0-rc4

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

    A formalisation of the Bruhat-Tits tree in Lean4
  17. jaalonso/Calculemus2usesv4.22.0-rc3

    Proof exercises in Lean4 and Isabelle/HOL
  18. jaalonso/Calculemus2_esusesv4.15.0-rc1

    Ejercicios de demostración con Lean4 e Isabelle/HOL.
  19. fpvandoorn/carlesonusesv4.22.0-rc4

    A formalized proof of Carleson's theorem in Lean