Four-colour Rado numbers for x+y+c=z

What is the four-color Rado number for x+y+c=z, allowing x=y? The proposed formula is R(c)=40c+41 for every integer c≥2.

Why it matters and what counts as progress

Why it matters: The formula determines a whole infinite family of finite four-color forcing thresholds from exact structural and finite certificates.

What counts as progress: Prove the universal formula by matching avoiding colorings and forcing bounds, or find a parameter where it fails.

How the problem developed

2000 · Finite computation [1]
Robert Malo Computed exact four-colour Rado numbers for c=1,2,3 and obtained the formula 40c+41 on two residue classes of c.
2015 · Conjecture [2][3]
Kellen Myers Conjectured that R₄(x+y+c=z)=40c+41 for every c≥2; the conjecture also appears in the 2016 n-colour Rado paper.
2026 · Reported claim [4]
ZestyWombat854’s AI-driven research campaign A public Lean and SAT artifact claims R₄(x+y+c=z)=40c+41 for all c≥2, reducing the statement to one base value and two finite unsatisfiability certificates.

AI contribution

Claude reports the general four-color Rado formula

For four colors, with x=y allowed, the reported proof gives R(c)=40c+41 for every integer c≥2 in x+y+c=z. It reduces the universal statement to R(2)=121 and two unsatisfiable spoke templates.

AI involvementAI-led

ImportanceNotable

Technical verificationFormal (Lean 4; exact SAT/DRAT certificate checking)

Human understandingFew