Lake's package registry

No results found

Latest Lean Stable:

leanprover/lean4:v4.18.0
Get Started with Lean

Reservoir indexes, builds, and tests packages within the Lean and Lake ecosystem. If you wish to see your package here, ensure that it meets the Reservoir inclusion criteria.

Most Popular

  1. Commit fb36f5e builds on the recent leanprover/lean4:v4.19.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 0e08fbb builds on the recent leanprover/lean4:v4.19.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  4. Commit 2c9cad0 builds on the recent leanprover/lean4:v4.19.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  5. Commit 53f112d builds on the old leanprover/lean4:v4.15.0
    scilean
    Scientific computing in Lean 4
  6. Commit fec5b39 builds on the old leanprover/lean4:v4.14.0-rc3
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  7. Commit f523fcb builds on the recent leanprover/lean4:v4.19.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  8. Commit 323e9f0 builds on the recent leanprover/lean4:v4.19.0-rc3
    aesop
    White-box automation for Lean 4
  9. Commit 731400d builds on the recent leanprover/lean4:v4.19.0-rc3
    lean4-metaprogramming-book
  10. Commit 07da422 builds on the old leanprover/lean4:v4.5.0
    formalising-mathematics-2024
    Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
All most popular

Newly Created

  1. Commit 078a0db builds on the recent leanprover/lean4:v4.19.0-rc3
    kimina
    A Lean tactic that invokes the Kimina Prover Preview model to offer proof suggestions.
  2. Commit 3118411 builds on the recent leanprover/lean4:v4.19.0-rc3
    cryptolib
  3. Commit 02f8d14 builds on the recent leanprover/lean4:v4.18.0-rc1
    LeanTeX_Mathlib
    LeanTeX pretty printers for mathlib
  4. Commit 6e27ac1 builds on the recent leanprover/lean4:v4.18.0-rc1
    NeuralNetworks
    Formalization of Neural Networks in Lean 4
  5. Commit c4586f5 builds on the recent leanprover/lean4:v4.18.0-rc1
    combinatorial-games
    Combinatorial game library in Lean 4
  6. Commit 0be2cbd fails to build on leanprover/lean4:v4.19.0-rc3
    lean4-analysis-tao
    Formalization of "Analysis I" by Terence Tao
  7. Commit 75d0dab fails to build on leanprover/lean4:v4.19.0-rc3
    sqlite
    Sqlite3 bindings for lean4
  8. Commit ecdde79 builds on the recent leanprover/lean4:v4.18.0-rc1
    LeanBanachTarski
  9. Commit 747d48e builds on the recent leanprover/lean4:v4.19.0-rc3
    Toric
    Formalisation of toric varieties in Lean 4
  10. Commit 7fd55ea fails to build on leanprover/lean4:v4.18.0
    formalising-mathematics
    Course on theorem proving with Lean
All newly created

Recently Updated

  1. Commit fb36f5e builds on the recent leanprover/lean4:v4.19.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit dcee04a builds on the recent leanprover/lean4:v4.18.0-rc1
    verso
    Lean documentation authoring tool
  3. Commit 5ef42ea builds on the recent leanprover/lean4:v4.19.0-rc3
    subverso
  4. Commit 0661c91 builds on the recent leanprover/lean4:v4.18.0
    VCVio
    Formalized Cryptography Proofs in Lean 4
  5. Commit f523fcb builds on the recent leanprover/lean4:v4.19.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  6. Commit 492605a builds on the recent leanprover/lean4:v4.19.0-rc3
    clt
    Central limit theorem in Lean
  7. Commit 731400d builds on the recent leanprover/lean4:v4.19.0-rc3
    lean4-metaprogramming-book
  8. Commit d797849 builds on the recent leanprover/lean4:v4.18.0
    lean4export
    Plain-text declaration export for Lean 4
  9. Commit 7bcce40 builds on the recent leanprover/lean4:v4.19.0-rc3
    Matroid
  10. Commit 9498454 builds on the recent leanprover/lean4:v4.18.0
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
All recently updated