leanprover-communitymathlib

The math library of Lean 4
Displaying 1-20 of 350 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.27.0

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

  3. smmercuri/adele-ring_locally-compactusescaac5b1

    The proof that the adele ring of a number field is locally compact, formalised in Lean 4.

  4. TristanCacqueray/advent-of-leanusesv4.3.0

  5. lindy-labs/aegisusesv4.20.0-rc5

    Verify Cairo contracts in Lean 4

  6. b-mehta/AharoniKormanuses9db6595

    Disproof of the Aharoni–Korman conjecture

  7. astrainfinita/algorithmusesv4.27.0-rc1

    Verified efficient algorithms in Lean4.

  8. jsm28/AMusesab58ce6

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

  9. dwrensha/animateusesv4.26.0

    tool for turning Lean proofs into Blender animations

  10. YaelDillies/APAPuses507f18f

    Formalisation of the Kelley-Meka bound on Roth numbers

  11. mdbrnowski/Apportionmentlibusesbb46736

    Formal verification of apportionment theory.

  12. misaka10987/archimedesusesv4.25.0-rc2

    Don't disturb my circle!

  13. FormalizedFormalLogic/arithmetizationusesf05ed67

    Formalization of Arithmetization of Mathematics/Metamathematics

  14. Verified-zkEVM/Arklibusesv4.26.0

    Formally Verified Arguments of Knowledge in Lean

  15. GasStationManager/ArtificialAlgorithmsusesv4.26.0

    Verified algorithms in Lean, implemented and proved by AIs

  16. JobPetrovcic/ArtinWedderburnuses7113817

    A formalized proof of Artin-Wedderburn theorem in Lean4

  17. ctchou/AutomataTheoryusesaad2696

    Automata theory in Lean

  18. Bergschaf/banach_tarskiuses15ce681

  19. eshelyaron/bddusesv4.27.0

    Binary Decision Diagrams in Lean 4

  20. mseri/BETuses9227fd8

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