The language for claims an exact checker can decide

1. The sentence, the source, the bytesas the claimant printed and published them.
2. claimbox reads the shapeor names the rule it cannot state the claim under, before anything runs.
3. The objectthe pinned bytes, their declared reading, each bound as the exact rational its digits mean.
4. cert-machine’s checkera separate program, run on the object as it is.
5. One of three wordsCERTIFIED, REFUTED with the object that breaks it, or REFUSED with the reason.

A claimant’s lower bound, decided from the claimant’s own bytes

records/primitive-run.json · sha256 878538ead7a8. The printed bound is underlined dashed: a number someone printed, which nothing decided until the checker did.

One claim, two phrasings

records/riemann-run.json · sha256 d97286c2db9e · records/riemann-coverage.json · sha256 bdccf3410a6e.

data   M = artifacts/riemann_104/machine.txt   -- pinned: sha256 ac0c7e8a76679ba2a3f2c1814166b392c8301e51110a08bcd2c06624be35f25d
read   M as a (Q, 2) transition table
source V = verify.py                        -- the producer’s own checker

claim  "after 9,037 steps from the blank tape, artifacts/riemann_104/machine.txt is in state 19 with the head at -7, 19 nonzero cells"
       quote from V

$ claimbox check
means      run M from the blank tape for 9,037 steps: the state is 19, the head is at -7, 19 cells are nonzero
kind       finite: decided now
word       CERTIFIED   (cert-machine)
rests on   machine.txt as pinned, the definition “after”, the reading “(Q, 2) table”

records/cryptids-run.json · sha256 3504f66720c7.

One file, two readings, both decided

The claim: the 605 vectors of v form a kissing configuration in dimension 11, over 605 vectors pinned once.

records/fork-605.json · sha256 d7df6d6bc37f. The same pinned bytes, two exact answers: the reading belongs to the claim. A fork shows every reading's word; when the words differ it says split, and claimbox never merges them into one.

• Printed back. The “means” line is printed from the object cert-machine receives, by the grammar run backwards, never by a model. What is read is what is checked.
• Every number has an address: a line of a source or a pinned file. A number with no address is not a claim.
• Every reading is written down: decimal digits or IEEE doubles, exact or wrapping integers. The same file read two ways can give two different exact answers, so the reading belongs to the claim.
• Holes. A claim that cannot be stated exactly yet keeps a named hole: the bytes are not published, no decider exists for this quantity. A hole is not a verdict.
• Forks. An ambiguous claim is decided under every declared reading, and every word is shown; when they differ the fork is split, and said so.
• Watchers. A claim about every case is run as a watcher that halts on a counterexample, and reports “not refuted up to N”, never CERTIFIED.
• Rests on. Every word comes with the files, definitions and readings it depends on.

1. cert-machine is the only judge. claimbox never prints CERTIFIED or REFUTED on its own; it shows cert-machine’s word.
2. Say what is checked. The plain-words print-back comes from the object cert-machine receives, not from what was typed.
3. Every number has an address: a line of a source or a pinned file.
4. Every reading is written down. There is no default.
5. Anyone may propose; only checks count. People, models and search may write claims; a proposal is marked as one until it is validated, and two proposals count as two only when they are of different kinds.
6. Unclear is an answer. A named hole, or a fork with every reading decided.
7. Planted wrong claims in every feature, every one of which must be caught, with the results, misses included, published.
8. Never say more than was checked. CERTIFIED means this object, under this reading, holds on these bytes. It does not mean the sentence is true.
9. The trusted part stays small: the step from a claim to the object the checker reads is short enough to read in an afternoon.
10. cert-machine stays separate. claimbox sends it objects; a change there is made there first.

Columns are read from each run’s rows; a run whose own totals disagree with its rows refuses the page. ∅ marks an empty set.

Written down before the run

Of the AI-written claims about the Riemann certificate, 15 of 15 came out as the word written beside each before it ran; of the claims written for the Riemann test, 99 of 99. The false ones are REFUTED or not stated with their rule; the true ones are CERTIFIED.

From prose to claims, so far

Of the 80 AI-written phrasings, the grammar proposes 3 claims and a model, claude-opus-5-5, proposes 53; for the other 27 the model names a hole. A proposal is checked four ways: every number in it is found in its sentence, it reads back with the sentence’s relation, it moves exactly with the sentence when one digit of the bar is changed, and it compiles to the same object as the decided reference. Of the model’s 53 claims, 41 equal the reference field for field, 1 states the same bar printed another way, 2 state another claim their sentence also prints, and 9 have no decided reference to compare with. On a copy of the source with the bar moved, the model’s statement moved with it in 51 runs and did not in 2. cert-machine certifies 56 of the 56 claims proposed.

Each claim is then moved. With its bar one unit of the last digit up and down, a box must be refuted both ways and a bound must hold when weakened: 54 did so (failures: none); 17 of the bounds are tight to their last digit. Recompiled over planted copies of its bytes, 47 change cert-machine’s word and 9 do not: the decimal constant’s, which is arithmetic on a library constant and reads nothing from the file. Said another way, with the relation before the bar rewritten from symbol to words or back, the model stated the same claim 40 times, another claim 1 (a refusal), and nothing 2; the grammar reads none of the rewritten sentences (3). Where two kinds of proposer agreed, on 3 sentences, they agreed on the decided reference 3 times (on another claim: none).

Validated: 3, the sentences where two kinds of proposer agree. Proposed by one kind only: 46. Refused: 4, where a proposal fails a check; 2 of them fail the moved bar. The read-back reads a relation written in symbols, or in the words of a fixed table (“at most”, “does not exceed”, “below”), and numbers written in Lean’s notation; any other phrasing is refused, never guessed. Not stated: 27, each with a named hole. The model’s run took 184 calls and 1.1818 US dollars, under a cap of 20.

Helpers, begun

The first helpers propose claims by search, and cert-machine decides every candidate. Tighten finds the strongest bar it certifies beside a neighbour one unit stronger that it refutes: |D(1)| ≤ 0.823953160713, with 0.823953160712 refuted; over the rows, for every j in 0 < j < 256 : |256·S(j) - j| ≤ 1.837·10⁻⁴⁰, where the source prints 3·10⁻⁴⁰. From a refuted claim it walks the other way: the lower bound rounded up becomes C_1c(w) ≥ 0.41030211723. Extend reads further digits of a print cut off with an ellipsis, each the only digit that cert-machine certifies: c₁* = 0.753296067856070677…, and there it stops, because no digit is certified: the bytes do not decide the next one. Each is a proposal, quoted from the source the search wrote, and checked again as a claim in the language.

A watcher takes a claim about every case and decides it instance by instance, each instance cert-machine’s. Its results are a counterexample or “not refuted up to” a reach, never a certificate. Two planted twins, machines known to halt, must stop it exactly where predicted: the four-state busy-beaver champion at step 107, the five-state one at step 47,176,870. Over the Goldbach, Riemann and ZF machines it reports what it reached: not refuted up to 100,000,000, 100,000,000 and 100,000,000 steps.

The register’s sentences

Of cert-machine’s register, 97 of 132 sentences take a shape today. The rest are not stated: 22 print no quantity, 11 are prose, 2 are asymptotic. A refusal is a measurement, not a failure.

From prose to claims on the register: claimbox pins the bytes of 24 of its sentences, through the reader jobs the register was written from. The grammar states 23 of them: 16 are the same object as their job’s, and 7 have no decided object to compare with. The model, asked those 24 alone, states 19. cert-machine certifies 40 of the 42 claims proposed and refuses 2, where its own record’s word is not one it decides with. A decomposition named inside a file that prints many is written n["heading"], and a platform problem with no verifier written here is decided through the row cert-machine’s own decider wrote for those bytes. Validated: 19. Proposed by one kind only: 4. Refused: none. The rest name bytes claimbox does not pin (74) or are not claims the grammar reads.

What the planted defects missed

On the cryptids copies, two plants went through without a changed word:

• 10-proof-file: a proof file edited: no claim the sources print pins it.
• 11-theorem-removed: a theorem removed from a configuration file: counting its names has no decider.

Not new, and said so: three verdicts, published denominators, controlled languages and hash pinning all exist elsewhere. What claimbox puts together is a deterministic statement layer, printed back from the object; every number anchored; the reading declared and forked; an exact separate checker with three words; and the refusal rate published with planted controls.

• Faithfulness to an author’s intent is not established. The best methods of 2026 for checking a translation still accept some wrong statements. claimbox tests its translations with planted changes and publishes how many it refuses; it does not certify them.
• Two models agreeing is not independent confirmation. Models tend to make the same mistakes, so agreement counts only between proposers of different kinds, and is tested on planted sources.
• CERTIFIED is about an object, not a sentence. It means this object, under this reading, holds on these pinned bytes.
• “Not refuted up to N” is not evidence for every case. A watcher reports exactly how far it searched.
• Real-number identities are not decided in general. Only the forms the checker admits are decided; the rest are refused with the reason.
• A small checker can still be wrong. Keeping it small and separate shrinks what must be trusted; planted controls are how it is watched.

git clone https://github.com/carlostoledo1891/claimbox
cd claimbox
python3 -m claimbox shape "K(11) >= 593"     # the shape, or the rule that refuses it
python3 tests/battery.py                    # red controls, calibration, coverage, planted defects
python3 -m web.build --check                # rebuild this page and read every count again

• Gordon, Milner, Wadsworth (1979), Edinburgh LCF; Barendregt & Wiedijk (2005), “The challenge of computer mathematics”. A small checker is the only thing that decides.
• Pnueli, Siegel, Singerman (1998), “Translation validation”; McConnell, Mehlhorn, Näher, Schweitzer (2011), “Certifying algorithms”. Check each translation and each output, not the translator.
• Knight & Leveson (1986), on independently written versions failing together; Kim, Garg, Peng, Garg (2025), “Correlated errors in large language models”. Agreement is not independence.
• Fuchs, Kaljurand, Kuhn (2008), Attempto Controlled English; Ranta (2004), Grammatical Framework; Kuhn (2014), a survey of controlled natural languages. A readable syntax that parses one way and reads back.
• Bos (1996), Hole Semantics; Copestake, Flickinger, Pollard, Sag (2005), Minimal Recursion Semantics; Belnap (1977), a four-valued logic. Holes, forks, and a split that is not a refusal.
• Goldberg (1991), “What every computer scientist should know about floating-point arithmetic”; RFC 8259, on the precision of JSON numbers. The reading of the bytes is part of the claim.
• Mei & Douglas (2026), “Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization”; Zhang et al. (2026), “Beyond Compilation”; Ammanamanchi, Bhat, Biderman (2026), “Faults in Our Formal Benchmarking”. Preprints. Mechanical checks over judges; compiling is not faithfulness; the statements themselves carry defects.
• Nuijten et al. (2016), statcheck; Brown & Heathers (2017), the GRIM test. Printed numbers recomputed: the closest precedents.
• Stroebl, Kapoor, Narayanan (2024), on the limits of resampling with imperfect verifiers; Georgiev, Gómez-Serrano, Tao, Wagner (2025), mathematical exploration at scale. A proposal loop finds the loophole; exact checking closes it.
• Aaronson (2020), “The Busy Beaver Frontier”; Google DeepMind, cryptids (2026). Claims about every case, and small machines that encode them.