No results found

doc-gen4

Document Generator for Lean 4
Displaying 1-20 of 38 packages depending on leanprover/doc-gen4
Sort by

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

    Verified efficient algorithms in Lean4.

  2. Bergschaf/banach_tarskiusesb941c42

  3. fpvandoorn/bonnAnalysisuses194403b

    repository for the collaborative formalization seminar in Analysis in Bonn

  4. morganfshirley/CommCompuses1b0072f

    Formalization of communication complexity in Lean

  5. leanprover-community/ConNFusesv4.19.0-rc2

    A formal consistency proof of Quine's set theory New Foundations

  6. Shreyas4991/DGAlgorithmsusesv4.16.0

    Distributed Graph Algorithms in Lean

  7. teorth/equational_theoriesuses059eb7e

    A project to map out the relations between different equational theories of Magmas.

  8. teorth/expdbusesv4.19.0-rc2

    Exponent pair database

  9. ivankobe/FactorizationSystemsuses059eb7e

  10. leanprover-community/flt-regularusesv4.19.0-rc2

    Fermat's Last Theorem for regular primes

  11. riccardobrasca/flt-regularusesv4.18.0-rc1

    Proof of Kaplanski criterion for being a UFD in Lean4

  12. mo271/FormalBookuses7b6a56e

    Formalizing "Proofs from THE BOOK"

  13. emilyriehl/InfinityCosmosusesv4.18.0-rc1

    A blueprint for a formalization of infinity-cosmos theory in Lean.

  14. SchrodingerZhu/lean-gccjituses649e779

    libgccjit bindings for Lean4

  15. Bergschaf/LeanBanachTarskiusese3f8a87

  16. utensil/LeanBlueprintExampleusesf9d9875

  17. fpvandoorn/LeanCourseusesv4.13.0-rc1

    Bonn Lean course for winter 24/25

  18. Bergschaf/leroyusesv4.18.0-rc1

  19. loganrjmurphy/libusesb334278

    LeanEuclid is a benchmark for autoformalization in the domain of Euclidean geometry, targeting the proof assistant Lean.

  20. leanprover/lnsymusesd36b7fd

    Armv8 Native Code Symbolic Simulator in Lean