Schur number S(6): improve 536 ≤ S(6), or determine S(6)
Difficulty 60: S(5) = 160 already needed a two-petabyte certified proof and the six-colour instance is far larger, while the construction side has not moved since 2000; it sits just below R(5,5) (62), a comparable finite Ramsey-type value, and well above the empty-heptagon question (45), which has a visible SAT route. Application value 3: none beyond SAT proof engineering. Leverage 12: additive Ramsey theory and proof-compression methods only.
The problem
Can the numbers 1 to 537 be sorted into six boxes so that in no box two numbers add up to a third?
- 1Put numbers 1..n into six boxes
- 2No box has x, y and x + y
- 3Known: 536 works
- 4Is 537 possible? Needs a find or a proof
The question in a small case. Try to split the numbers 1, 2, 3, 4 into two groups so that no group contains , and ( allowed, so a group may not contain both and ). The split {1, 4} and {2, 3} works. Adding 5 fails: wherever 5 goes, some sum appears. A group with no such triple is called , and the S(k) is the largest such that 1, …, n can be split into sum-free groups. So S(2) = 4. The known values are 1, 4, 13, 44 and 160 for = 1 to 5. (Some sources count one higher and list 2, 5, 14, 45, 161; the question is the same.)
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Step 3
- SAT solving (CDCL)Algorithm
- Step 4
- DRAT and LRAT proof certificates and checkersLibrary · host
- Then
- Schur number S(6): improve 536 ≤ S(6), or determine S(6)The problem
State of the art
Fredricksen and Sweet (Electronic Journal of Combinatorics, 2000) constructed symmetric sum-free partitions giving S(6) ≥ 536 and S(7) ≥ 1680. A 2026 preprint on shifted S-templates (arXiv:2607.15034) still cites S(6) ≥ 536 as the known bound and states no upper bound for S(6). S(5) = 160 was proved by Heule in 2017 with a SAT proof of about two petabytes, verified by a formally verified checker (arXiv:1711.08076). For six colours the encoding is far larger. The general upper bound comes from multicolour Ramsey numbers, S(k) ≤ R_k(3) − 2 (OEIS A045652), which is far above 536; no specific upper bound for S(6) close to the lower bound has been published. For seven colours, Rowley (2021) raised the lower bound to S(7) ≥ 1696.
Realistic applications
No direct application. A proof of S(6) = 536 would dwarf the two-petabyte S(5) proof and would drive proof compression and checker engineering; a partition of {1, …, 537} would be a small, instantly checkable construction.
What counts as solved
Lower bound: an explicit partition of {1, …, 537} into six sum-free sets, verified by a script. Upper bound: a DRAT or LRAT proof that the standard CNF encoding for n = 537 and k = 6 is unsatisfiable, accepted by a verified checker.
How it gets verified
Bound / recordA numeric bound or record checked from a certificate or recomputation.
Quantity: the largest n with a partition of {1..n} into six sum-free sets; current record S(6) ≥ 536 (Fredricksen and Sweet, 2000), no matching upper bound. A lower-bound improvement is certified by an explicit colouring of {1..537} (or higher) checked by a short script; a matching upper bound is certified by a DRAT/LRAT refutation of the standard encoding (variable x_{i,c}, clauses forbidding monochromatic x + y = z), checked with drat-trim and a verified LRAT checker. Publish the generator, the CNF and the proof hash.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
Both directions are mostly computation: a heavily structured search for a partition of 537 numbers, or a SAT proof far larger than the five-colour one. Theory enters through symmetry and template constructions.
Bottlenecks
ranked by votes- #1ComputeProof size of the six-colour encoding
The five-colour case already produced about two petabytes of proof; the six-colour instance is much larger even after symmetry breaking, so storage and checking time become limits.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.