Pinned Reservoir catalog
Search package metadata by name, description, keyword, license, toolchain, or dependency name. Proof-indexed projects connect to their exact Therefore declaration records.
782 packages
782 packages pinned from Reservoir
sdiehl/KittyCats
Category theory but for kitty cats, meow 🐱🐈
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
agenticsnz/unsorry
Autonomous agents proving theorems in Lean 4 - SETI@Home but for maths proofs using LLMs. Git is the queue, the kernel is the gate, no sorry survives.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
djvelleman/htpi
Lean package for "How To Prove It with Lean", a companion to the book "How To Prove It"
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lambdaclass/trzk
Verified Optimizing Compiler for Cryptographic Primitives
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
riccardobrasca/FLT3
Proof in Lean of Fermat Last Theorem for exponent 3
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dwrensha/tryAtEachStep
Try a tactic at each step in a Lean proof.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
kmill/LeanTeX
Lean 4 library for pretty printing expressions as LaTeX
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leonardoalt/evmSmith
A framework for AI systems to write EVM bytecode and prove it safe, built on NethermindEth/EVMYulLean.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
argumentcomputer/Megaparsec.lean
Lean 4 port of Megaparsec
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover/lean4export
Plain-text declaration export for Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
dwrensha/Chess
Chess in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
google-deepmind/imo
Lean formalizations of IMO problem statements
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.