The four-colour Rado number of 5(x-y) = 4z is 741

Identifier: F:rado-r4-a5-b4
Proof route: search-certificate
External status: open
Axiom footprint: Empty

Recorded description

Every 4-colouring of {1,...,741} contains a monochromatic solution of 5(x-y) = 4z, and some 4-colouring of {1,...,740} avoids one. So R_4(5(x-y)=4z) = 741.

Formal statement

(assert (and (forall-colourings 741 4 (exists-mono-solution (= (* 5 (- x y)) (* 4 z)))) (exists-colouring 740 4 (no-mono-solution (= (* 5 (- x y)) (* 4 z))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

claim-741

Kind: claim-ref
Status: checked

Supports: R_4(5(x-y)=4z) = 741, both sides

Checker command

python3 scripts/check-claim-certificates.py

Evidence notes

A complete adaptive cube cover of F_741: 6241 cubes, every one refuted, every DRAT proof re-derived by axeyum's own backward checker; covered measure exactly 4294967296/4294967296. Lower side is a replayed 4-colouring of [740].

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum cube-and-conquer, campaign lane agent-b",
  "prior_art": [
    {
      "citation": "Chang, De Loera, Wesley, ISSAC 2022",
      "establishes": "Table 10 leaves the (a,b) = (5,4) cell blank"
    }
  ]
}