#792: F*(13) = 6 — the first n where a 13-set must hold a sum-free subset larger than Bourgain's bound
The problem (erdosproblems.com/792; Problem 1 on Ben Green's open-problem list). Let f(n) be the largest m such that every set A ⊂ ℤ with |A| = n contains a sum-free B ⊆ A with |B| ≥ m — sum-free meaning a + b = c has no solution in B (a = b allowed). Erdős showed f(n) ≥ n/3; Alon–Kleitman (n+1)/3; Bourgain (n+2)/3; Bedert n/3 + c log log n; and Eberhard–Green–Manners proved f(n) ≤ n/3 + o(n). The problem asks for the true order of the error term. Nobody knows it.
Where the August report left it. Our working report separated the literal
function (0 allowed in A) from the standard one on nonzero sets — they differ by exactly a shift of one — and
pinned the standard value F*(n) for every n ≤ 14 by explicit sets whose largest
sum-free subset meets Bourgain's bound, except at n = 13: there Bourgain gives 5, the best set we could find has
6, and a 13-set of positive integers can never do better than 6 (a QF_LRA instance, UNSAT in 47 s). A set with
both signs could in principle still reach 5. The report tried the mixed-sign case, got unknown from z3 at
60–120 seconds, and stopped.
Today's computation. Negating a set preserves every relation a + b = c, so a 13-set with no sum-free 6-subset may be assumed to have k ∈ {0, …, 6} negative elements; k = 0 is the settled positive case. For each k the question "do reals x0 < … < x12 exist, exactly k of them negative, such that every one of the C(13,6) = 1716 six-subsets contains some xi + xj = xm" is quantifier-free linear real arithmetic, which an SMT solver decides exactly. Integers are reals and scaling is a symmetry, so UNSAT over the reals rules out every integer set with that sign pattern. The order and sign constraints prune the candidate relations (two positives sum above both, two negatives below both, a negative plus a positive lands strictly between them), leaving 322–352 atoms per pattern; a second encoding keeps all 1,014 unpruned atoms so that a pruning mistake could not hide a witness. All six patterns are UNSAT:
| negatives k | atoms (pruned) | z3, pruned | atoms (unpruned) | z3, unpruned | cvc5, pruned |
|---|---|---|---|---|---|
| 1 | 352 | 124 s | 1014 | 546 s | 4579 s |
| 2 | 342 | 389 s | 1014 | 850 s | 33980 s |
| 3 | 334 | 297 s | 1014 | 2008 s | 16520 s |
| 4 | 328 | 225 s | 1014 | 1592 s | 31622 s |
| 5 | 324 | 332 s | 1014 | 899 s | 29968 s |
| 6 | 322 | 316 s | 1014 | 1978 s | 34039 s |
cvc5, a second solver with its own simplex and case-splitting, independently returned UNSAT on all six — k = 1 and 3 inside the original six-hour budget, k = 2, 4, 5 and 6 on a 12-hour re-run (8.3–9.5 h each; the one pattern z3 found slow, k = 2, was cvc5's slowest too). Together with k = 0 and the explicit 13-set {1, 2, 3, 4, 5, 6, 8, 9, 10, 18, 100, 200, 300} whose largest sum-free subset has 6 elements, this gives F*(13) = 6, and for the literal zero-allowed function fℤ(14) = 6. The exact table now reads F*(n) = 0, 1, 1, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 6, 6 for n = 0, …, 14 — equal to ⌈(n+2)/3⌉ at every n ≥ 3 except n = 13, the first point where the Bedert-type excess over Bourgain's bound actually shows up. The next positive rung has since finished too: every positive 15-set contains a sum-free 7-subset (z3, one encoding, UNSAT in 2.0 h), and {1, 2, 3, 4, 5, 6, 8, 9, 10, 18, 100, 200, 10000, 20000, 1000000} has largest sum-free subset exactly 7, so S+(15) = 7 against Bourgain's 6 — the excess persists. The seven mixed-sign patterns at n = 15 are now closed too — see F*(15) = 7.
Controls. The known UNSAT (k = 0, six-subsets) reproduces under the new encoding in 52 s. Three SAT controls — the same instances with seven-subsets, for k = 0 and k = 3 on both engines — each returned a rational model that was scaled to integers and re-checked from the definition by brute force (every 7-subset carries a relation; largest sum-free subset exactly 6), so the encoding admits the solutions it should. One of them is a genuinely mixed-sign 13-set with no sum-free 7-subset: {−73, −72, −36, 4, 8, 12, 16, 20, 24, 32, 36, 40, 72}.
Labels and what isn't claimed. The real-relaxation and negation reductions are (a) elementary; the six UNSATs are (d) computational — two solvers, two encodings, no kernel-checked proof object. This is one exact value in a table; it says nothing about the order of f(n) − n/3, which is the actual problem. We found no published value of F*(13) for mixed signs (Lewko reported computer evidence for the positive case in 2013); no priority claim beyond the computation itself.