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

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

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

    Verify Cairo contracts in Lean 4
  4. b-mehta/AharoniKormanuses9db6595

    Disproof of the Aharoni–Korman conjecture
  5. astrainfinita/algorithmusesv4.23.0-rc2

    Verified efficient algorithms in Lean4.
  6. jsm28/AMusesb457494

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

    tool for turning Lean proofs into Blender animations
  8. FormalizedFormalLogic/arithmetizationusesf05ed67

    Formalization of Arithmetization of Mathematics/Metamathematics
  9. Verified-zkEVM/Arklibusesv4.22.0

    Formally Verified Arguments of Knowledge in Lean
  10. JobPetrovcic/ArtinWedderburnuses7113817

    A formalized proof of Artin-Wedderburn theorem in Lean4
  11. ctchou/AutomataTheoryusesaf83bb0

    Automata theory in Lean
  12. eshelyaron/bddusesv4.23.0-rc2

    Binary Decision Diagrams in Lean 4
  13. mseri/BETuses0a0178f

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

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

    repository for the collaborative formalization seminar in Analysis in Bonn
  16. roos-j/BooleanFunusescbbe71d

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

    Construction of a Brownian Motion in Lean