The Ramanujan Machine, audited

The July 2022 sheet ("Results using mixed orders of ζ") prints, as its third row, the identity 2/(2ζ(5) − 2ζ(3) − 1) = CF, where the continued fraction is defined by the row's own polynomials a_n = n⁵+(n+1)⁵+6(n³+(n+1)³)−4(2n+1), b_n = −n¹⁰. The printed left-hand side is -1.5035… — negative. The continued fraction converges to 2.9862258661092707…, certified here by a proved tail band to width 8.9e-16. The two are provably disjoint: the printed identity is false.

The mechanism is a sign slip, and the audit proves it constructively: the same certified enclosure contains 2/(2ζ(5) − 2ζ(3) + 1) — the printed constant term −1 should read +1 — so the corrected identity survives on the very enclosure that refutes the printed one. (The sheet's displayed convergent also shows a₁ = 275 where the row's own polynomial gives 75, and reuses n⁸ numerators on rows whose b_n is −n¹⁰ or −n¹⁴; the polynomial column is the mathematical object, and it is what this audit decides.)

SURVIVES: the claimed closed form lies inside a rigorous enclosure of the continued fraction, with the final comparison made in exact rational arithmetic — consistency certified to the stated width, typically 1e-14 to 1e-15. It is NOT a proof of equality; no finite enclosure proves an identity, and no row here is marked proved unless the literature proved it. REFUTED: the claimed value lies provably OUTSIDE the enclosure — that verdict is a theorem. A row the instrument cannot decide is REFUSED and never counted either way; this build refuses to ship if any row refuses.

Method, by sheet: positive continued fractions are evaluated backward in interval arithmetic from a tail seeded by proof (never by assumption). The minus-CF sheets (zeta(3), Catalan, pi², ln 2, mixed orders) ride a per-row TAIL BAND [L(n), U(n)] proved by shift-and-check coefficient positivity, with convergence proved inside the certificate — no external convergence theorem is consumed. Constants come from their defining series with proved tails (zeta(3), zeta(5), zeta(7), Catalan's G with an exact convexity bound) or from certified Machin enclosures (pi², with Euler's identities named where consumed). Every sheet PDF is hash-pinned and re-hashed at certify time: the certificate is over a byte sequence, not a memory of it.

The Ramanujan Machine publishes conjectures found by matching truncated decimals, argued from collision probability — its papers say so plainly, and its own Ramanujan Challenge (July 2026) now asks for "reproducible CAS-based or formally verified code". This page is that verification, applied to the Machine's entire published output: every verdict is produced by an instrument with red controls that must fire, calibrated on proved rows (Apéry's 6/ζ(3); the two pi² rows proved by Kadyrov–Orynbassar) before being trusted on unproven ones, and re-run in full by the repository's test battery.

The registry updates as sheets appear. A future row that survives will be added as SURVIVES with its width; a future row that fails will be added as REFUTED with its mechanism — this build refuses to render either without the certificate.