An evaluation graded against reference values inherits the failure class of whatever computed them — and for mathematical ground truth the computing pipeline is usually floating point, checked by digit agreement. This note holds three certified specimens of answer keys going wrong in ways reruns and digit cross-checks provably cannot catch, one published claim the same instruments CONFIRM — a control, because an audit that only ever refutes is not an audit — and one working design that removes the answer key altogether. Every specimen was re-proved during the build that produced this page.
Both bars are published values, and both are wrong — in opposite directions. One stops being correct just past the reach of a hand-check; the other stays correct far past the reach of any float screen and is still not the thing it claims to be.
The reference values in mathematical answer keys are computed — by scripts, by CAS calls, by a model run once and trusted. When the pipeline is floating point, its silent failures become the key's silent failures, and the usual defenses do nothing: a RERUN of the same pipeline reproduces the same artifact bit for bit, and a DIGIT CROSS-CHECK against an independently computed float value agrees, because both pipelines drop the same mass the same way. The failure class lives inside the key, and a model that reproduces the artifact grades as correct — while a model that computes the true value grades as wrong.
This is not hypothetical. Each section below is a certified specimen from this site's audits — re-proved, not cited, during this page's build.
A GPT-published constant on Erdős #852 — an Euler product over primes — is wrong from its 12th significant digit. The wrong digits are not near the truth by accident: re-run live during this build, the naive double-precision product over 148,932 primes emits 0.0752403861777419 — the published value, digit for digit — because 87.5% of its factors round to exactly 1.0 and silently vanish. The exact partial product, a strict lower bound with no tail estimate needed, already exceeds the printed value: REFUTED, re-decided this build. The published constant is the bug, printed.
If that number sat in an answer key, every float-faithful model would score correct and every exact model would score wrong. The full mechanism, the certified correction, and the failure taxonomy are in the Erdős #852 report; this is its §6 argument, promoted to a page of its own.
Validating a key by matching digits assumes agreement implies identity. The impostor catalog is the certified counterexample set: 21 published constants that agree with simple closed forms — and are provably not equal to them, each refutation one exact BigInt comparison at the full published precision. The deepest specimen (A271880, re-derived this build) agrees with a plain rational for 62 significant digits before exact arithmetic separates them. Any digit-matched validation shallower than that certifies the impostor; twenty digits — a "discovery" threshold elsewhere — is not close. Agreement depth is evidence about your precision budget, never about identity.
The subtlest class: the key is wrong even though the computation behind it was right. The Ramanujan Machine's 2022 mixed-zeta sheet prints an identity that is FALSE as printed — a sign slip in the constant term, one of three typographic errors on the sheet — while the continued fraction its own polynomials define converges to the corrected value exactly: both directions re-certified on one enclosure during this build. No rerun of the discovery pipeline catches this, because the pipeline was never wrong; the print is. A key transcribed from a paper inherits the paper's typos as ground truth, and a model reproducing the (correct) computation grades as wrong against the (false) print.
Every specimen so far is a key that went wrong, which is exactly the reason this one is here. An instrument that returns REFUTED on everything it is pointed at is not an audit, it is a search — and the taxonomy of answer keys is not complete without the case where the published value is right and the audit says so. This site's third audit domain supplies it. Alongside tensor decompositions and continued fractions there is an exact rational sum-of-squares certifier, aimed at control theory, and pointed at a 2026 paper's machine-DISCOVERED Lyapunov functions it returns CONFIRMED. The paper held up. That is the headline, and it is a stronger result for this machine than another refutation would have been.
arXiv:2606.10045 reports Lyapunov functions found by constrained symbolic regression for the nonlinear system it gives as Eq. 17,
The instrument re-derives V̇ = ∇V · f symbolically over the rationals — Python's fractions and nothing else, no floating point anywhere in the decision — and then demands an exact sum-of-squares certificate rather than a numerical minimum. For the function the paper states as valid, V = x1² + 4·x2², it gets one:
The cross term is not small, it is absent: the coefficient 4 is what annihilates it exactly. What is left is a weighted sum of squares whose only zero is the origin, so V decreases along every nonzero trajectory and the system is globally asymptotically stable — decided, not estimated, and re-derived during the build that produced this page. The method is classical (Lyapunov 1892; SOS-Lyapunov, Parrilo 2000) and the function is the paper's. Nothing here is ours except the re-verification.
The same run also refutes the 3 under-sampled candidates the paper reports — and the paper flags them itself. Its Eq. 23, V = x1² + 3.97·x2², is stated in the paper as having an incorrect coefficient; the instrument supplies the exact witness that sentence implies. At the rational point x = (3/200000, 1/1000) the derivative is
— a positive rational, checkable by hand, with no tolerance anywhere in the statement. V increases there, so V is not a Lyapunov function for that system, full stop. The coarser candidates fall the same way: V = x1² + 2·x2² at (1/1000, 1/1000) gives V̇ = 499999/250000000000, and V = x1² + 3·x2² at (1/2000, 1/1000) gives V̇ = 249997/500000000000. This is corroboration of the authors' own statement, not a catch — they wrote down that the coefficient was wrong, and the machine wrote down the number that proves it. What exact arithmetic adds is the distinction the paper is already drawing. The coefficients are not "approximately right" and "nearly right": 4 is exactly right and 3.97 is exactly wrong, and no float screen anywhere in the neighbourhood of a derivative the size of 22103/50000000000000 would tell you which was which.
The third outcome is the one that makes the other two worth anything. The same certifier, run on the Motzkin polynomial x1⁴·x2² + x1²·x2⁴ − 3·x1²·x2² + 1 — nonnegative for every real x1 and x2, and famously (Motzkin 1967) not a sum of squares — returns REFUSED. It declines to certify a statement that is TRUE, because the certificate it requires provably does not exist for it. It prints the probe M(1,1) = 0 beside the refusal so the refusal reads as what it is: a refusal to certify, never a claim of falsity. That is the honest behaviour and not a bug. A checker that fudged Motzkin through would be certifying by wishful thinking, and its CONFIRMED on the Lyapunov function would then be worth exactly nothing.
| verdict | object | the exact reason |
|---|---|---|
| CONFIRMED | V = x1² + 4·x2², the paper's stated valid function | V̇ = −2·x1² − 8·x2⁴ — an exact weighted SOS, zero only at the origin |
| REFUTED | V = x1² + 3.97·x2², flagged as under-sampled by the paper itself | witness x = (3/200000, 1/1000) gives V̇ = 22103/50000000000000 > 0 |
| REFUSED | the Motzkin polynomial — nonnegative everywhere, and not a sum of squares | no SOS certificate exists, so none is issued; the instrument declines a true statement rather than guess (probe M(1,1) = 0) |
Read the three as a set, because separately none of them is the argument. One machine-discovered result confirmed exactly. The paper's own flagged candidates refuted with rational witnesses. One true statement refused for want of a certificate. Three verdicts, three different reasons, one instrument that can reach all three — which is the only condition under which the first one means anything. For an evaluation builder the transfer is direct: a grader you have never seen decline is not known to be able to decline, and a grader that cannot decline will eventually confirm your answer key back to you.
This section is its own gate. The three programs ran during this build, each exited 0, and together they reported 19 PASS rows and no failures — including the red controls that must fire (a corrupted certificate refused, an overclaimed bound refuted at x = 1, and an unstable perturbation whose witness gives V̇(1,0) = 2 > 0). If any one of them fails or stops printing ALL PASS, this page is not written at all. Run them yourself from a clone — stdlib only, no SDP solver, no dependencies:
python3 instruments/sos/reverify_ai_lyapunov.py python3 instruments/sos/sos_verify.py python3 instruments/sos/lyapunov_cert.py
All three are also rows in make test, so they run on every battery, not only when this page is built. The exact global lower bound in the second one — a quartic certified at ≥ 5 by an exact SOS decomposition, the bound attained — is the same instrument doing the ordinary version of the job.
Published, not peer-reviewed, not independently rerun. arXiv:2606.10045 is cited as a CLAIM: its system, its Lyapunov functions and its own statement about the under-sampled coefficients are taken as printed, and every verdict above reads "given those equations". The mathematics is not ours — the Lyapunov functions are the paper's, discovered by its method, and the SOS-Lyapunov technique is Parrilo 2000 on Lyapunov 1892. No priority is claimed for anything in this section; it re-verifies someone else's result exactly and reports that it holds.
The structural fix is to grade tasks where no reference value exists to contaminate: ask the model to EXHIBIT a witness — a decomposition, a certificate, a construction — and let the grader re-derive the claim from the witness alone, exactly. The matmul eval on this site is the running instance: 364 frontier-model proposals graded to date, every certified row a theorem, every refuted row a proof of error, zero false certifications — measured, and structurally guaranteed, because there is no answer key to be wrong.
Three rules transfer to any evaluation built on computed ground truth. Screens may only PRUNE: no float comparison ever admits a claim. Grade with certificates, not tolerances: the verdict should be checkable by re-derivation, not by proximity to a stored number. And put red controls in the grader: deliberately false submissions that must fail, run before anything real is graded — a grader that has never rejected a forgery is not known to reject forgeries. The methods note states the discipline in full; every gate on this site runs under it.