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 | — | — | 91c6ad8884ba8578… |
| 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 | — | — | e577361347e77561… |
| 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 CERTIFIED | — | — | — | 5931f9ad48b4ed87… |
| 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 | — | bf8857db9f64b650… |
| 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 | — | — | c3f99c9398ef410e… |
| certs/mc100-alphatensor-q.json node and python3 (the transcriber is stdlib Python for the npz archives); the verifier is python3 standard library alone | 12 rows 12 CERTIFIED | node tools/run-mc100-tensors.js alphatensor-q not yet timed | python3 tools/verify_strassen.py certs/mc100-alphatensor-q.json --sources corpus/sources not yet timed | — | 753485444a3e4498… |
| certs/mc100-alphatensor-f2.json node and python3 (the transcriber is stdlib Python for the npz archives); the verifier is python3 standard library alone | 8 rows 8 CERTIFIED | node tools/run-mc100-tensors.js alphatensor-f2 not yet timed | python3 tools/verify_strassen.py certs/mc100-alphatensor-f2.json --sources corpus/sources not yet timed | — | 0222c5552b7c24f3… |
| certs/mc100-alphaevolve-nb-matmul.json node and python3 (the transcriber is stdlib Python for the npz archives); the verifier is python3 standard library alone | 15 rows 15 CERTIFIED | node tools/run-mc100-tensors.js alphaevolve-nb-matmul not yet timed | python3 tools/verify_strassen.py certs/mc100-alphaevolve-nb-matmul.json --sources corpus/sources not yet timed | — | 50183f3ffba87bd2… |
| certs/mc100-einstein-arena.json node (about 90 s: the 65,536-value autocorrelation and the 500-row edges-vs-triangles envelope dominate) | 8 rows 1 REPAIRED, 7 CERTIFIED | node tools/run-mc100-einstein.js not yet timed | — | — | cc0b63ba9ed9ebdc… |
| certs/mc100-station-v2.json python3 standard library and instruments/polymaps | 1 row 1 CERTIFIED | python3 tools/run-mc100-station.py not yet timed | — | — | b526305ff85bbb35… |
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.
The milestone of this program is one sentence: five independent parties obtain the same verdicts on this corpus — or record where they do not. These rows were chosen for one property — someone outside this lab has a reason to re-derive them and the means to do it in a line. Each party's ask is drafted in the repository (outreach/rerun-asks-2026-10-02.md) and is sent only on the operator's word, one at a time; a party counts below when a row of theirs in the registry names one of these ids, and not before.
| party | why them | rows | status |
|---|---|---|---|
| rainrzk (GitHub) — re-certified λ(4) with no shared code on 2026-09-30 | the one outside party who has already done this once; three rows with standard-library verifiers or a finite re-derivation | erdos852-cstar · REFUTED REFUTED at its printed digits; one Python file, 0.6 s, re-hashes the pinned thread and refutes a forgery mm-alphaevolve-48-4x4x4 · CERTIFIED AlphaEvolve's 48 over Z[i]: 4,096 identities, one Python file, 0.3 s optconst-84b · REPAIRED REPAIRED: a note's chain re-derived for every choice; a finite sweep of the kind the λ(4) audit did, 37 s | open |
| S. Norin (Gupta–Ndiaye–Norin–Wei), for the authors | the theorem both rows are decided on is theirs; one row certifies their own unverified iteration, the other refutes a certificate claimed against it | gnnw-gai-3782 · CERTIFIED their own 'preliminary, unverified' G_AI certified on their Theorem 14 by two programs; the one-file verifier runs in 8 s horizonmath-ramsey-asymptotic · REFUTED a certificate claimed against their theorem, REFUTED: 56 of 201 points outside R; --check in 2 s | open |
| the EinsteinArena thread (vinid/einstein-arena #64) and the Dualverse Station authors | their 604 configurations are the rows; the thread is open since 2026-09-08; one of their rows is REPAIRED, which is the kind an author wants to re-check | kiss-ea-604 · CERTIFIED the platform's headline 604 certified from its own file; congruent to the Station's configuration 1 kiss-station-604-1 · CERTIFIED the Station's configuration 1, the same configuration in another frame; the congruence certificate is public ea-overlap-together_ai_2026 · REPAIRED REPAIRED: the published step function is a witness only within the platform's tolerance; the repaired one beside it is certified | open |
| S. Sra (count-ex-machina) | the one case in his library that holds under one of its own two readings and not the other | countex-dpp-feasible-step · PARTIAL PARTIAL, depends-on-reading: certified under the context paragraph's 'feasible', not under the statement block's Prop. A.1 bound | open |
| the LabECO pair (UFSC; not named in this repository) | the wave rows are their field and the partnership is open; a rerun by them is also the first step of P1's review | ecbench-marginals · MIXED MIXED: of the benchmark's 15 printed Hs marginals, 5 reproduce a certified maximum, 1 printed as Hs is the fit of Tz; --check in 6 min | open |
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 | 108 |
| 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 | 5 |
| 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 | 0 |
| 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. not a register row (a lab theorem) | 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.