Registry
Proof registry
Four Lean 4 formal-verification packages. Every number below is machine-extracted from the source repositories at a pinned commit. Machine-readable: /api/proofs.
| Package | Status | Key metric | Identifiers |
|---|---|---|---|
| S437: Lean 4.34.1 port and rebuild of OpenAI's NavierStokesAndEuler formalization (Clay alternatives C and D) gi:proof:s437 |
Released Builder-run · not independently reviewed |
21 modules edited · 2 kernels | DOI 10.5281/zenodo.23448690 Q141761720 |
| Navier–Stokes R2/R3 community verification package, V1 gi:proof:r2r3 |
Released Builder-run · not independently reviewed |
40,986 theorems · 620-module closure | DOI 10.5281/zenodo.23535805 Q141803373 |
| Lean 4 - Proof - Navier–Stokes C/D (KTS Global) gi:proof:nscd |
Released Builder-run · not independently reviewed |
12 declarations · 14 axiom-policy checks | DOI 10.5281/zenodo.23917705 Q141986416 |
| Lean 4 - Proof - Tao ShortBound to Global Regularity gi:proof:tao-shortbound |
Release candidate Conditional Builder-run · not independently reviewed |
8,959 jobs · 58 axiom-policy checks | DOI pending Wikidata pending |