cert-machine · a repository's finite layer, decided twice

The cryptids audit: a repository's finite layer, decided twice

What a producer's checker checks, and what it does not

google-deepmind/cryptids publishes small Turing machines whose halting encodes Goldbach, ZF consistency and the Riemann Hypothesis, with Lean proofs of the state reductions and a standard-library checker of its own, verify.py. The theorems are the kernel's. Underneath them is a finite layer — pinned tables, digests, state and cell counts, the step at which a bootstrap ends and the configuration it ends in, ratios printed to their digits — and that layer can be decided exactly from the bytes. It was decided here twice, at commit 664cd03904a8…: once by hand, one lane written for this source, and once through claimbox, the claim-machine, with the receiver's decider for machines. The gaps come first.

Published, not peer-reviewed. Nothing here verifies a halting equivalence, a non-halting proof or the semantics; those are the Lean kernel's, and the kernel lane below only re-checks the build, the stated theorems and the axioms under a second kernel. The two arms were run by the same agent, the hand lane first, so what it learned about the source was available to the other; the pre-registration says so. The repository's authors were not contacted before this page; the asks are in the gaps.

tl;dr

The finding. 8 gaps in the repository's finite layer, found by reading verify.py and confirmed by running. The checker never builds Lean and tests theorem statements by substring; its riemann_104 check says it runs riemann_120 and never does; it records the proof files' digests and compares them to nothing; one write-up counts "non-halting transitions" by one convention and another by the other; the riemann_104 checkpoint table prints steps at "checkpoint k" without saying which event k counts (the printed steps are root entries, the 179th, 210th, 879th and 1,721st, not the 100th, 116th, 500th and 1,000th). Everything else the finite layer prints holds: 143 of 152 claims CERTIFIED by hand, 95 of 107 through claimbox, 124 of 128 paired claims with the same word.
The mechanism. Every table parsed, every upstream source compiled under the stated convention, every machine simulated from the blank tape in exact integers — by two implementations that share no code in each arm. A claim is one of three words: CERTIFIED with the certificate, REFUTED with the witness, REFUSED with the rule and, where there is one, the threshold that would change the word.
Check it. node tools/build-cryptids-benchmark.js --check recomputes the comparison from the two arms' records; node tools/run-cryptids.js re-derives arm H's rows in JavaScript; python3 instruments/claimbox/tm.py --decide and tm.js re-decide claimbox's objects; make drift re-hashes the repository's copy against its pin.

claims by hand

152

143 CERTIFIED · 1 REFUTED · 8 REFUSED, each with its rule

claims through claimbox

107 + 22

107 objects written, 106 admitted by the checker; 22 sentences refused by the grammar with the rule

paired claims

124 of 128 agree

4 differ: one digit-grouped decimal the receiver does not read, three counts it has no decider for

planted defects caught

10/11 · 9/11

by hand · through claimbox; the miss in both: a proof file nothing pins. The green control (a comment) moved nothing.

gaps

in the producer's checker and its write-ups, dated at the pin; 4 with every related claim decided

§1 · the gaps

What verify.py does not check, and what the write-ups print loosely

The producer's checker is a careful piece of work: it pins five upstream sources and their derived tables by sha256, re-derives each table from its source in three formats, checks that the Lean definitions load the right files, and replays bootstraps and lockstep checkpoints. What follows is what it does not do, read before any run and confirmed by running; each row names the claims here that decide the matter.

gap	status	decided by
verify.py never builds Lean and checks theorem statements by substring	confirmed by reading; the kernel lane decides the build and the axioms (certs/cryptids-kernel.json)	challenge-states-all cert challenge-states-constructive cert
the riemann_104 check never runs riemann_120 although its docstring says it does	confirmed by reading; the stage run here: riemann_120 does not halt within its printed 89,775,610-step bootstrap, and the write-up's reference column is REFUSED because the root event is not stated in finite terms	riemann-120-no-halt-boot-length cert riemann-120-checkpoint-table open
the proof files' sha256s are recorded and compared to nothing	confirmed: no pin exists; the recall plant in a proof file flips no word in either arm	verifypy-proof-hashes open
the Goldbach message says 92 cells checked where the code checks 42	confirmed by reading verify.py (verify_goldbach_proof_tables: the message counts candidate and edited cells, the loop runs over the 42 candidate cells); both arms check the 42 under the write-up's map	goldbach-embed cert
two ZF boot checkpoints (39,753 / state 64 and 39,773 / state 99) are used without explanation	measured: both hold; step 39,773 is not an entry into state 64, so the two are different events twenty steps apart	zf-393-39773-state-99 cert zf-39773-is-not-state-64 cert
the simulations stop at 250,000 steps	confirmed; the ten-million-step correspondence and the 89,775,610-step run were done here	zf-overhead-10m cert riemann-120-no-halt-boot-length cert
the ZF write-up's "785 → 759 non-halting transitions" and the riemann_104 write-up's "238 → 207" count by two conventions	found by both arms: the ZF numbers are the non-halting cells plus one (the explicit halt line is counted), the Riemann numbers are the non-halting cells	cells-zf dep
the riemann_104 checkpoint table's "checkpoint k" is not defined in finite terms	found by both arms: the printed candidate steps are root entries (the 179th, 210th, 879th, 1,721st), not the 100th, 116th, 500th, 1,000th; REFUSED with the threshold: publish the selection rule	riemann-104-table-steps-are-root-entries cert riemann-104-checkpoint-k open

The asks. Publish the selection rule that makes a root entry a "checkpoint", and the four candidate rows and five reference rows of the riemann_104 table become decidable from the bytes. Say which state of riemann_120 is "main.0" and the reference bootstrap length, 89,775,610 steps, can be decided too (the machine runs that far without halting; what it is in at that step is recorded). Pin the proof files' digests, or drop the lines that record them. Use one convention for "non-halting transitions". Run riemann_120 in the check that says it does.

§2 · by hand

Arm H: one lane for one source

The way cert-machine audited sources before claimbox existed: tools/run-cryptids.py, standard library, exact integers, its own parsers for the canonical table and the three upstream formats, its own simulator. It states each claim in the auditor's prose with the file it is about, that file's sha256, the quote where there is one (53 of 53 found byte for byte), what was computed and one of three words. tools/run-cryptids.js, a second implementation sharing no code, recomputes every decision-bearing row; the battery refuses on a disagreement.

class	certified	refuted	refused
count	27	1	1
hash	38	0	1
derivation	13	0	0
lean-def	18	0	0
structural	4	0	0
arithmetic	12	0	0
checkpoint	18	0	3
runtime	10	0	0
statement-string	3	0	0
kernel	0	0	3

The one refutation. the ZF reduction takes 785 non-halting transitions to 759, computed [784,758] against [785,759]. each ZF table has two halting cells: the explicit halt line of the source and one (state, symbol) pair the source never defines; the printed counts are the non-halting cells plus one, i.e. the transitions the source defines including the one that halts — the riemann_104 write-up counts the other way (238 and 207 are non-halting cells exactly), so the two write-ups use two conventions for one phrase

The refusals, each with its rule.

core-transitions-goldbach. no definition of "core" is printed; the table has 49 and 41 non-halting cells; the claim is not decidable from the bytes until "core" is defined
riemann-104-checkpoint-k. the event "checkpoint k" is not defined in finite terms: the printed steps are root entries, but the 179th, 210th, 879th and 1,721st, not the 100th, 116th, 500th and 1,000th; which root entries count as instruction checkpoints is the register machine's abstraction and is not printed. Publish the selection rule and the four rows become decidable from the bytes
riemann-120-checkpoint-table. the root entry is named by a register-machine state (main.0), not by a state of riemann_120, and "checkpoint k" is not defined in finite terms (the candidate column above); publish the state of riemann_120 that is the root and the selection rule, and the column becomes decidable — the stage verify.py says it checks and never runs
kernel-all-proofs. a theorem, not a finite claim: the Lean kernel is the authority; the kernel lane re-checks the build and the axioms as stated (a concordance), this lane does not
kernel-equivalences. a theorem, not a finite claim: the Lean kernel is the authority; the kernel lane re-checks the build and the axioms as stated (a concordance), this lane does not
kernel-holdouts. a theorem, not a finite claim: the Lean kernel is the authority; the kernel lane re-checks the build and the axioms as stated (a concordance), this lane does not
riemann-104-register-values. the encoding of the five registers on the tape is not stated in finite terms in the write-up; the step counts are decided above, the register values are not
verifypy-proof-hashes. recorded and compared to nothing: no pin exists for the proof files in verify.py or PROVENANCE.md, so there is no claim to decide; a plant in a proof file flips no word (recall plant 10)

What the long runs decided. zf_380 after 10,015,814 steps has the tape and head zf_393 has after 10,000,000 steps (the write-up's step overhead, read as a configuration correspondence): CERTIFIED. riemann_120 does not halt within 89,775,610 steps, the length the write-up prints for its bootstrap: CERTIFIED. each candidate step the write-up's checkpoint table prints (26,093; 28,934; 165,200; 498,382) is a step at which riemann_104 enters its root state 19: CERTIFIED; they are the 26,093 → 179th, 28,934 → 210th, 165,200 → 879th, 498,382 → 1,721th entries, counting the boot entry as the 0th.

§3 · through claimbox

Arm C: a reader, the grammar, the receiver

claimbox's reader (claimbox/readers/cryptids.py) turns the sentences the sources print — the provenance table, verify.py's pinned constants and assertions, the write-ups — into jobs, each with the quote byte for byte and the file it is about; the grammar's new machine family states the claim or refuses it with a rule; the translator writes the object; cert-machine's decider for machines (instruments/claimbox/tm.py, with tm.js held to it) decides the named functions over the pinned bytes; the ratios and percentages are exact expressions the checker decides from the object alone; and the checker (instruments/claimbox/check.py) admits or refuses every object: 106 admitted, 1 refused (ratio-riemann-104-boot: a digit-grouped decimal, 9,934.23, which the receiver's printed-bar rule does not read).

named function or expression	certified	refuted	from the object / refused
canonical_sha256	17	0	0
states	15	0	0
nonhalting_cells	5	2	0
derived	9	0	0
stage_entry	4	0	0
embeds_into	1	0	0
halting_cells	1	0	0
no_halt	10	0	0
arithmetic	9	0	1
sha256	21	0	0
after	5	0	0
entries	3	0	0
same_tape_and_head	3	0	0
same_tape_and_head_at_entries	1	0	0

Refused by the grammar, 22 sentences. 10 ambiguous, 9 unbounded, 3 decider: the eight halting equivalences and the kernel sentence (unbounded: the kernel is the authority), the "core" transitions (no definition), the nine "checkpoint k" rows (no finite definition of the event), the counts of markdown rows and JSON names (no decider).

§4 · the comparison

The two arms on the eight metrics

Fixed before the run (notes/cryptids-benchmark-preregistration-2026-10-23.md): what each arm states, how it pins, how it refuses, what it catches when the input is planted with defects, whether the two agree, what each cost, and what a reader must trust. The eighth, the producer's checker, is §1.

metric	by hand	through claimbox
M1 claims stated	152 rows: 143 / 1 / 8	107 objects (95 / 2 by the receiver, the rest from the object) + 22 refused by the grammar
M2 pins	53 of 53 quotes verbatim; every row names a file and its digest	107 of 107 objects with a verbatim quote and the pin of the bytes: the format refuses otherwise
M3 refusals with a rule	8, the rule in prose on the row	22 by the grammar (a named rule each) + 1 by the checker
M4 planted defects	10 of 11 caught; green control quiet; the miss: the proof file nothing pins	9 of 11 caught; green control quiet; misses: 10-proof-file, 11-theorem-removed
M5 concordance	124 of 128 paired claims agree	4 differ: ratio-riemann-104-boot (CERTIFIED / REFUSED); comparator-count-all (CERTIFIED / REFUSED); holdouts-BB6 (CERTIFIED / REFUSED); holdouts-BB33 (CERTIFIED / REFUSED)
M6 cost	18.3 s for the full run; 681 lines tools/run-cryptids.py, 172 lines tools/run-cryptids.js, 127 lines tools/run-cryptids-recall.py	17.8 s to decide, 0 s for the checker; 425 lines instruments/claimbox/tm.py, 164 lines instruments/claimbox/tm.js; reused: the format, both checkers, the batch and record machinery
M7 what an outsider must trust	2 files by one author; no checker outside them	4 files; the checker shares no code with the reader and refuses objects whose quote, pin or record is wrong

Reading it. The hand lane reaches further: it states 46 claims the reader has no object for (its own measurements, the Lean-definition and statement-string checks, the counts the receiver has no decider for) and it supplied readings where the write-ups are loose. The claimbox lane is the one an outsider can check without reading the auditor: every object carries the quote, the pin and the record, and a checker that shares no code with the reader accepts or refuses it. On the claims both state, the words agree except where the receiver's format or decider surface falls short, which is a measurement of the receiver, not a disagreement about the repository. The same two findings, the counting convention and the checkpoint event with no finite definition, came out of both arms.

§5 · the kernel lane

The build, the stated theorems and the axioms, under a second kernel

The repository at its pin, built with its own toolchain (Lean v4.35.0-rc4) and the Mathlib cache, then audited by leanprover/comparator at the matching release with nanoda on, using the configurations the repository ships. A CERTIFIED row is a concordance with the repository's own CI; it verifies no mathematics.

configuration	theorems	permitted axioms	kernels	time	word
all	22	propext, Quot.sound, Classical.choice	Lean default kernel accepts the solution; nanoda kernel accepts the solution	398 s	cert
constructive	10	propext, Quot.sound	Lean default kernel accepts the solution; nanoda kernel accepts the solution	101 s	cert

§6 · what is claimed, and what is not

The limits

Claimed. For each finite claim the sources print, a decision from the bytes at the pin by two implementations that share no code, with the reading stated where the auditor supplied one; the gaps of §1, each decided or refused with its rule; the comparison of the two arms on the metrics fixed before the run.
Used, not re-proved. The Lean kernel's acceptance of the proofs, and comparator's check that the stated theorems are the proved ones; the compilation convention the provenance file states; the checkpoint pattern verify.py states for the Goldbach stages.
Not claimed. Any halting equivalence, non-halting proof or semantics; that the "core" transitions, the "checkpoint k" events or the register values mean anything in particular; that the holdout machines are cryptids (the community's word).
Independence. From the repository, whose checker was read but never run as evidence; not from the operator (one), and not between the arms (the same agent, the hand lane first).