The 4-color Rado number of x+y+c=z: general case
For a constant , the 4-colour Rado number is the least such that every colouring of in four colours contains a monochromatic solution to . Myers (Rutgers thesis, 2015, Conjecture 4.9) and Ahmed, Boza, Emamy-Khansary, Marin, Revuelta and Sanz (Math. Comp. 85, 2016, §5.5) conjecturedfor all sufficiently large , with the small values and as exceptions. Previous methods reached individual values but not the general case.
This claims the conjecture for every , by reducing it to three finite facts: the single base value and the unsatisfiability of two "spoke" templates. The reduction is formalised in Lean 4 and holds for every ; the two templates are settled by SAT with DRAT certificates.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Rado numbers / partition regularity
- Posed by
- ABEMRS16 (Math. Comp. 85, 2016, §5.5); Myers (Ph.D. thesis, 2015, Conj. 4.9)
- Year posed
- 2015
- Years open
- 11y
- Solved
- 2026-08-19
- Model
- Claude Fable 5
- Vendor
- Anthropic
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Announced
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The claim is for every , reduced to three finite facts: the base value , and the unsatisfiability of a 321-position and a 521-position spoke template. The reduction is Lean-checked and holds for every ; 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 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.
What the AI did
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.
Verification
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.
Sources
- Lean proofR(c)=40c+41 for every c>=2: SAT certificates, five-solver verdicts, second encoder, Lean-checked reductionThe Lean 4 reduction (core Lean, no Mathlib)
- CodeThe evidence repository: proof, Lean reduction, certificates and claim map
- OtherCLAIMS.md - every public claim mapped to the artifact backing it
Submitted by ZestyWombat854 on