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. 8 independent reruns recorded at this build, by 4 outside parties, 6 with no code of ours; they name 15 of the 145 register rows. Every other verdict here rests 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/ 5.5 s | python3 tools/verify_erdos852.py certs/erdos852-certificate.json --sources corpus/sources < 1 s | — | 13cfc7fa212a4355… |
| certs/kissing-ledger.json node | 11 rows 10 CERTIFIED, 1 QUEUED | node tools/ 7.2 s | — | — | 5c823b21ac43b5bd… |
| ledger.json node | 1 row 1 MIXED | make engine 5.7 min | — | — | 4b666d3d92235765… |
| 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/ < 1 s | python3 tools/verify_strassen.py certs/strassen-certificate.json --sources corpus/sources < 1 s | — | 0e400efeb8a4bba9… |
| certs/easota-ledger.json node | 20 rows 16 CERTIFIED, 4 REPAIRED | node tools/ 3.2 s | — | — | 57f46876a7c79b0c… |
| certs/ecbench-ledger.json node | 1 row 1 MIXED | node tools/ 6.1 s | — | — | 8b1230e4fb6f91d9… |
| certs/gsm8k-ledger.json python3 standard library and the instrument's own modules (instruments/gsm8k) | 1 row 1 MIXED | python3 tools/ 1.6 s | — | — | 7fbcda606b601c9c… |
| certs/horizon-ledger.json python3 standard library and the instrument's own modules (instruments/horizon) | 1 row 1 MIXED | python3 tools/ 2.2 min | — | — | fa5b0bac0539bf96… |
| certs/hseva-ledger.json node; workers in parallel | 1 row 1 MIXED | node tools/ 8.6 min | — | — | 23aa58c1078c357a… |
| certs/design-table-audit.json node | 1 row 1 NEEDS DATA | node tools/ < 1 s | — | — | c88a6bcd5ce5b76e… |
| 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/ 1.2 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/ 1.5 s | — | — | ad853dabf8380298… |
| certs/sumproduct-ledger.json python3 standard library and instruments/sumproduct | 1 row 1 REPAIRED | python3 tools/ 38.6 s | — | — | d7ba43139ee62901… |
| certs/turan-ledger.json python3 standard library and instruments/turan | 2 rows 2 PARTIAL | python3 tools/ 1.7 s | — | — | e6143188777c194f… |
| 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/ 34.5 s | — | — | 948f6c633e514274… |
| certs/horizonmath-ledger.json python3 standard library and instruments/horizonmath | 3 rows 1 REFUTED, 1 CERTIFIED, 1 NEEDS DATA | python3 tools/ 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/ 3.6 min | python3 tools/verify_gnnw_gai.py certs/gnnw-certificate.json 9.4 s | node instruments/ 2.7 min | 3d53ef1378303a8a… |
| certs/polymaps-ledger.json python3 standard library and instruments/polymaps | 8 rows 7 CERTIFIED, 1 PARTIAL | python3 tools/ 1.6 min | — | — | b6fbd6aad035e3de… |
| 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/ < 1 s | python3 tools/verify_strassen.py certs/mc100-alphatensor-q.json --sources corpus/sources < 1 s | — | 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/ < 1 s | python3 tools/verify_strassen.py certs/mc100-alphatensor-f2.json --sources corpus/sources < 1 s | — | 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/ 1.6 s | python3 tools/verify_strassen.py certs/mc100-alphaevolve-nb-matmul.json --sources corpus/sources 1.1 s | — | 50183f3ffba87bd2… |
| certs/mc100-einstein-arena.json node (the 65,536-value autocorrelation and the 500-row edges-vs-triangles envelope dominate the run) | 8 rows 1 REPAIRED, 7 CERTIFIED | node tools/ 46.6 s | — | — | 2526c08b4a11f2ab… |
| certs/mc100-station-v2.json python3 standard library and instruments/polymaps | 1 row 1 CERTIFIED | python3 tools/ < 1 s | — | — | 07eb6c0f63784e1e… |
| certs/eth-kernel.json node; the imported pod facts in corpus/eth-refutation/runs (runpod-x8ifbbj2vbolyj, runpod-69d9t7dxjffo6n, runpod-ijw7890hq4ed9x) | 2 rows 2 CERTIFIED | node tools/ < 1 s | — | — | 09302f11bbae643e… |
| certs/eth-tsavo-bridge.json node; the kept GitHub run under corpus/eth-refutation/tsavo/runs | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | 9349d0dfa43cdffc… |
| certs/eth-hawkley-bridge.json node; the kept GitHub run under corpus/eth-refutation/hawkley/runs | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | 8d00cca0cdc5f816… |
| certs/eth-hawkley-heavy.json node; the imported pod facts in corpus/eth-refutation/hawkley/runs/runpod-dumwx3gz82jcvf | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | 7c88e9465fd439b4… |
| certs/eth-cslib-d1.json node; the imported pod facts in corpus/eth-refutation/cslib/runs | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | 73f02f389c226bd7… |
| certs/eth-chain.json node; the imported pod facts in corpus/eth-refutation/chain/runs | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | a6291d9300aa7a5a… |
| certs/eth-openai-chain.json node; the imported pod facts of both runs in corpus/eth-refutation/openai-chain/runs | 1 row 1 CERTIFIED | node tools/ < 1 s | — | — | 8fdc50bc1a14b073… |
| certs/wsp-baseline.json python3 standard library; the cached generations under corpus/wsp/.cache/baseline-runs; node for the second grader | 1 row 1 MIXED | python3 -I tools/ 3 s | — | node tools/ 3.5 s | 27cbeeb6082d6877… |
| certs/claims-intake-2026-11-08.json node; python3 standard library; the pinned inputs under corpus/claims-intake/inputs (ThetaEvolve @ 7c12898, Apache-2.0) and corpus/einstein-arena/best-7.json | 4 rows 2 CERTIFIED, 2 REFUTED | node tools/ 11.4 s | python3 -I corpus/claims-intake/circles/check.py 3; python3 -I corpus/claims-intake/circles/check.py 5; python3 -I corpus/claims-intake/autocorr2/check.py; python3 -I corpus/claims-intake/pnt/check.py 4.3 s | — | c5afbcacdf0b32f7… |
| certs/claims-intake-7-2026-11-08.json node; python3 standard library; the pinned input under corpus/claims-intake/inputs (ThetaEvolve @ 7c12898, Apache-2.0) | 1 row 1 CERTIFIED | node tools/ < 1 s | python3 -I corpus/claims-intake/issue-7/check.py < 1 s | — | c6efa76e70af3dcf… |
Runtimes are measured — so they carry the dashed underline: one machine, one day, nothing decided them — every command executed on 2026-11-08 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 | re-run by another party |
| 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 | re-run by another party |
| 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 the partner group pair (the university; 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 |
| the maintainers of Lean's kernel checkers (con-leche, con-ron, nanoda, lean4lean) | their checkers ran on this export, public with a DOI since 2026-11-05; con-leche's maintainer asked for the runs | eth-openai-chain · CERTIFIED 239 MB, one checker, 64 GB, about 2 minutes | 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 | 118 |
| 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 | 2 |
| 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 | 6 |
| 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 | 2 |
| 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 | 2 |
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/ not a register row (a lab theorem) | own- | the same verdict; three documentation findings in the write-up, folded in (commit 1c248ca) | code · posted |
| maximusrufus (GitHub) | 2026-10-23 | Twelve register rows re-decided with their own exact code, at cert-machine aa52e8d (Linux): the kissing configurations of AlphaEvolve (593) and EinsteinArena (594, 604); the sum–difference certificates of 3b (13 points) and 3c (147 and 95 points), agreeing to 30 digits; and six EinsteinArena constructions — two circles-in-a-rectangle (with the 44 overlapping pairs of the as-published Together AI packing), two Heilbronn convex, two min-distance ratios. A duplicated vector and moved probability weight are rejected by their check as by ours. register rows: kiss- | own- | the same verdict on all twelve rows, no disagreement; two findings, both answered on the thread | code · posted |
| maximusrufus (GitHub) | 2026-10-23 | The three ledgers re-derived with the tools that write them, at cert-machine aa52e8d (Linux, Python 3.14.4, Node v22.11.0); verify_sumdiff.py run beside the sum–difference ledger, its false-bound control firing. records: certs/ | full- | every verdict and count identical | code · posted |
| JeetuSK0808 (GitHub) | 2026-10-24 | The registry’s two C₃₁ rows (Lueker’s automaton at h = 9 and h = 10), our replay of reports/ records: certs/ | own- | the same verdict on both rows; their bounds a little looser (vectors stopped once certified); their independence confirmed on the thread 2026-10-27 | code · posted |
| JeetuSK0808 (GitHub) | 2026-10-24 | The registry’s C₈₄b correction (reports/ register rows: optconst- | own- | the same verdict; their 0.00071385 is the maximum, our 0.0007150508 a ceiling above it (answered on the thread, where we printed 0.0007150507: the ceiling truncated, rounded outward since 2026-10-24) | code · posted |
| maximusrufus (GitHub) | 2026-10-24 | The registry’s C₄₂ record (certs/ register rows: optconst- | full- | the same verdicts (PARTIAL); the three defects fixed, recorded in the self-audit’s amendment of 2026-10-24 | code · posted |
| maximusrufus (GitHub) | 2026-10-24 | Google’s AlphaEvolve Ramsey lower-bound graphs decided with their own clique search (two methods), before ours and with no code of ours: 15 of the 18 graphs, the verdicts compared with certs/ records: certs/ | own- | the same verdict on all 15; R(10,12) and R(7,13), which they could not finish, decided here; R(8,18) unfinished on both sides | code · posted |
| arhancanli (GitHub) | 2026-11-11 | R(3, 33) ≥ 241, JeetuSK0808’s circulant certificate, which we re-decided on 2026-10-27 (the outside row of certs/ records: certs/ | own- | the same verdict: no triangle and no independent 33-set, through the same eight multipliers and the same 31 orbits | 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.
The same list as premises, in the order a verdict travels through them, each with the rung its checking reached:
Every decision is exact given these; the weakest premise is assumed, and on most rows it is the last one. An outside rerun with its own code is the one thing that moves it, which is why §5 counts them and never declares them.