---

Claim. The second question of Problem 635 has the answer yes. For every $t\ge1$ and every $\varepsilon>0$, for all sufficiently large $N$, every set $A\subseteq\{1,\ldots,N\}$ such that $b-a\nmid b$ whenever $a,b\in A$ and $b-a\ge t$ satisfies $\lvert A\rvert\le(1/2+\varepsilon)N$; that is, $\lvert A\rvert\le(1/2+o_t(1))N$. This is the theorem thm_main of the Lean file linked above, whose header lists the results it formalizes from a write-up titled Sets with no divisible differences above a threshold, the human-readable version linked above: the bound, the fact that the odd numbers satisfy the condition, a construction for $t\ge2$ from the odd numbers and powers of $2$ of size at least $\lceil N/2\rceil+\tfrac12\log_2N-O_t(1)$ (the write-up's Proposition 2, as the thread's comments name it), and the exact maximum $\lceil N/2\rceil$ for $t=1$. The proof is a second-moment argument: the condition says that $A$ contains no two consecutive multiples of any $d\ge t$, and weighting the elements by the primes $p\ge t$ dividing them bounds the count of elements with many prime divisors in the range. The result gives no error term beyond $o_t(1)$.

Submission note. Posted to the site's forum by Liam Price on 30 January 2026:

GPT-5.2 Pro gives a proof, formalised in Lean by Aristotle. Here's the human readable version. Kevin assisted with cleaning up the Lean.

Covers. The second question, the bound $\lvert A\rvert\le(1/2+o_t(1))N$, for every $t\ge1$. The first question, the maximum of $\lvert A\rvert$ as a function of $N$ and $t$, is not covered: Erdős's observations give the exact maximum $\lfloor(N+1)/2\rfloor$ for $t=1$ and a set of size at least $N/2+c\log N$ for $t=2$, and the gap between $N/2+c\log N$ and $(1/2+o_t(1))N$ is open.

Remarks. The proof was posted on 30 January 2026 in the site's discussion thread by the forum account Leeham (display name Liam Price), who states that GPT-5.2 Pro produced the proof and that Aristotle formalized it in Lean; the Lean file's header says it was generated by Aristotle, against Lean 4.24.0 and a pinned Mathlib. The site's commentary credits the resolution of the second question to ChatGPT-5.2, prompted by Leeham. In the thread, Terence Tao observed that the deduction of the write-up's Theorem 1 from its Lemma 4 follows at once from an inequality of Elliott (Lemma 4.7 of Probabilistic number theory I, 1979, [El79] on the problem page), that the second-moment argument is nearly identical to Elliott's although the write-up cites no sources, that only the second part of the problem is solved, and that the $o_t(1)$ term the method gives decays slowly, about $O(1/\log\log N)$, where Erdős probably sought an accuracy near $O(\log N/N)$. Another forum member noted that the construction's hypothesis $2^{k_0}\ge t$ is unnecessary and that a construction for $t=2$ serves every larger $t$.

Depends on. No page of this wiki.

Acceptance. None listed as evidence. The site labels the problem OPEN, a label that settles no part, so the commentary's credit is not listed as reviewed; Tao's remarks in the thread are commentary, and Tao marked only the second part solved in the community database, which lists the problem as open. There is no refereed publication. This corpus has not built or audited the Lean file, and the file's own #print axioms output is not recorded in the thread, so no formalized evidence is listed.