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 f541cd9 builds on the recent leanprover/lean4:v4.21.0-rc3
    mathlib
    The math library of Lean 4
  2. Commit 2b2d590 builds on the recent leanprover/lean4:v4.21.0-rc3
    LeanCopilot
    LLMs as Copilots for Theorem Proving in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 8624132 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  5. Commit 7fc314d builds on the recent leanprover/lean4:v4.21.0-rc3
    FLT
    Ongoing Lean formalisation of the proof of Fermat's Last Theorem
  6. Commit 902b97d builds on the recent leanprover/lean4:v4.21.0-rc3
    paperproof
    Lean theorem proving interface which feels like pen-and-paper proofs.
  7. Commit 53f112d builds on the old leanprover/lean4:v4.15.0-rc1
    scilean
    Scientific computing in Lean 4
  8. Commit f1ba144 builds on the recent leanprover/lean4:v4.20.1
    equational_theories
    A project to map out the relations between different equational theories of Magmas.
  9. Commit d12fdad builds on the recent leanprover/lean4:v4.21.0-rc3
    batteries
    The "batteries included" extended library for the Lean programming language and theorem prover
  10. Commit 1b1abe6 builds on the recent leanprover/lean4:v4.21.0-rc3
    aesop
    White-box automation for Lean 4

Newly Created

  1. Commit b1b92c7 builds on the recent leanprover/lean4:v4.21.0-rc3
    cslib
    Lean library for Computer Science
  2. Commit 98153df fails to build on leanprover/lean4:v4.21.0-rc3
    tactic-programming-beginner-guide
    Beginner's guide to Tactic Programming in Lean
  3. Commit 3d91ad1 builds on the recent leanprover/lean4:v4.20.0
    analysis
    A Lean companion to Analysis I
  4. Commit 3c0efe0 builds on the old leanprover/lean4:v4.19.0
    Lie
    A classification theorem in Lean of solvable Lie algebras of dimension zero to three
  5. Commit 312192d builds on the old leanprover/lean4-pr-releases:pr-release-8003
    mini-redis
    An implementation of mini-redis in Lean 4
  6. Commit 7351fae builds on the old leanprover/lean4:v4.18.0
    verina
    Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
  7. Commit 9f0f43c builds on the recent leanprover/lean4:v4.21.0-rc3
    SemicircleLaw
    Formalization of Wigner's Semicircle Law in Lean
  8. Commit 7087b15 fails to build on leanprover/lean4:v4.21.0-rc3
    lie-classification
    Classification of Lie algebras in Lean
  9. Commit 8624132 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  10. Commit b8d0cec builds on the old leanprover/lean4:v4.19.0
    bruhat-tits
    A formalisation of the Bruhat-Tits tree in Lean4

Recently Updated

  1. Commit f554728 builds on the old leanprover/lean4:v4.17.0-rc1
    SSA
    A minimal development of SSA theory
  2. Commit 8624132 builds on the old leanprover/lean4:v4.17.0
    formal_conjectures
    A collection of formalized statements of conjectures in Lean.
  3. Commit 528ee45 builds on the recent leanprover/lean4:v4.20.1
    Clean
    Lean circuit DSL
  4. Commit 3df8b7c builds on the recent leanprover/lean4:v4.21.0-rc3
    Heights
    An attempt at formalizing the theory of heights in Lean
  5. Commit 4e76d20 builds on the recent leanprover/lean4:v4.20.0
    PrimeNumberTheoremAnd
    blueprint for prime number theorem and more
  6. Commit e08b4a8 builds on the recent leanprover/lean4:v4.21.0-rc3
    veil
    A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.
  7. Commit 76be179 builds on the recent leanprover/lean4:v4.21.0-rc3
    verso
    Lean documentation authoring tool
  8. Commit f541cd9 builds on the recent leanprover/lean4:v4.21.0-rc3
    mathlib
    The math library of Lean 4
  9. Commit 99ffeee builds on the old leanprover/lean4:v4.18.0
    ix
    a zero-knowledge proof-carrying code platform for Lean 4
  10. Commit 64a6adb builds on the old leanprover/lean4:v4.19.0
    KLR
    A formalization of ML kernel languages