No results found

Qq

Intuitive, type-safe expression quotations for Lean 4.
Displaying 1-20 of 221 packages depending on leanprover-community/Qq
Sort by

  1. b-mehta/ABCExceptionsusesv4.21.0-rc3

    Exceptions to the ABC conjecture in Lean

  2. YaelDillies/AddCombiusesv4.20.0

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

  3. TristanCacqueray/advent-of-leanusesd3a1d25

  4. lindy-labs/aegisusesv4.20.0-rc2

    Verify Cairo contracts in Lean 4

  5. FR-vdash-bot/algorithmusesv4.19.0-rc2

    Verified efficient algorithms in Lean4.

  6. jsm28/AMusesv4.20.0-rc2

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

  7. dwrensha/animateusesv4.18.0

    tool for turning Lean proofs into Blender animations

  8. FormalizedFormalLogic/arithmetizationusesv4.17.0-rc1

    Formalization of Arithmetization of Mathematics/Metamathematics

  9. Verified-zkEVM/Arklibusesv4.21.0-rc3

    Formally Verified Arguments of Knowledge in Lean

  10. Bergschaf/banach_tarskiuses01ad339

  11. eshelyaron/bddusesv4.20.0-rc2

    Binary Decision Diagrams in Lean 4

  12. mseri/BETuses1357f4f

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

  13. estradilua/BirkhoffErgodicThmusesv4.20.0-rc2

    A proof of Pointwise Birkhoff Ergodic Theorem in Lean

  14. fpvandoorn/bonnAnalysisusesa7bfa63

    repository for the collaborative formalization seminar in Analysis in Bonn

  15. roos-j/BooleanFunusesv4.15.0

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

  16. sven-manthe/borel_detusesv4.19.0-rc2

  17. RemyDegenne/BrownianMotionusesv4.21.0-rc3

    Construction of a Brownian Motion in Lean

  18. chrisflav/bruhat-titsusesv4.19.0

    A formalisation of the Bruhat-Tits tree in Lean4

  19. RikHeurter/BscThesisFormalisationusesv4.19.0-rc2

  20. jaalonso/Calculemus2usesv4.20.0-rc2

    Proof exercises in Lean4 and Isabelle/HOL