cert-machine · the claims desk

Send us a claim

A mathematical claim that comes down to finitely many exact arithmetic facts can be decided here — certified with a certificate that re-runs without this engine, refuted with the falsifying witness printed, or honestly refused. The verdict is published whichever way it falls, and we never run the claimant's code.

The queue is open and EMPTY: 0 claims have been submitted so far. Every row in the ledger below was self-initiated — we chose the claim — and the page says so rather than implying a busy desk. That distinction is the first thing this desk would want measured about itself.

tl;dr

The finding. 18 published claims decided so far, all self-initiated: 14 CERTIFIED, 1 PARTIAL, 1 REFUTED, 1 NEEDS DATA, 1 MIXED, with 1 queued and not yet decided — queued is not decided, so it is counted separately. Each row is derived from the record that decided it — a claim with no record gets no row.
The mechanism. The instrument returns THREE verdicts and no fourth: CERTIFIED and REFUTED are theorems, REFUSED is what a claim gets when this instrument cannot decide it — a real outcome, published like any other, and not evidence either way. The other labels in the ledger are COMPOSITIONS of those three, not extra verdicts: PARTIAL is a certified fragment beside a refused core, and names which is which; NEEDS DATA is a refusal whose reason belongs to the claimant (the bytes were never published); MIXED is an aggregate row whose record holds both a certification and a refutation.
Check it. Submit through the claim form. Everything decided is on this page, and every verdict links to the record it came from.

claims decided

Each derived from the record that decided it: 14 CERTIFIED · 1 PARTIAL · 1 REFUTED · 1 NEEDS DATA · 1 MIXED. A further 1 is queued and deliberately not counted as decided.

submitted by others

The queue is open. Until this number moves, everything on this page is work we chose ourselves, and saying so is the point.

claimant code run

Independence is from the CLAIMANT: their code is never in the trust path. Every decision is re-derived from the published statement and bytes.

verdicts available

CERTIFIED · REFUTED · REFUSED. A claim outside the boundary is refused rather than guessed at, and the refusal is published.

§1 · the boundary

What can be decided here, and what cannot

In scope. claims that come down to finitely many exact arithmetic facts — exhibit a witness, verify an identity, bound a quantity, decide a constant. Everything else is REFUSED as out of scope rather than guessed at.

A constant, to stated digits. Exhibit the value; the instrument brackets the true quantity in exact arithmetic and compares. This is how a published constant was refuted at its twelfth significant digit.
An exhibited object. A configuration, a decomposition, a construction — anything whose correctness is finitely many exact checks on the bytes you publish.
An identity or inequality over a finite set. Every case decided exactly; no sampling, no tolerance, no "checked at 10,000 random points".
The computational part of a published proof. Named as such: the fragment is decided and the analytic core is left alone, with the page saying exactly which is which.
OUT of scope, and refused rather than guessed at. Asymptotics, statements over infinite families with no finite reduction, and proofs whose content is prose. A refusal here is a statement about this instrument's reach, not about your claim.

§2 · how

What to send, and what comes back

Open a claim issue with the statement, where it is published, and — if you have one — the witness or the exact bytes. Unpublished claims are welcome; say so and they are labelled that way.

What comes back is one of the three verdicts with its evidence attached: a certificate that re-runs on stock Python with no engine present, a printed falsifying witness, or a stated reason for refusing. It is published on this site, added to the ledger below, and linked to the record that produced it. If the claim is yours and the verdict goes against it, that is still what gets published — and if you can refute one of OUR results, the same applies in the other direction.

the one thing this desk will not do

Run your code. Independence here means independence from the claimant: the decision is re-derived from the published statement and the published bytes, and the claimant's program is never in the trust path. That is the whole reason a verdict from this desk is worth more than a re-run of your own pipeline.

§3 · the ledger

Every claim decided, and by what

claim	claimant	verdict	what was actually decided	where
Maxwell's point-charge bound	a manuscript produced with frontier-model help	CERTIFIED	at ε = 1/6 only	the record
The Korenblum constant	a manuscript produced with frontier-model help	CERTIFIED	the numerical criterion	the record
Erdős Problem #1038	a manuscript produced with frontier-model help	CERTIFIED	the computational fragment	the record
Ran–Teng Conjecture 20	a manuscript produced with frontier-model help	PARTIAL	machine-checkable fragment only	the record
The Mathieu property for Lie groups	a manuscript produced with frontier-model help	CERTIFIED	supporting identities only	the record
The rank-two Poisson conjecture	a manuscript produced with frontier-model help	CERTIFIED	the explicit counterexample	the record
C* for Erdos #852, published as 0.0752403861777 with no error bound	a problem thread post produced with frontier-model help	REFUTED	the constant itself, to its printed digits	the record
K(4) >= 24 — exact value, Musin 2003	classical (generated here)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(8) = 240 — exact value, Levenshtein / Odlyzko–Sloane 1979	classical (generated here)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 593 — the May 2025 record	AlphaEvolve (Novikov et al., DeepMind)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 594 — the solved n=594 rung, score-0 winner (solution #1492)	EinsteinArena agents (Bianchi et al. platform)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 604 — configuration 1 of three	The Station agents (dualverse-ai)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 604 — configuration 2 of three	The Station agents (dualverse-ai)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 604 — configuration 3 of three	The Station agents (dualverse-ai)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 582 — the pre-2022 record shell, integer norm-4 maximum (Lean-proved maximal by the Station)	classical (Best 1977 class; bytes from the Station bundle)	CERTIFIED	the configuration as published, in exact arithmetic	the record
construction device: 604 integer D12 vectors whose oblique shadow is configuration 3 (also a valid 604-point direction set in R^12)	The Station agents (dualverse-ai)	CERTIFIED	the configuration as published, in exact arithmetic	the record
K(11) >= 604 — the paper's headline result, credited by Cohn's reference table (2026-06-22)	EinsteinArena (Bianchi, Kwon, Pappu, Zou — arXiv:2606.10402)	NEEDS DATA	undecidable here: no public coordinates	the record
K(11) >= 592 — the 2022 record the AI ladder started from	M. Ganzhinov (arXiv:2207.08266, Highly symmetric lines)	QUEUED	the configuration as published, in exact arithmetic	the record
the published Ramanujan Machine result sheets, 52 printed rows	the Ramanujan Machine project	MIXED	51 rows survive their certified enclosure, 1 refuted exactly	the record

The scope column is the load-bearing one. "CERTIFIED" without it says something the record does not: several of these rows certify a computational fragment of a claim whose analytic core was never touched, and the row says which. One row is NEEDS DATA — a headline result whose coordinates have never been published, so it cannot be decided by anyone but its authors. That verdict measures the claimant, not the claim.