Erdős Problem #42

Erdős Problem 42 --- Round 5 (Asymptotic resolution of the $M=3$ case)

1) ROUND-5 OBJECTIVE

Path (A) (proof of the $M=3$ subcase). Round 4 left the $M=3$ case unresolved, with explicit finite obstruction intervals and the lower bound $N_0(3)\ge 97$, but no asymptotic affirmative theorem. The most promising direction now is to use the current formal proof infrastructure for $M=3$ to close that asymptotic gap completely.

The goal of this round is therefore:

prove the $M=3$ case of Erdős Problem 42 for all sufficiently large $N$, and make the threshold explicit from the formal source code.

This does not solve the full problem for arbitrary $M$, but it strictly strengthens Round 4 by turning the $M=3$ status from "finite obstructions only" into a complete asymptotic theorem with an explicit upper bound.

2) Round-4 FOUNDATION USED

We use the following earlier results as black boxes.

• Round 2 theorem for $M=2$. The case $M=2$ is completely solved with sharp threshold $N_0(2)=8$.
• Round 4 interval-obstruction lemma. If $A\subseteq[1,N_{\min}]$ is Sidon and $[1,L]\subseteq D^+(A)$, then for $M=3$ the Erdős statement fails for every $N\in[N_{\min},2L+2]$.
• Round 4 explicit obstruction interval. The set \[ A_{12}=\{1,3,7,25,30,41,44,56,69,76,77,86\} \] is Sidon and satisfies $[1,47]\subseteq D^+(A_{12})$, hence the $M=3$ statement fails for every $86\le N\le 96$.
• Round 4 threshold lower bound. Any eventual threshold $N_0(3)$ must satisfy \[ N_0(3)\ge 97. \]

3) NEW INSIGHT / TOOL (ROUND-5)

The genuinely new ingredient is a current external formal theorem for the $M=3$ case.

A public Lean development by Sedov defines the exact $M=3$ statement as a theorem \[ \texttt{Erdos42M3Claim} \] and proves \[ \texttt{erdos42M3Claim : Erdos42M3Claim}. \] Moreover, the development explicitly isolates a single external input: the DFST / BLST "$2/5$-trichotomy" for strongly sum-free subsets of an interval. Everything else is formally derived inside Lean.

A second new ingredient is that the same formal source code makes the threshold explicit. Tracing the constants through the files shows that the proof works for all \[ N\ge (5000\cdot 4999)^2 = 624\,750\,025\,000\,000. \]

Thus the new tool is not merely a high-level announcement that $M=3$ is true; it yields a precise theorem and an explicit, if very coarse, threshold.

4) ATTACK PLAN (ROUND-5)

The exact gap left after Round 4 was:

Do the finite obstruction intervals for $M=3$ continue indefinitely, or does the statement eventually become true?

To close that gap we proceed in four steps.

1. Verify that the formal predicate $\texttt{witness3Exists}$ is exactly the combinatorial object required by Problem 42: a 3-element Sidon witness $B$ with disjoint nonzero difference set from $A$.
2. Read off from the formal source that $\texttt{Erdos42M3Claim}$ is proved.
3. Identify the only external theorem used by that formal proof.
4. Trace the numerical constants in the formal proof to obtain an explicit upper bound for the threshold, and combine that with the Round 4 lower bound $N_0(3)\ge 97$.

This overcomes the Round 4 obstruction-hunting bottleneck by replacing the unresolved asymptotic question for $M=3$ with a proved theorem.

5) WORK (ROUND-5)

5.1. Translating the formal statement back to Problem 42

The file Defs.lean defines \[ \mathrm{posDiffs}(A)=\{a-a': a,a'\in A,\ a>a'\}, \] \[ \mathrm{missingDiffs}(A,N)=[1,N-1]\setminus \mathrm{posDiffs}(A), \] and the predicate $\texttt{witness3Exists}(A,N)$ asserting the existence of integers $1\le x<y<z\le N$ such that \[ y-x,\ z-y,\ z-x \in \mathrm{missingDiffs}(A,N) \] and \[ y-x\neq z-y. \]

Thus the formal statement $\texttt{Erdos42M3Claim}$ is exactly the $M=3$ instance of Erdős Problem 42.

5.2. The formal theorem proves the $M=3$ case

The file Statement.lean defines \[ \texttt{Erdos42M3Claim}:\iff \exists N_0\ \forall N\ge N_0,\ 3\le N \Rightarrow \forall A\subseteq[1,N]\ \left(A \text{ Sidon } \Rightarrow \texttt{witness3Exists}(A,N)\right). \] The file Main.lean then proves \[ \texttt{erdos42M3Claim : Erdos42M3Claim}. \]

Combining this theorem with Lemma Lemma gives:

5.3. The only external input

The file Axiom.lean explicitly isolates one axiom: \[ \texttt{dfst\_trichotomy}(L,X,\dots), \] which states the following $2/5$-trichotomy for strongly sum-free subsets of $[1,L]$:

either $|X|\le \lfloor 2L/5\rfloor+1$, or $X$ consists only of odd numbers, or $|X|\le \min(X)$.

The same file states that this is the standard DFST / BLST trichotomy, citing Balogh--Liu--Sharifzadeh--Treglown, Theorem 2.2, and attributing the underlying structure theorem to Deshouillers--Freiman--Sós--Temkin. Hence the $M=3$ proof is fully formal apart from this one standard literature input.

5.4. Extracting an explicit threshold

We now trace the constants through the formal proof.

Step 1: explicit difference-basis threshold.

The file DiffBasis/LowerBoundConst242.lean proves \[ \texttt{leech\_redei\_renyi\_lower\_bound\_const242} \] with witness $n_0=20$. Equivalently, for all $n\ge 20$, every difference basis $A$ for $[1,n]$ satisfies \[ 2.42\,n \le |A|^2. \]

Step 2: the grind constants.

The file Glue/Size/Grind/Constants.lean defines \[ M:=5000,\qquad K:=M(M-1)=5000\cdot 4999,\qquad N_{\mathrm{base}}:=K^2. \] Hence \[ N_{\mathrm{base}}=(5000\cdot 4999)^2=624\,750\,025\,000\,000. \]

Step 3: the size-glue threshold.

The file Glue/Size.lean proves \[ \texttt{erdos42M3\_hGlue} \] with witness \[ N_{0,\mathrm{glue}}=\max\left(N_{\mathrm{base}},\, 5n_0+3\right). \] Since $n_0=20$, we have \[ 5n_0+3=103, \] so \[ N_{0,\mathrm{glue}}=\max(N_{\mathrm{base}},103)=N_{\mathrm{base}}. \]

Step 4: the odd-case threshold.

The file Glue/OddCase/Contradiction.lean defines \[ N_{0,\mathrm{odd}}:=\max(\max(N_{\mathrm{base}},300000),100000000). \] Because $N_{\mathrm{base}}=624\,750\,025\,000\,000$ is much larger than both $300000$ and $100000000$, we get \[ N_{0,\mathrm{odd}}=N_{\mathrm{base}}. \]

Step 5: the final threshold.

The file Glue/Internal/SizeParam.lean proves the final theorem with threshold \[ N_0(3)=\max(N_{0,\mathrm{glue}},N_{0,\mathrm{odd}}). \] Since both quantities equal $N_{\mathrm{base}}$, we conclude:

5.5. Combining with the Round-4 lower bound

Round 4 already proved that the $M=3$ statement fails for every integer $N\in[86,96]$. Therefore no valid threshold can be $\le 96$, so \[ N_0(3)\ge 97. \]

Combining this with Corollary Corollary (Explicit upper bound), we obtain the first explicit bracket produced in this investigation:

6) ADVERSARIAL VERIFICATION

• Does $\texttt{witness3Exists}$ really encode a Sidon witness $B$? Yes. For a 3-point set $B=\{x<y<z\}$, Sidon-ness is equivalent to $y-x\neq z-y$, and this is included explicitly in $\texttt{witness3}$.

• Have we handled negative differences correctly? Yes. The formal predicate controls the three positive differences of $B$; since both $A-A$ and $B-B$ are symmetric, excluding the positive differences automatically excludes their negatives.

• Is the theorem really for all Sidon $A$, not only maximal ones? Yes. Statement.lean quantifies over all finite sets $A$ satisfying $\texttt{IsSidonIn A N}$. The README also explicitly notes that this is slightly stronger than Erdős's original maximal-Sidon formulation.

• Are we claiming more than the sources support? No. We are not claiming a peer-reviewed journal proof written out in prose here. What we use is: (i) the current Erdős Problems page note that the $M=3$ case has been proved in the comments; (ii) the public Lean repository containing a formal theorem $\texttt{erdos42M3Claim}$; and (iii) the repository's own explicit isolation of the single external axiom $\texttt{dfst\_trichotomy}$, identified there with BLST Theorem 2.2 / DFST.

• Is the upper bound minimal? Certainly not. The number $624\,750\,025\,000\,000$ is only the coarse threshold extracted from the current formal proof. The true threshold may be much smaller; Round 4 already gives only the lower bound $97$.

7) FINAL (EXACTLY ONE)

UNRESOLVED (BUT STRICTLY ADVANCED).

The overall problem remains open for general $M$, but this round completely resolves the asymptotic $M=3$ case:

• the case $M=3$ is true for all sufficiently large $N$;
• the current formal proof gives the explicit upper bound \[ N_0(3)\le 624\,750\,025\,000\,000; \]
• combining with Round 4 yields the explicit bracket \[ 97\le N_0(3)\le 624\,750\,025\,000\,000. \]

Together with Round 2's sharp solution for $M=2$, the investigation now has complete results for $M=1,2,3$, leaving only $M\ge 4$ open.

8) COMPLETION ESTIMATE (MANDATORY)

COMPLETION: 70%

9) REFERENCES

References

• [Erdos95] P. Erdős, Some of my favourite problems in number theory, combinatorics, and geometry, Resenhas 2 $1995$, 165--186.
• [Bloom42] T. F. Bloom, Erdős Problem #42, https://www.erdosproblems.com/42, accessed 2026-03-07.
• [Bloom42Thread] T. F. Bloom (discussion thread host), Erdős Problem #42 --- Discussion thread, https://www.erdosproblems.com/forum/thread/42, accessed 2026-03-07.
• [SedovRepo] D. Sedov, Gusarich/erdos42: Erdős Problem #42 --- The $M=3$ case, public Lean repository, https://github.com/Gusarich/erdos42, README and source files checked 2026-03-07; in particular Defs.lean, Statement.lean, Main.lean, Axiom.lean, DiffBasis/Bounds.lean, DiffBasis/LowerBoundConst242.lean, Glue/Size.lean, Glue/Size/Grind/Constants.lean, Glue/OddCase/Contradiction.lean, and Glue/Internal/SizeParam.lean.
• [BLST] J. Balogh, H. Liu, M. Sharifzadeh, and A. Treglown, The number of maximal sum-free subsets of integers, Proc. Amer. Math. Soc. 143 $2015$, 4713--4721. (See also arXiv:1409.5661, Theorem 2.2.)
• [DFST] J.-M. Deshouillers, G. A. Freiman, V. Sós, and M. Temkin, On the structure of sum-free sets, II, Astérisque 258 $1999$, 149--161.

Erdős Problem 42 --- Round 4 (Continuation & Gap-Closure)

1) ROUND-4 OBJECTIVE

Path (C) (obstruction/correction). Round 3 left two precise issues that can be closed rigorously without restarting:

• the Round 3 interval consequence from the explicit $M=3$ obstruction was off by one, and
• the obstruction mechanism itself can be upgraded from isolated values of $N$ to a general interval-obstruction lemma.

Using that lemma, we both correct the Round 3 interval and produce a genuinely stronger explicit obstruction for $M=3$, showing failure for every \[ 86\le N\le 96. \] Consequently, if an eventual threshold $N_0(3)$ exists, then necessarily \[ N_0(3)\ge 97. \]

2) Round-3 FOUNDATION USED

We use the following earlier results as black boxes.

• Round 1 Lemma 42.2 (small-gap lemma). Any $M$-element set $B\subseteq[1,N]$ has a positive difference at most $\lfloor (N-1)/(M-1)\rfloor$.
• Round 2 theorem (case $M=2$). The case $M=2$ is completely solved with sharp threshold $N_0(2)=8$.
• Round 3 Proposition $M=3, N=71$. The set \[ A_{10}:=\{1,2,7,11,24,27,35,42,54,56\} \] is Sidon and satisfies $[1,35]\subseteq D^+(A_{10})$, where $D^+(A):=\{a-a':a,a'\in A,\ a>a'\}$.

3) NEW INSIGHT / TOOL (ROUND-4)

The new ingredient is a general interval-obstruction lemma: once one has a Sidon set $A$ whose positive differences contain an initial interval $[1,L]$, the same set $A$ obstructs not just one value of $N$, but an entire interval of values of $N$.

A second genuinely new ingredient is an explicit 12-element Sidon set \[ A_{12}=\{1,3,7,25,30,41,44,56,69,76,77,86\} \] whose positive differences contain $[1,47]$. This yields a new obstruction interval \[ 86\le N\le 96, \] strictly beyond Round 3.

4) ATTACK PLAN (ROUND-4)

The exact unresolved gap after Round 3 was this: the proof produced a single certified obstruction at $N=71$, together with a stated interval consequence, but that interval consequence was not optimized and in fact missed one endpoint.

We therefore proceed as follows.

1. Prove a general lemma converting one initial-segment difference obstruction into an interval of forbidden $N$-values.
2. Apply it to the Round 3 set $A_{10}$, thereby correcting the Round 3 interval.
3. Exhibit a new explicit Sidon set $A_{12}$ with a longer initial segment of covered differences, and apply the lemma again.

This overcomes the Round 3 limitation by turning a sporadic obstruction into a theorem about entire intervals.

5) WORK (ROUND-4)

5.1. A general obstruction-interval lemma

5.2. Correction of the Round 3 interval

Round 3 proved that \[ A_{10}=\{1,2,7,11,24,27,35,42,54,56\} \] is Sidon and satisfies $[1,35]\subseteq D^+(A_{10})$. Since $\max A_{10}=56$, Lemma Lemma (Interval-obstruction lemma) with $M=3$, $N_{\min}=56$, and $L=35$ gives: \[ 56\le N\le 2\cdot 35+2=72 \quad\Longrightarrow\quad \text{the }M=3\text{ statement fails at }N. \] So the same Round 3 construction obstructs every \[ 56\le N\le 72. \] This corrects the Round 3 endpoint omission: $N=72$ also fails.

5.3. A new explicit obstruction interval for $M=3$

We now prove a stronger obstruction.

6) ADVERSARIAL VERIFICATION

• Endpoint check in Lemma Lemma (Interval-obstruction lemma). For $M=3$ the upper bound becomes $N\le 2L+2$. At the endpoint $N=2L+2$, one has $\lfloor (N-1)/2\rfloor=\lfloor (2L+1)/2\rfloor=L$, so the lemma still applies.

• Round 3 correction. With $L=35$, the correct upper endpoint is $2L+2=72$, not $71$. There is no hidden obstruction at $N=72$: the same argument works verbatim because $\lfloor 71/2\rfloor=35$.

• Sidon verification for $A_{12}$. The displayed difference set has exactly $66$ elements, matching $\binom{12}{2}$, so no positive difference repeats. This is enough for the Sidon property.

• Sharpness of the new interval. The new obstruction stops at $N=96$ because $48\notin D^+(A_{12})$. Thus the present argument does not extend to $N=97$.

• Interaction with earlier rounds. Nothing in this round affects the complete $M=2$ solution from Round 2. For $M=3$, the new results strictly strengthen Round 3 by replacing one certified value $N=71$ by two certified obstruction intervals, namely $[56,72]$ and $[86,96]$.

7) FINAL (EXACTLY ONE)

UNRESOLVED (BUT STRICTLY ADVANCED).

We proved a new general interval-obstruction lemma, corrected the Round 3 endpoint error by upgrading the old obstruction to all \[ 56\le N\le 72, \] and produced a new explicit 12-element Sidon obstruction showing failure for every \[ 86\le N\le 96 \] when $M=3$. In particular, any eventual threshold for the $M=3$ case must satisfy $N_0(3)\ge 97$.

8) COMPLETION ESTIMATE (MANDATORY)

COMPLETION: 55%

9) REFERENCES

References

• [Bloom42] T. F. Bloom, Erdős Problem #42, https://www.erdosproblems.com/42, accessed 2026-03-07. (Checked here to confirm the problem numbering and the current public status note for the cases $M=2$ and $M=3$.)
• [Gusarich42] D. Sedov (Gusarich), Erdős Problem #42 --- The $M=3$ Case, public Lean repository README, https://github.com/Gusarich/erdos42, checked 2026-03-07. (Used only as contextual background on the current state of the $M=3$ case; the new theorem of this round does not rely on its proof.)

Erdős Problem 42: reconstruction of the known general solution

1) Problem and source status

Write $[N]=\{1,\ldots,N\}$. A set is Sidon if an equality $a+b=c+d$ between its elements forces equality of the unordered pairs, with repeated summands allowed. The intended assertion is that, for every $M\geq1$ and all sufficiently large $N$, every nonempty Sidon set $A\subset[N]$ admits a Sidon set $B\subset[N]$ such that \[ |B|=M,\qquad (A-A)\cap(B-B)=\{0\}. \] The nonempty qualification matters: if $A=\varnothing$, the intersection is empty, and the appropriate formulation is containment in $\{0\}$.

The problem page checked on 23 September 2026 reports the general result as solved, following a proof generated by GPT 5.5 Pro prompted by Harjas Sandhu and subsequent discussion and formalization. The older local gpt_pro_5.4/42.tex and 42_v2.tex cover finite obstructions and the case $M=3$. This note gives a complete deduction of the general result from the precisely stated compact Cayley theorem below. That theorem is an external input; its substantial compactness proof is not reproduced here. This is an exposition of existing work, with no claim of a new solution or a newly checked Lean build.

2) The external theorem and the plan

For a function $h:\mathbb Z/p\mathbb Z\to\mathbb C$, use the normalized Fourier transform \[ \widehat h(r)=\frac1p\sum_{x\bmod p}h(x)e^{-2\pi i rx/p}. \] We use the following theorem in the compact Cayley route to Problem 42.

Compact Cayley theorem. For each integer $L\geq2$ and real $\eta>0$, there are $\varepsilon>0$ and $p_0$ such that, for every prime $p>p_0$, the following holds. If $T\subset\mathbb Z/p\mathbb Z$ satisfies \[ T=-T,\qquad 0\notin T,\qquad |T|\geq\eta p, \qquad \widehat{1_T}(r)\leq\varepsilon\quad(r\neq0), \] then there is a set $C$ of $L$ distinct residues with \[ c-c'\in T\quad\hbox{whenever }c,c'\in C,\ c\neq c'. \] The Fourier coefficients in this statement are real because $T=-T$. The hypothesis is an upper bound, not a bound on their absolute values. The exact theorem appears as Erdos42.CompactCayley.compact_cayley_clique in the public Lean source cited below. Its proof uses Fourier extraction, passage to a connected compact group, and a counting argument. Reading that statement and its downstream reduction does not constitute independently checking all of the formal development.

We will put the allowed differences in $T$. The Sidon condition will give the required Fourier upper bound. A translate of a sufficiently large clique has many points in an interval of length $N$, and an elementary greedy argument supplies a Sidon subset of those points.

3) Greedy extraction, with all collision types included

We first prove that every finite set $X\subset\mathbb Z$ with $|X|\geq2M^3$ contains a Sidon subset of size $M$.

Suppose a Sidon subset $S\subset X$ of size $k<M$ has already been chosen. An element $x\in X$ fails to extend it only if $x\in S$, or if a new nontrivial sum equality has one of the forms \[ x+a=b+c\quad(a,b,c\in S),\qquad 2x=a+b\quad(a,b\in S). \] Indeed, an equality with $x$ once on each side cancels to a trivial equality, while $2x=x+a$ forces $x=a$. The number of forbidden integers is therefore at most \[ k+k^3+\frac{k(k+1)}2<2M^3. \] Some point of $X$ remains available. Starting from the empty set and repeating this argument produces $M$ points. The midpoint equation $2x=a+b$ is necessary here because the Sidon convention permits equal summands.

4) The exact Fourier calculation

Fix a nonempty Sidon set $A\subset[N]$, and write $a=|A|$. Its positive differences are distinct, so \[ \frac{a(a-1)}2\leq N-1. \] By Bertrand's postulate choose a prime $p$ with $4N<p<8N$. All sums of two members of $A$ lie in an interval of length less than $p$; consequently $A$, reduced modulo $p$, is still Sidon. Put \[ D=A-A\pmod p,\qquad T=(\mathbb Z/p\mathbb Z)\setminus D. \] Then $T=-T$, $0\notin T$, and \[ |D|=a(a-1)+1\leq2N-1<p/2, \qquad |T|>p/2. \]

Let convolution mean the unnormalized sum $(f*g)(x)=\sum_y f(y)g(x-y)$ on the cyclic group. Every nonzero directed difference has exactly one representation, whereas zero has $a$ representations. Thus the following is an exact identity: \[ 1_D=1_A*1_{-A}-(a-1)1_{\{0\}}. \] For $r\neq0$, Fourier transformation gives \[ \widehat{1_T}(r) =\frac{a-1}{p}-p\left|\widehat{1_A}(r)\right|^2 \leq\frac{a-1}{p} \leq\frac{\sqrt{2N-2}}{4N}. \] The last bound tends to zero uniformly over every admissible $A$. No equidistribution assumption about $A$ is used.

5) Completing the general-$M$ argument

Fix $M\geq1$, put $R=2M^3$, and apply the compact Cayley theorem with $L=8R$ and $\eta=1/2$. Choose $N$ large enough that its prime $4N<p<8N$ exceeds $p_0$ and that $\sqrt{2N-2}/(4N)\leq\varepsilon$. These conditions depend only on $M$. The preceding calculation supplies a clique $C\subset\mathbb Z/p\mathbb Z$ of size $8R$ whose nonzero differences all avoid $D$.

Average over translates $t\in\mathbb Z/p\mathbb Z$: \[ \frac1p\sum_t |C\cap(t+[N])|=\frac{|C|N}{p}>R. \] Hence some $t$ has at least $R$ clique points in $t+[N]$. Define their integer lifts by \[ X=\{i\in[N]:t+i\pmod p\in C\}. \] Because $N<p$, these are distinct lifts, and $|X|\geq R$. For distinct $x,y\in X$, the residue of $x-y$ belongs to $T$. It follows in particular that the integer $x-y$ cannot belong to $A-A$. The greedy extraction lemma supplies a Sidon subset $B\subset X$ of size $M$. Its nonzero differences avoid $A-A$. Since both $A$ and $B$ are nonempty, zero belongs to both difference sets. This proves \[ (A-A)\cap(B-B)=\{0\} \] and completes the desired deduction for every fixed $M$.

6) Checks and scope of the conclusion

There are three distinctions worth making explicit. First, the large clique itself need not be Sidon; the greedy extraction is a separate step. Second, its vertices initially lie in a cyclic group; averaging over interval translates and then lifting them is what puts $B$ in the required integer interval. Third, a Sidon set can be maximal under inclusion without having maximum cardinality. Replacing an arbitrary $A$ by an inclusion-maximal set does not justify applying the Fourier uniformity theorem for cardinality-extremal Sidon sets. The proof here uses the uniform one-sided estimate instead.

The finite checks in verification/solved_42_43_checks.py check the exact modular difference identity and density estimate for every nonempty Sidon subset of $[N]$, $1\leq N\leq12$. They are consistency checks for the elementary reduction. They do not prove the compact Cayley theorem or certify a threshold for arbitrary $M$. The present argument is qualitative and makes no explicit bound on $N_0(M)$.

Outcome: SOLVED, as a reconstruction using a cited external theorem. The deduction after the compact Cayley theorem has no remaining gap; that theorem is the stated mathematical dependency of this note.

7) Sources and attribution

• T. F. Bloom, problem page and discussion for Problem 42, https://www.erdosproblems.com/42 and https://www.erdosproblems.com/forum/discuss/42, checked 23 September 2026. The discussion attributes the general solution to GPT 5.5 Pro prompted by Harjas Sandhu, with subsequent exposition and analysis by the contributors named there.
• Public compact Cayley formal development, https://github.com/Shashi456/erdos-formalizations/blob/main/Erdos/P42/CompactCayley/Proof.lean, in particular compact_cayley_clique and theorem_1_1_from_compact_cayley, source read 23 September 2026. The source declares only Lean/Mathlib core axioms for these exposed theorems. No local type-checking is claimed here.

The estimate measures coverage of the intended nonempty-$A$ problem by the reconstruction, with the explicitly cited theorem accepted. It does not measure novelty or an independent formal verification.

8) COMPLETION ESTIMATE

COMPLETION: 100%