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
davidturturean/Erdos870
Erdős Problem #870: paper and sorry-free, axiom-clean Lean 4 formalization.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
google-deepmind/putnam_like
Lean formalizations of Putnam-like problems
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ImperialCollegeLondon/IUM
Lean formalisation of parts of Imperial College London's Introduction to University Mathematics course
Reservoir metadata only · declarations not indexed
palladin/lean_eff
LeanEff is a small Lean 4 extensible-effects library
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
SAIRcompetition/stage2-judge
This repository hosts the SAIR Mathematics Distillation Challenge: Equational Theories Stage 2, providing Lean 4 problem sets, judging tools, and submission harnesses for generating machine-checkable proof certificates.
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
alok/LeanPlot
Interactive React-powered charting library for Lean 4 in VS Code's infoview
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
AxiomMath/LatticeTriangle
Lean formalizations for the paper "On the paucity of lattice triangles"
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ElifUskuplu/stlc
Simply Typed Lambda Calculus with de Bruijn indices
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build. Therefore did not run this build.
lenianiva/Prismriver
(Mirror) A Music formalization library and DSL in Lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
nimarasekh/Formalization_SoSe25
Teaching Material for Course on Formalization Summer Semester 2025 at Uni Greifswald
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
quangvdao/Zklib
deprecated, use Verified-zkEVM repository instead
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
siddhartha-gadgil/lean-loris
Experiments with some ways of automating reasoning in lean 4
Reservoir metadata only · declarations not indexed
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.