Certified three-colour Rado numbers for ax+by=cz with non-unit coefficients

Abstract

For positive integers a,b,c and r ≥ 1, the Rado number Rᵣ(ax+by=cz) is the least N such that every r-colouring of {1,…,N} admits a monochromatic solution of ax+by=cz. Several hundred values of R₃ are in print, and those not covered by a closed form are the output of a satisfiability solver reporting an unaudited verdict; as far as our search reached, no proof log accompanies any of them. We close that gap for seven equations. For each of 5x+3y=3z, 3x+3y=2z, 5x+y=z, 5x+3y=2z, 6x+3y=2z, 5x+5y=4z, 3x+2y=z we determine R₃ exactly — the values are 186, 243, 286, 395, 648, 875 and 1093 — and both halves of each determination are machine-checked: the avoiding colouring of ints(R₃-1) is exhibited and verified, and the non-existence of an avoiding colouring of ints(R₃) is an LRAT refutation replayed by a formally verified checker against a propositional formula that is constructed, not read from a file. The bridge between the formula and the colouring problem is a single encoding-fidelity theorem, proved once for all (a,b,c,r,N), and it is proved without any appeal to computation. The largest instance refutes a formula with 298,663 clauses. As far as our search reached, these are the first Rado numbers with coefficients other than a=b=c=1 to carry a machine-checkable certificate. All statements are verified in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   9487c671eab3557dfec359511e849ffa5dfc39b5f63c3605026c21d52a22a74e