Erdős problem #792 — wave 7m report
Accessed: 2026-07-27 (UTC)
Authoritative page: erdosproblems.com/792
Standalone verifier: runs/erdos792_wave7m_reverify.py
Claim labels
- (a) elementary-rigorous: a complete proof is given here.
- (b) rigorous-modulo-named-theorem: the deduction is complete assuming the
precisely identified theorem.
- (c) plausible/structural-unverified: a proposed interpretation or route,
not used as a theorem.
- (d) computational-only: established by the stated finite computation or
direct browser inspection.
0. Mandatory live-page and collision check
(d) I fetched the Cloudflare-protected live page through the Bright Data
browser path. I separately fetched its LaTeX view and discussion thread and
expanded every bibliography popover (eight unique records; Erdős [Er65] is
linked twice). The page showed:
- status OPEN;
- 0 claimed proofs;
- “Currently working on this problem: None”;
- “Interested in collaborating: None”;
- 3 comments;
- last edited 23 January 2026.
Thus none of the mandatory stop conditions applied.
Live statement
To stay within the webpage quotation limit, the exact-source opening (22
verbatim words) is:
> Let \(f(n)\) be maximal such that in any \(A\subset \mathbb Z\) with
> \(|A|=n\) there exists some sum-free subset \(B\subseteq A\)
The remainder of the live LaTeX source requires \(|B|\geq f(n)\), defines
“sum-free” to mean that \(a+b=c\) has no solution with \(a,b,c\in B\), and asks
to estimate \(f(n)\). The complete exact source is at the
Results listed on the live page
The page attributes the following bounds:
\[ f(n)\geq \frac n3 \quad\text{(Erdős [Er65])}, \] \[ f(n)\geq \frac{n+1}{3} \quad\text{(Alon--Kleitman [AlKl90])}, \qquad f(n)\geq \frac{n+2}{3} \quad\text{(Bourgain [Bo97])}, \] \[ f(n)\geq \frac n3+c\log\log n \quad\text{for some }c>0 \quad\text{(Bedert [Be25b])}, \]and
\[ f(n)\leq \frac n3+o(n) \quad\text{(Eberhard--Green--Manners [EGM14])}. \]It also identifies this as Problem 1 on Ben Green's open-problem list. The page
warns that its OPEN label reflects the site owner's current belief and may miss
literature.
The expanded result references were:
1. N. Alon and D. J. Kleitman, Sum-free subsets (1990), 13--26,
MR 1117002.
2. J. Bourgain, Estimates related to sumfree subsets of sets of integers,
Israel J. Math. 97 (1997), 71--92, MR 1441239.
3. B. Bedert, *Large sum-free subsets of sets of integers via
\(L^1\)-estimates for trigonometric sums*, arXiv:2502.08624 (2025).
4. S. Eberhard, B. Green, and F. Manners, *Sets of integers with no large
sum-free subset*, Ann. of Math. (2) 180 (2014), 621--652, MR 3224720.
The page's four original-problem references were Erdős's 1965 *Extremal
problems in number theory, his 1973 Problems and results on combinatorial
number theory, his 1992 Some of my forgotten problems in number theory*, and
Problem 1.22 in the 1999 booklet Some of Paul's favorite problems.
All three live comments
(d) The comments do not claim a proof and do not announce work on the
discrete problem.
1. Xiao Hu, 25 July 2026, points to a continuous analogue on Green's list and
links arXiv:2607.06073, saying that it proves a similar upper bound.
2. Adenwalla, later that day, asks whether the linked question is the product
version of the real case.
3. Xiao Hu, 26 July 2026, replies that taking logarithms makes it additive.
The forum itself warns that comments are user-supplied and unverified.
1. A normalization issue in the literal live statement
Write
\[ \alpha(A)=\max\{|B|:B\subseteq A,\ B\text{ is sum-free}\}. \]Define the standard nonzero-integer function
\[ F_*(m)=\min_{\substack{A\subset\mathbb Z\setminus\{0\}\\|A|=m}}\alpha(A) \]and let \(f_{\mathbb Z}(n)\) denote the function literally defined by the live
page, where the host set may contain \(0\).
Exact shift
Proposition (a).
\[ \boxed{f_{\mathbb Z}(n)=F_*(n-1)\qquad(n\geq1).} \]Proof. A sum-free set cannot contain \(0\), because \(0+0=0\). Hence, if
\(0\in A\), then
\[ \alpha(A)=\alpha(A\setminus\{0\}). \]If \(0\notin A\), the minimum over such \(n\)-sets is \(F_*(n)\); if \(0\in A\),
the minimum is \(F_*(n-1)\). Therefore
\[ f_{\mathbb Z}(n)=\min(F_*(n),F_*(n-1)). \]The function \(F_*\) is nondecreasing: every \((m+1)\)-element nonzero set
contains an \(m\)-element subset, and its largest sum-free subset is at least
that of the smaller set. Thus the displayed minimum is \(F_*(n-1)\). \(\square\)
This is not just a cosmetic small-\(n\) point. For example,
\[ f_{\mathbb Z}(1)=0,\qquad f_{\mathbb Z}(3)=1 \](use the host sets \(\{0\}\) and \(\{0,1,2\}\)), so the finite
\((n+1)/3\) and \((n+2)/3\) inequalities printed on the page cannot literally
hold for its zero-allowed definition. The primary literature normally uses
positive integers or nonzero integers. The shift does not affect the
asymptotic \(1/3\) density or the order of an unbounded error term.
The standalone script independently checks
\(\alpha(A\cup\{0\})=\alpha(A)\) for every explicit witness below. (d)
2. Primary-source audit and current state
1. Erdős's 1973 paper,
Section 9, formulates the host as \(n\) nonzero real numbers and states the
\(n/3\)-scale result. This directly confirms that the historical
normalization excludes \(0\). (b)
2. The Alon--Kleitman chapter exists as pages 13--26 of *A Tribute to Paul
Erdős*, DOI
The introduction of Eberhard--Green--Manners precisely records its
\(F_*(n)\geq(n+1)/3\) consequence. (b)
3. Bourgain's paper exists at DOI
10.1007/BF02774027. The introduction
of Eberhard--Green--Manners states the theorem as
\(F_*(n)\geq(n+2)/3\) for \(n\geq3\). George Shakan's
arXiv:2207.14210, Theorem 1, gives an
alternative proof in the positive, coprime normalization and explicitly
isolates the exceptional set \(\{1,2\}\). (b)
4. Eberhard--Green--Manners,
arXiv:1301.4579 and
Annals DOI 10.4007/annals.2014.180.2.5,
define \(F_*\) on nonzero integers and prove
\(F_*(n)\leq n/3+o(n)\). Their introduction and abstract match the claim on
the live page. Their paper says the error is more or less ineffective
because of two uses of arithmetic regularity; it specifically identifies
the regularity input in its small-doubling analysis as the main obstacle to
an effective error. (b)
5. Bedert,
arXiv:2502.08624, defines the main
extremal function on positive integers and proves
\[ \alpha(A)\geq |A|/3+c\log\log |A| \]
for finite integer sets. Section 2 explicitly removes \(0\) before applying
the torus argument. This verifies the live page's lower bound and its
applicability, after the harmless one-index normalization above. (b)
6. The December 2025 edition of Ben Green's
marks its original Problem 1 Solved because Bedert proved an unbounded
additive improvement. The same entry still calls a reasonable effective
upper error interesting. Thus there is no contradiction with the live
page's OPEN label: Green's yes/no question is solved, while “estimate
\(f(n)\)” still has the wide error-term gap below. (b)
7. The paper linked in the new comments is Franchi--Gowers--Yip,
[Product-free subsets of \((0,1)\),
arXiv:2607.06073](https://arxiv.org/abs/2607.06073), submitted 7 July 2026.
Its abstract solves Green's continuous Product Problem 3 at the \(1/3\)
threshold. It does not claim a finite error term for the discrete function
in #792. (b)
Exact-title, author, citation, and 2025--2026 keyword searches found no primary
source improving Bedert's \(c\log\log n\) lower error or making the
Eberhard--Green--Manners upper error effective. This is a search report, not a
proof that no such source exists. (d)
Consequently, for the standard normalization, the verified current gap is
\[ \boxed{ c\log\log n \ \leq\ F_*(n)-\frac n3 \ \leq\ o(n). } \tag{1} \]3. Exact finite values and explicit certificates
For \(n\geq3\), Bourgain's theorem gives
\[ F_*(n)\geq \left\lceil\frac{n+2}{3}\right\rceil. \tag{2} \]This is (b), not reproved here. The following positive witnesses give the
opposite inequalities. Their largest sum-free subsets are recomputed from
scratch over all \(2^n\) subsets by the verifier. (d)
| \(n\) | positive witness \(A\) | \(\alpha(A)\) |
|---:|:---|---:|
| 1 | \(\{1\}\) | 1 |
| 2 | \(\{1,2\}\) | 1 |
| 3 | \(\{1,2,3\}\) | 2 |
| 4 | \(\{1,2,3,4\}\) | 2 |
| 5 | \(\{1,2,3,4,5\}\) | 3 |
| 6 | \(\{1,2,3,4,5,6\}\) | 3 |
| 7 | \(\{2,3,4,5,6,8,10\}\) | 3 |
| 8 | \(\{1,2,3,4,5,6,7,8\}\) | 4 |
| 9 | \(\{2,3,4,5,6,8,10,100,200\}\) | 4 |
| 10 | \(\{1,2,3,4,5,6,8,9,10,18\}\) | 4 |
| 11 | \(\{1,2,3,4,5,6,8,9,10,18,100\}\) | 5 |
| 12 | \(\{1,2,3,4,5,6,8,9,10,18,100,200\}\) | 5 |
| 13 | \(\{1,2,3,4,5,6,8,9,10,18,100,200,300\}\) | 6 |
| 14 | \(\{1,2,3,4,5,6,8,9,10,18,100,200,10000,20000\}\) | 6 |
The gaps are systematic. If \(A,C\subset\mathbb Z_{>0}\) and
\(M>2\max A\), every Schur relation in \(A\cup MC\) lies wholly in one block.
Indeed:
- two elements of \(A\) sum to less than \(M\), below every element of \(MC\);
- a sum of two elements of \(MC\) cannot land in \(A\);
- \(a+Mc_1=Mc_2\) would give \(a=M(c_2-c_1)\), impossible for
\(0 Therefore This block lemma is (a); the script also ignores it and checks each combined set directly. Combining (2) with the certificates yields the following exact table for the standard nonzero function, except at \(n=13\): All exact entries in (3) are (b) for their universal lower direction and (d) for their explicit upper certificate. The uncertainty at 13 is real: Bourgain gives 5, while the positive witness gives 6; a mixed-sign nonzero set could in principle attain 5. Applying the elementary shift from Section 1 gives a concrete exact table for the literal live-page function: In particular, the script certifies every upper witness in (3)--(4) without using a cited theorem. Let The verifier makes the following finite satisfiability reduction. Suppose a positive 13-set \(A\) had \(\alpha(A)\leq5\). Sort it as4. The first unsettled positive case: \(S_+(13)=6\) computationally
possible Schur relation has the form
\[ x_i+x_j=x_k,\qquad i\leq j\(\alpha(A)\leq5\) is exactly the conjunction, over all
\(\binom{13}{6}=1716\) six-index subsets, that at least one candidate equality
is supported inside that subset. Repeated summands are handled correctly:
\(2x_i=x_k\) needs only the two values \(x_i,x_k\).
The script builds this QF_LRA formula from scratch. Solving over the reals is a
relaxation of the integer problem, so UNSAT over the reals rules out an integer
counterexample. Z3 5.0.0 returned:
POSITIVE n=13 SMT: z3=5.0.0 atoms=364 coverage_clauses=1716
result=unsat seconds=47.229
Together with the 13-element witness of independence number 6, this gives
\[ \boxed{S_+(13)=6} \]as a (d) computational-only result. This sharpens Bourgain's value 5 in the
first finite case where his bound is not attained by the known certificates.
It agrees with Mark Lewko's 2013 report
of computer evidence that every 13-element natural-number set should have a
sum-free 6-subset, but the present run is an independent formulation and
computation.
I do not promote this to an elementary theorem: the run is reproducible,
but this report does not contain an independently kernel-checked Z3 proof
object.
Reproduction
Immediate standard-library certificate checks:
python runs/erdos792_wave7m_reverify.py --skip-smt
Full run:
python -m venv /tmp/erdos792-z3
/tmp/erdos792-z3/bin/pip install z3-solver==5.0.0.0
/tmp/erdos792-z3/bin/python runs/erdos792_wave7m_reverify.py
The script can also emit the complete generated formula with
--dump-smt2 PATH.
5. Precisely where the computation and asymptotic problem stall
Mixed signs at \(n=13\)
The positive computation does not settle \(F_*(13)\), because \(F_*\) permits
both signs. I tested the exact mixed-sign relaxation as follows.
Negation preserves all Schur relations, so one may assume at most six elements
are negative, sort the set, and scale the seventh element to \(x_6=1\). The
combined encoding had 665 candidate equalities and the same 1716 coverage
clauses. Z3 returned unknown at the imposed 120-second timeout. Fixing exactly
six negative elements reduces the candidate list to 322; that run returned
unknown at 60 seconds. (d)
Thus the exact missing finite certificate is:
> either exhibit a 13-element nonzero mixed-sign integer set with
> \(\alpha=5\), or prove the seven sign patterns (zero through six negatives,
> up to negation) QF_LRA-unsatisfiable.
A proof-producing solver portfolio with a one-core-hour cap per unresolved
sign pattern would cost at most about 6 core-hours (roughly \$0.30--\$0.60 at
\$0.05--\$0.10/core-hour), but completion is not guaranteed. A genuinely
auditable result should retain exact Farkas or SMT proof certificates rather
than only solver status lines. I did not run that larger job here.
For orientation, the next positive case—15 elements with no sum-free
7-subset—has 560 relation atoms and 6435 coverage clauses; Z3 returned
unknown at 90 seconds. (d)
The uniform asymptotic wall
The remaining asymptotic question is the order of
\[ D(n)=F_*(n)-n/3. \]Bedert proves \(D(n)\gg\log\log n\); Eberhard--Green--Manners construct sets
with \(D(n)=o(n)\). Closing (1) requires one of two genuinely new ingredients:
1. a quantitative replacement for the Eberhard--Green--Manners regularity
argument yielding an explicit upper error—matching Bedert would require
constructions with
\(\alpha(A)\leq n/3+O(\log\log n)\); or
2. a stronger universal lower mechanism showing that \(D(n)\) grows faster
than \(\log\log n\).
The exact missing upper-bound lemma can be stated cleanly: make the
small-doubling/weight construction in Eberhard--Green--Manners effective with
parameters tending to zero at an explicit rate. Their two regularity
applications currently destroy such a rate. Finite SMT tables do not supply
the uniform family of host sets needed for this step, and the 2026 continuous
product-free theorem controls only the limiting \(1/3\) threshold, not the
discrete error \(D(n)\).
PARTIAL: The literal zero-allowed function is exactly the standard nonzero function shifted by one; this gives exact values through the stated small regime, and a reproducible UNSAT computation gives \(S_+(13)=6\), while mixed signs and the asymptotic error remain open.