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
kkytola/ExtremeValueProject
A project to formalize Fisher-Tippett-Gnedenko theorem (default project of course MS-EV0029)
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
klavins/LeanBook
Notes on the Foundations of Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
kmill/CSE290Q
CSE 290Q: Topics in Interactive Theorem Provers
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lean-ja/verso-manual
「The Lean Language Reference」の日本語訳（作業中）
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
leanprover/LPBackendSoplexFFI
LPBackend adapter for kim-em/soplex-ffi. Priority 10 (FFI band). The native backend kim-em/soplex defaults to.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
lindy-labs/WadrayVerification
Verification of the Wadray library
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
m4lvin/Gossip
Verified Results about Gossip protocols in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
madvorak/thue
Semi-Thue systems a.k.a. string rewriting systems
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
Mintpath/p_ne_np
Machine-verified proof (0 sorries, 2 axioms) that P ≠ NP via exponential circuit lower bounds for Hamiltonian Cycle. Lean 4 formalization with Mathlib. Proves SIZE(HAM_n) ≥ 2^{Ω(n)} using frontier analysis, switch blocks, cross-pattern mixing, recursive funnel magnification, continuation packets, rooted descent, and signature rigidity.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
misaka10987/archimedes
Don't disturb my circle!
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
mitchell-horner/ErdosStoneSimonovitsKovariSosTuran
Formalising the Erdős-Stone-Simonovits theorem and the Kővári–Sós–Turán theorem in Lean
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
monsterkrampe/PossiblyInfiniteTrees
This repo formalizes (possibly) infinite trees of finite degree in Lean. So far this is mainly a dependency for one of my other projects and tailored towards this purpose. The repo features a formalization of (a special case of) König's Lemma.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.