No results found

mathlib

The math library of Lean 4
Sort by
  1. Registry dependency.
    Found on Reservoir.

    plausiblev4.17.0-rc1

  2. Registry dependency.
    Found on Reservoir.

    LeanSearchClient0c169a0

    Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
  3. Registry dependency.
    Found on Reservoir.

    importGraph461b96f

    Tools to analyse and visualise the import structure of Lean packages and their files.
  4. Registry dependency.
    Found on Reservoir.

    proofwidgetsv0.0.52-pre2

    Helper toolkit for creating your own Lean 4 UserWidgets
  5. Registry dependency.
    Found on Reservoir.

    aesopnightly-testing-2025-02-03

    White-box automation for Lean 4
  6. Registry dependency.
    Found on Reservoir.

    Qqv4.17.0-rc1

    Intuitive, type-safe expression quotations for Lean 4.
  7. Registry dependency.
    Found on Reservoir.

    batteries80520e5

    The "batteries included" extended library for the Lean programming language and theorem prover