weiran-sun/PDE
PDE
PDE Lean formalization
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 8
- License
- Apache-2.0
Reservoir observed an exact-toolchain build failure. 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
AlexeyMilovanov/kolmogorov_complexity
kolmogorov_complexity
Formalization of Algorithmic Information Theory in Lean 4
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
andrejbauer/lean2sexp
lean2sexp
Convert Lean .olean files to s-expressions
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- BSD-2-Clause
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
anoma/juvix-lean
juvix-lean
Juvix Lean library for compiler run verification
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
argumentcomputer/Blake3
Blake3
Lean4 bindings to Blake3
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
arthur-adjedj/Leanduction
Leanduction
Generate good induction principles on nested inductive types
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Bacon-labs/tamago
tamago
Common EVM smart contracts similar to solady/solmate, formally verified using Tama + Verity
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT
Reservoir observed an exact-toolchain build. Therefore did not run this build.
bkase/VerifiedGPU
VerifiedGPU
No package description is available.
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
bridgekat/filter-game
filter-game
Lean 4 version of the filter game.
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
GasStationManager/FormalizeWithTest
FormalizeWithTest
Autoformalization of coding problems, verified with test cases
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- GPL-3.0
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
girafe-ai/formalising-mathematics
formalising-mathematics
Course on theorem proving with Lean
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- Apache-2.0
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
jimscarver/QuantumLogicalFramework
QuantumLogicalFramework
quantum genesis constructive possibilist quantum logical synthesis
Reservoir metadata only · declarations not indexed
- Versions
- 61
- Declarations
- Not indexed
- GitHub stars
- 7
- License
- MIT