leanprover-communityproofwidgets

Helper toolkit for creating your own Lean 4 UserWidgets
Displaying 1-20 of 257 packages depending on leanprover-community/proofwidgets
Sort by

  1. b-mehta/ABCExceptionsusesv0.0.62

    Exceptions to the ABC conjecture in Lean

  2. YaelDillies/AddCombiusesv0.0.68

    The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics

  3. TristanCacqueray/advent-of-leanusesv0.0.23

  4. lindy-labs/aegisusesv0.0.59

    Verify Cairo contracts in Lean 4

  5. b-mehta/AharoniKormanusesv0.0.50

    Disproof of the Aharoni–Korman conjecture

  6. astrainfinita/algorithmusesv0.0.71

    Verified efficient algorithms in Lean4.

  7. jsm28/AMusesv0.0.71

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

  8. dwrensha/animateusesv0.0.62

    tool for turning Lean proofs into Blender animations

  9. FormalizedFormalLogic/arithmetizationusesv0.0.52-pre2

    Formalization of Arithmetization of Mathematics/Metamathematics

  10. Verified-zkEVM/Arklibusesv0.0.68

    Formally Verified Arguments of Knowledge in Lean

  11. JobPetrovcic/ArtinWedderburnusesv0.0.46

    A formalized proof of Artin-Wedderburn theorem in Lean4

  12. ctchou/AutomataTheoryusesv0.0.71

    Automata theory in Lean

  13. Bergschaf/banach_tarskiusesv0.0.39

  14. eshelyaron/bddusesv0.0.71

    Binary Decision Diagrams in Lean 4

  15. mseri/BETusesv0.0.43

    Project for "Machine-Checked Mathematics" at the Lorentz Center

  16. estradilua/BirkhoffErgodicThmusesv0.0.59

    A proof of Pointwise Birkhoff Ergodic Theorem in Lean

  17. fpvandoorn/bonnAnalysisusesv0.0.39

    repository for the collaborative formalization seminar in Analysis in Bonn

  18. roos-j/BooleanFunusesv0.0.50

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

  19. sven-manthe/borel_detusesv0.0.56

  20. RemyDegenne/BrownianMotionusesv0.0.71

    Construction of a Brownian Motion in Lean