AlexKontorovich/PrimeNumberTheoremAnd
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
Therefore indexed · 57 selected declarations
- Versions
- 9
- Declarations
- 57
- GitHub stars
- 325
- License
- Apache-2.0
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
teorth/PFR
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Therefore indexed · 45 selected declarations
- Versions
- 23
- Declarations
- 45
- GitHub stars
- 222
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
fpvandoorn/carleson
carleson
A formalized proof of Carleson's theorem in Lean
Therefore indexed · 60 selected declarations
- Versions
- 38
- Declarations
- 60
- GitHub stars
- 101
- License
- Apache-2.0
YaelDillies/APAP
APAP
Formalisation of the Kelley-Meka bound on Roth numbers
Therefore indexed · 38 selected declarations
- Versions
- 21
- Declarations
- 38
- GitHub stars
- 27
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
leanprover-community/mathlib
mathlib
The math library of Lean 4
Reservoir metadata only · declarations not indexed
- Versions
- 106
- Declarations
- Not indexed
- GitHub stars
- 3663
- License
- Apache-2.0
teorth/Analysis
Analysis
A Lean companion to Analysis I
Reservoir metadata only · declarations not indexed
- Versions
- 1
- Declarations
- Not indexed
- GitHub stars
- 1826
- License
- Apache-2.0
Reservoir observed an exact-toolchain build. Therefore did not run this build.
ulfjack/ryu
ryu
Converts floating point numbers to decimal strings
Reservoir metadata only · declarations not indexed
- Versions
- 2
- Declarations
- Not indexed
- GitHub stars
- 1347
- License
- Apache-2.0
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
lean-dojo/LeanCopilot
LeanCopilot
LLMs as Copilots for Theorem Proving in Lean
Reservoir metadata only · declarations not indexed
- Versions
- 48
- Declarations
- Not indexed
- GitHub stars
- 1302
- License
- MIT
Reservoir observed an exact-toolchain build failure. Therefore did not run this build.
google-deepmind/formal_conjectures
formal_conjectures
A collection of formalized statements of conjectures in Lean.
Reservoir metadata only · declarations not indexed
- Versions
- 18
- Declarations
- Not indexed
- GitHub stars
- 1122
- License
- Apache-2.0
ImperialCollegeLondon/FLT
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Reservoir metadata only · declarations not indexed
- Versions
- 46
- Declarations
- Not indexed
- GitHub stars
- 947
- License
- Apache-2.0
leanprover-community/Physlib
Physlib
A project to digitalise results from physics into Lean.
Reservoir metadata only · declarations not indexed
- Versions
- 22
- Declarations
- Not indexed
- GitHub stars
- 655
- License
- Apache-2.0
leanprover/cslib
cslib
The Lean Computer Science Library (CSLib)
Reservoir metadata only · declarations not indexed
- Versions
- 29
- Declarations
- Not indexed
- GitHub stars
- 630
- License
- Apache-2.0