Problem detail · source-aware
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
For a constant $c$, the 4-colour Rado number $R(c)$ is the least $N$ such that every colouring of $\{1,\ldots,N\}$ in four colours contains a monochromatic solution to $x + y + c = z$. Myers (Rutgers thesis, 2015, Conjecture 4.9) and Ahmed, Boza, Emamy-Khansary, Marin, Revuelta and Sanz (Math. Comp. 85, 2016, §5.5) conjectured $$R(c) = 40c + 41$$ for all sufficiently large $c$, with the small values $R(0) = 45$ and $R(1) = 83$ as exceptions. Previous methods reached individual values but not the general case. This claims the conjecture for every $c \ge 2$, by reducing it to three finite facts: the single base value $R(2) = 121$ and the unsatisfiability of two "spoke" templates. The reduction is formalised in Lean 4 and holds for every $D \ge 1$; the two templates are settled by SAT with DRAT certificates.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
Claude surveyed three mutually-unaware literatures (Malo 2000, Myers 2015, ABEMRS16 2016), proved the scaling lemma and 28 base values (partial entry), then devised the spoke relaxation, proved that band templates fail, built the Lean formalisation, and ran the two UNSAT template computations to settle the general case. Human direction limited to run design, operational supervision, and posting.
Provider: Anthropic · Prompt public: unknown · Independence: unknown
Unreviewed: AI-produced, no peer review, and no authoritative tracker has accepted it. The artifact is unusually well organised, though, and some of it was checked here. Checked: the repository's CI is green on the verification workflow (CNF regeneration, hash checks, Lean reduction check); lean/Rado.lean is 354 lines with no sorry, no axiom declarations and no native_decide; and the theorem structure matches the prose, in that `upper` takes the three finite facts as explicit hypotheses, so Lean proves the reduction and the SAT work discharges the leaves rather than the Lean claiming the whole theorem. Not checked here: the two DRAT proofs were not re-verified, the SAT solves were not re-run, and the Lean was not rebuilt. By the repository's own logs drat-trim takes 998 s and 1125 s on the two templates, so this is compute rather than judgement, and it is exactly what site-confirmed would require. Worth noting in the submission's favour: a second, independently written encoder reproduces both unsatisfiability results from the definitions, the templates are regenerated from the Lean definitions and hash-checked against pins, and R(88) = 3561 was solved directly as a positive control.
Correctness: unknown · statement fidelity: unaudited · peer review: none
The claim is $R(c) = 40c+41$ for every $c \ge 2$, reduced to three finite facts: the base value $R(2) = 121$, and the unsatisfiability of a 321-position and a 521-position spoke template. The reduction is Lean-checked and holds for every $D \ge 1$; the two unsatisfiability results carry DRAT proofs. This completes the partial entry for the same conjecture, which proved it for roughly two thirds of integers via a scaling lemma; that lemma is now one of three legs, covering the branch where $d$ is divisible by 3. The supporting results are worth more than the headline for anyone deciding whether to believe it: the paper also shows every band relaxation is satisfiable, which is why previous attempts stalled, and that the affine method alone is exactly sharp and can never finish.
Source-reported tools: computation.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.