Every row of the claims register is derived from a record, and every record is re-derivable from this repository. This page is the kit: for each record, the command that re-derives it, the standard-library verifier where one exists, the independent second implementation where one exists, and the record's hash at this build — and the registry of who outside has re-run what, which is the only number here that measures the independence this machine claims.
Published, not peer-reviewed. 1 independent rerun recorded at this build, 1 with no code of ours. Until that number is larger than the number of operators (one), the verdicts here rest on one machine and one person, and this page says so rather than implying otherwise.
| record · what it needs | rows it decides | re-derive | stdlib verifier | second implementation | sha256 at this build |
|---|---|---|---|---|---|
| certs/ai-claims-summary.json nothing to run | 6 rows 5 CERTIFIED, 1 PARTIAL | — | — | — | d5e561e3888537da… |
| certs/erdos852-certificate.json node for the export; python3 standard library for the verifier; corpus/sources for the pinned paper | 1 row 1 REFUTED | node tools/export-erdos852-certificate.js 4.8 s | python3 tools/verify_erdos852.py certs/erdos852-certificate.json --sources corpus/sources < 1 s | — | 4379194d0bd4e63b… |
| certs/kissing-ledger.json node | 11 rows 10 CERTIFIED, 1 QUEUED | node tools/run-kissing-ledger.js 2.9 s | — | — | 9d1cf51507fee327… |
| ledger.json node; about four minutes | 1 row 1 MIXED | make engine 5 min | — | — | 2a34c34f14867fbf… |
| certs/strassen-certificate.json node for the export; python3 standard library for the verifier; corpus/sources for the pinned bytes | 10 rows 10 CERTIFIED | node tools/export-strassen-certificate.js < 1 s | python3 tools/verify_strassen.py certs/strassen-certificate.json --sources corpus/sources < 1 s | — | 2ab21d5adc6a2948… |
| certs/easota-ledger.json node | 20 rows 16 CERTIFIED, 4 REPAIRED | node tools/run-easota-ledger.js 3 s | — | — | 60b947daf148e6ec… |
| certs/ecbench-ledger.json node; about a minute | 1 row 1 MIXED | node tools/run-ecbench-ledger.js 5.8 s | — | — | cdecac8aae53d79c… |
| certs/gsm8k-ledger.json python3 standard library and the instrument's own modules (instruments/gsm8k) | 1 row 1 MIXED | python3 tools/run-gsm8k-ledger.py 1.5 s | — | — | 7fbcda606b601c9c… |
| certs/horizon-ledger.json python3 standard library and the instrument's own modules (instruments/horizon) | 1 row 1 MIXED | python3 tools/run-horizon-ledger.py 1.9 min | — | — | fa5b0bac0539bf96… |
| certs/hseva-ledger.json node; several minutes with workers in parallel | 1 row 1 MIXED | node tools/run-hseva-ledger.js --check 6.3 min | — | — | a6971779e880a359… |
| certs/design-table-audit.json node | 1 row 1 NEEDS DATA | node tools/run-design-table-audit.js --check < 1 s | — | — | e8278b62a87d2e0a… |
| corpus/navier-stokes/audit.json a Lean 4 toolchain at the pinned commit, for the counts the record points at | 1 row 1 PARTIAL | — | — | — | 88beb85b6a5474f7… |
| certs/sumdiff-ledger.json node; python3 standard library for the verifier | 3 rows 3 CERTIFIED | node tools/run-sumdiff-ledger.js --check 1.1 s | python3 tools/verify_sumdiff.py < 1 s | — | 5b4ce435f0d004fc… |
| certs/fei-ledger.json python3 standard library and instruments/fei | 1 row 1 CERTIFIED | python3 tools/run-fei-ledger.py --check 1.4 s | — | — | 38d06c5e779f366e… |
| certs/sumproduct-ledger.json python3 standard library and instruments/sumproduct | 1 row 1 REPAIRED | python3 tools/run-sumproduct-ledger.py --check 36.7 s | — | — | 61cc3c57f7a6567c… |
| certs/turan-ledger.json python3 standard library and instruments/turan | 2 rows 2 PARTIAL | python3 tools/run-turan-ledger.py --check 1.6 s | — | — | f0b9c2b48a5b3265… |
| certs/countex-ledger.json python3 standard library and instruments/countex (fourteen deciders, each reading only the published certificate) | 14 rows 5 PARTIAL, 9 CERTIFIED | python3 tools/run-countex-ledger.py --check 33.3 s | — | — | 948f6c633e514274… |
| certs/horizonmath-ledger.json python3 standard library and instruments/horizonmath | 3 rows 1 REFUTED, 1 CERTIFIED, 1 NEEDS DATA | python3 tools/run-horizonmath-ledger.py --check 1.6 s | — | — | 78adab0aa528381d… |
| certs/gnnw-certificate.json python3 standard library for the ledger and the verifier; node for the second implementation (bigfloat, monotone bounds, no written derivative) | 1 row 1 CERTIFIED | python3 tools/run-gnnw-ledger.py --check 3.1 min | python3 tools/verify_gnnw_gai.py certs/gnnw-certificate.json 7.7 s | node instruments/gnnw/second.js certs/gnnw-certificate.json 2.1 min | b7127457078d064e… |
| certs/polymaps-ledger.json python3 standard library and instruments/polymaps | 8 rows 7 CERTIFIED, 1 PARTIAL | python3 tools/run-polymaps-ledger.py --check 83.5 s | — | — | 63ce598a073c1718… |
Runtimes are measured: every command executed on 2026-10-02 on Apple M2 (Darwin 27.0.0, v24.14.1, Python 3.9.6), the register's rows compared before and after. The hash is of the record as this page was built; a clone at another commit may differ, and the report form asks for the hash you have.
The debts. certs/ai-claims-summary.json: The consolidated summary of the six-lane audit of a frontier-model manuscript (reports/ai-claims-audit.html): six verdicts, each a named PASS row of its lane's battery. No single command re-derives this record; the lanes' batteries are the re-derivation and the page names them. A kit debt. corpus/navier-stokes/audit.json: The qualitative findings of the 2026-09-09 audit of OpenAI's Navier–Stokes claim. The record itself is read, not computed; every count on its page comes from lean-repo.json, probes.json and build.json, which the pinned Lean build (corpus/navier-stokes/MANIFEST.json) re-derives. A kit debt: the Lean rebuild is not a one-line command here. These are the records a reader cannot re-derive with one line yet; the page counts them rather than hiding them.
Every row of the register carries the same fields, filled from its record by tools/run-claims-ledger.js and never typed: id, claim (what the claimant printed), claimant, source (the bytes, pinned where they exist), origin (self-initiated or submitted), verdict, scope (what was actually decided), kind (what went wrong, from the vocabulary below), decidedFrom (the record), page, recordedOn (the first commit whose record held the row). The three verdicts are CERTIFIED, REFUTED and REFUSED; PARTIAL, MIXED, REPAIRED and NEEDS DATA are compositions of those three and the register page says which.
| kind | meaning | rows |
|---|---|---|
| none | the claim holds as printed | 64 |
| narrower-scope | decided only in a narrower scope than printed; the rest is out of reach, not wrong | 8 |
| float-printed-as-exact | a floating-point result printed as the exact quantity | 1 |
| sign-slip | a sign wrong in a printed constant | 1 |
| arithmetic-slip | a printed arithmetic step that does not hold | 2 |
| tolerance-witness | a witness only within a numerical tolerance; the printed value is the tolerance's | 4 |
| not-the-optimum | printed as an optimum, but not the one the definition names (a stop short of it, or a local one) | 1 |
| wrong-quantity | the printed number is a correct answer to a different question | 1 |
| not-from-the-published-data | the printed number is not what the published data give, and the arithmetic is not why | 1 |
| outside-support | the printed model gives observed data zero density | 0 |
| clause-missing-from-formal-statement | a clause the prose claims is absent from the formal statement that is proved | 1 |
| data-not-public | the data behind the claim are not public, so no one outside can decide it | 2 |
| depends-on-reading | the claim holds under one of two definitions its own text gives, and not under the other | 1 |
| checker-wider-than-definition | the checker that accepted the claim admits what the definition it encodes excludes | 1 |
The oracle's machine-readable contract — the claim a caller sends and the result it gets back — is a JSON schema in the repository: oracle/claim-schema.json and oracle/certificate-schema.json, enforced by oracle/battery.py at every build of /oracle/.
| who | date | what was rerun | how | obtained | hash · code |
|---|---|---|---|---|---|
| rainrzk (GitHub) | 2026-09-30 | λ(4) for Erdős #510 (reports/lambda4.html): the cubic, the 14 generic collisions and the nine families re-derived from the write-up with independent code; every finite case re-certified in interval arithmetic; every gcd-reduced 4-set with largest element ≤ 80 swept as a proof-independent control. | own-code | the same verdict; three documentation findings in the write-up, folded in (commit 1c248ca) | code · posted |
Three kinds and no fourth: own-code — the claim re-derived from the published statement with the reporter's own program; none of this repository's code ran; detached-verifier — one of the standard-library verifiers run on a copy of the record; the sha256 it prints reported; full-rederive — the record re-derived with the tool that writes it; the register's rows compared. The registry is corpus/external-reruns.json; a row is added by hand from a rerun report, and the build refuses a row that lacks a field or names a kind outside these three.
V8's BigInt and IEEE-754 directed rounding in the engine; Python's fractions and decimal in the detached verifiers; a handful of named external theorems consumed and cross-checked, never machine-proved; the operating system's hashing; and one operator on one machine. Each item on that list is shrunk by a different thing: the verifiers shrink the engine, the second implementations shrink the verifiers, and only the registry above shrinks the last item.