rami3l/plfl
plfl
Learn Lean 4 with PLFA proofs.
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 114
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Pinned Reservoir catalog
Lean packages and dependencies
Search package metadata by name, description, keyword, license, toolchain, or dependency name. Proof-indexed projects connect to their exact Therefore declaration records.
Package records are ecosystem metadata. Build evidence appears only when Reservoir observed the exact revision and toolchain.
782 packages
782 packages pinned from Reservoir
AxiomMath/Putnam2025
Putnam2025
Our solutions to Putnam 2025.
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 111
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/Project
Project
A template for blueprint-driven formalization projects in Lean.
Reservoir metadata only · declarations not indexed
- Versions
- 32
- Declarations
- Not indexed
- GitHub stars
- 111
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/Qq
Intuitive, type-safe expression quotations for Lean 4.
Reservoir metadata only · declarations not indexed
- Versions
- 58
- Declarations
- Not indexed
- GitHub stars
- 111
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
vihdzp/CombinatorialGames
CombinatorialGames
Combinatorial game library in Lean 4
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 110
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/plausible
plausible
No package description is available.
Reservoir metadata only · declarations not indexed
- Versions
- 59
- Declarations
- Not indexed
- GitHub stars
- 109
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
pandaman64/lean-regex
lean-regex
No package description is available.
Reservoir metadata only · declarations not indexed
- Versions
- 25
- Declarations
- Not indexed
- GitHub stars
- 108
- License
- Apache-2.0
emilyriehl/InfinityCosmos
InfinityCosmos
A blueprint for a formalization of infinity-cosmos theory in Lean.
Reservoir metadata only · declarations not indexed
- Versions
- 20
- Declarations
- Not indexed
- GitHub stars
- 106
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/Comparator
Comparator
No package description is available.
Reservoir metadata only · declarations not indexed
- Versions
- 23
- Declarations
- Not indexed
- GitHub stars
- 106
- License
- Apache-2.0
James-Hanson/junk-theorems
junk-theorems
A small collection of formally verified junk theorems provable in Lean4 + Mathlib.
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 105
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lean-dojo/TorchLean
TorchLean
Neural network specification, execution, and verification in Lean 4.
Reservoir metadata only · declarations not indexed
- Versions
- 5
- Declarations
- Not indexed
- GitHub stars
- 104
- License
- MIT
leanprover/lnsym
lnsym
Armv8 Native Code Symbolic Simulator in Lean
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 103
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.