Displaying 1-20 of 339 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.85

    The (currently unofficial) sublibrary of Mathlib dedicated to additive combinatorics
  3. smmercuri/adele-ring_locally-compactusesv0.0.40

    The proof that the adele ring of a number field is locally compact, formalised in Lean 4.
  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.84

    Verified efficient algorithms in Lean4.
  7. jsm28/AMusesv0.0.88

    Lean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)
  8. dwrensha/animateusesv0.0.83

    tool for turning Lean proofs into Blender animations
  9. YaelDillies/APAPusesv0.0.86

    Formalisation of the Kelley-Meka bound on Roth numbers
  10. mdbrnowski/Apportionmentlibusesv0.0.87

    Formal verification of apportionment theory.
  11. misaka10987/archimedesusesv0.0.77

    Don't disturb my circle!
  12. FormalizedFormalLogic/arithmetizationusesv0.0.52-pre2

    Formalization of Arithmetization of Mathematics/Metamathematics
  13. Verified-zkEVM/Arklibusesv0.0.83

    Formally Verified Arguments of Knowledge in Lean
  14. GasStationManager/ArtificialAlgorithmsusesv0.0.83

    Verified algorithms in Lean, implemented and proved by AIs
  15. JobPetrovcic/ArtinWedderburnusesv0.0.46

    A formalized proof of Artin-Wedderburn theorem in Lean4
  16. ctchou/AutomataTheoryusesv0.0.74

    Automata theory in Lean
  17. eshelyaron/bddusesv0.0.85

    Binary Decision Diagrams in Lean 4
  18. mseri/BETusesv0.0.86

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