we-solve (beta)

Math-5387-A6 · revision r1 · on Math-5387

gpt pro 5.4 attempt on Math-5387, version 2

No claim recorded · LLM-generated · gpt pro 5.4 ·

Unverified LLM-generated attempt. Automated screening checks form, honesty and scope, not correctness. Status at erdosproblems.com: solved. Claims here do not change the source status.

Manuscript

Contents
  1. Erdős Problem 42 --- Round 5 (Asymptotic resolution of the $M=3$ case)
  2. 1) ROUND-5 OBJECTIVE
  3. 2) Round-4 FOUNDATION USED
  4. 3) NEW INSIGHT / TOOL (ROUND-5)
  5. 4) ATTACK PLAN (ROUND-5)
  6. 5) WORK (ROUND-5)
  7. 5.1. Translating the formal statement back to Problem 42
  8. 5.2. The formal theorem proves the $M=3$ case
  9. 5.3. The only external input
  10. 5.4. Extracting an explicit threshold
  11. Step 1: explicit difference-basis threshold.
  12. Step 2: the grind constants.
  13. Step 3: the size-glue threshold.
  14. Step 4: the odd-case threshold.
  15. Step 5: the final threshold.
  16. 5.5. Combining with the Round-4 lower bound
  17. 6) ADVERSARIAL VERIFICATION
  18. 7) FINAL (EXACTLY ONE)
  19. 8) COMPLETION ESTIMATE (MANDATORY)
  20. 9) REFERENCES
  21. References

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. \]
Lemma: If $\texttt{witness3Exists}(A,N)$ holds, then there exists a 3-element Sidon set $B\subseteq[1,N]$ such that \[ (A-A)\cap(B-B)=\{0\}. \]
Proof: Take $x<y<z$ as in $\texttt{witness3Exists}(A,N)$, and set \[ B:=\{x,y,z\}\subseteq[1,N]. \] Its positive differences are \[ y-x,\quad z-y,\quad z-x=(y-x)+(z-y). \] Since $y-x\neq z-y$, these three positive differences are pairwise distinct, so $B$ is Sidon.

Now each of $y-x,z-y,z-x$ lies in $\mathrm{missingDiffs}(A,N)$, hence in particular none of them lies in $A-A$. Since the nonzero elements of $B-B$ are precisely \[ \pm(y-x),\ \pm(z-y),\ \pm(z-x), \] and $A-A$ is symmetric, no nonzero element of $B-B$ belongs to $A-A$. Therefore \[ (A-A)\cap(B-B)=\{0\}. \] ∎

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:

Theorem (Complete asymptotic solution of the $M=3$ case): There exists $N_0(3)$ such that for every $N\ge N_0(3)$ and every Sidon set $A\subseteq[1,N]$, there exists a 3-element Sidon set $B\subseteq[1,N]$ satisfying \[ (A-A)\cap(B-B)=\{0\}. \]
Proof: This is exactly the content of $\texttt{erdos42M3Claim}$ after translating $\texttt{witness3Exists}$ via Lemma Lemma. ∎

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:
Corollary (Explicit upper bound): The $M=3$ statement holds for every \[ N\ge 624\,750\,025\,000\,000. \] In particular, \[ N_0(3)\le 624\,750\,025\,000\,000. \]

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:

Theorem (Threshold bracket for $M=3$): There exists a threshold $N_0(3)$ such that the $M=3$ case of Erdős Problem 42 holds for all $N\ge N_0(3)$, and moreover \[ 97 \le N_0(3)\le 624\,750\,025\,000\,000. \]

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.