---

Claim. There is an infinite set $A\subset\mathbb N$ such that $a+a'$ is squarefree for all $a,a'\in A$, the case $a=a'$ included, with

$$|A\cap[1,x]|\gg(\log x)^2$$

for all large $x$; equivalently, writing $A=\{a_1<a_2<\cdots\}$, there is an absolute constant $C$ with $a_j\le\exp(C\sqrt j)$ for all $j\ge1$. This is the Theorem of Xiyu Hu, A logarithmic-square construction for squarefree pairwise sums, dated July 2026, a note of about seven pages whose PDF and TeX source are in the public repository hxypqr/squarefree-pairwise-sums (three commits, all of 23 July 2026, the pinned head being the last). The author submitted it to the site's proof-claim tab the same day (the page name's date) as a partial result toward Problem 1103. The note's declaration states that OpenAI's GPT-5.6 Pro was used substantially, for the decomposition of the proof, an audit of the sieve parameters, the literature and much of the drafting, and that the author retains sole responsibility for the mathematics; the tab's header names GPT-5.6 Sol. The proofs are not checked in this corpus.

Submission note. Posted to erdosproblems.com as a proof claim by Xiyu Hu (account hxypqr) on 23 July 2026, giving "GPT-5.6 Sol" as the AI used:

I would like to share a partial result toward Erdős Problem #1103.The construction follows the general line of ideas developed by Wouter van Doorn and Terence Tao in their paper Growth rates of sequences governed by the squarefree properties of its translates, particularly their CRT-based treatment of local obstructions and iterative approach to constructing sequences with squarefree sums. The additional ingredient here is a more refined use of Konyagin’s quadratic Brun sieve in the finite extension step, which leads to the logarithmic-square bound above. I prove that there exists an infinite set $A\subset\mathbb N$ such that all pairwise sums, including diagonal sums, are squarefree and

$$|A\cap[1,x]|\gg(\log x)^2.$$

Equivalently,

if $A=\{a_1<a_2<\cdots\}$, then $a_j\leq\exp(C\sqrt j)$. Notes: The proof combines a compatible Chinese-remainder class for the small prime-square obstructions with a Konyagin-style quadratic Brun sieve for the remaining primes, followed by iteration of a finite extension principle. The optimal asymptotic growth in Erdős Problem #1103 remains open. An arXiv submission is planned.

The argument as the note describes it. A finite extension principle: given a finite good set $F\subset[1,N/2]$ with $|F|=O((\log N)^2)$, the new elements are placed in one Chinese-remainder class modulo $p^2$ for every prime $p<\lambda\log N$, a class compatible with $F$ (Lemma 2.1, the local restrictions), and the primes $p\ge\lambda\log N$ are handled by a uniform consequence of Konyagin's quadratic Brun sieve (Lemma 3.1, which the note derives from Lemmas 5 to 7 of Section 4 of Konyagin's 2004 paper, recorded on the card Konyagin 2004, and then checks the parameters of). Iterating the extension on dyadic scales gives the infinite set. The note's remarks say that a single Chinese-remainder class forces $z=O(\log N)$ and so loses the factor $\log\log N$ of Konyagin's finite lower bound, and that the plausible infinite scale $\log a_j\ll\sqrt{j/\log j}$ is not reached.

Covers. The construction side of the question: a sequence with squarefree pairwise sums need grow no faster than $\exp(C\sqrt j)$. This improves the sub-exponential construction of van Doorn and Tao, Theorem 7 of the first arXiv version of their paper (arXiv:2512.01087v1, 30 November 2025), recorded on their claim page: an infinite squarefree sequence with squarefree sums and $a_j\le\exp(Cj/\log j)$ for all $j\ge2$, where for large $j$ the constant $C$ may be any number above 4 (the site's commentary records the bound with the constant 5). The second arXiv version (7 December 2025), recorded on the card van Doorn and Tao 2025, keeps that construction as a remark referring to the first version, and says it is likely that Konyagin's constructions can be modified to give an infinite sequence with $|A\cap[N]|\gg\log^2N\log\log N$; that counting bound inverts to the scale $\log a_j\ll\sqrt{j/\log j}$, which Hu's note names as the scale it does not reach. Not covered: the necessary growth, where the best bound is $a_j\ge j^{15/11-o(1)}$, obtained in the same paper by inverting Konyagin's finite upper bound $\mathrm{ES}_N\le N^{11/15+o(1)}$ (Konyagin 2004), nor the true growth rate; the note itself says the optimal growth remains open.

Formalization. The repository is a Lean 4 project pinned to Lean and Mathlib v4.32.0, whose README calls the formalization partial and states that it does not claim a checked proof of the final theorem. At the pinned commit, the good-set predicate with diagonal sums, Lemma 2.1, the Chinese-remainder assembly, a finite inclusion and exclusion sieve with the Brun tree, the quadratic survivor set, the extension step, the iteration and the transfer of a stagewise bound to the counting function are stated as kernel-checked, with no sorry, admit or project axiom in the proof files; the analytic input, the note's Lemma 3.1, is represented by the proposition SquarefreeSums.Brun.HuLemma31, which is stated and not proved; the README's status note adds that the analytic sieve input and the Chinese-remainder progression estimates are not yet fully formalized; and the unconditional conclusion is the proposition PaperClaim, whose completion gate CompletionCertificate the README says has no inhabitant yet. The corpus has not built or audited the development, so it counts as no acceptance evidence.

Standing. Claimed. The site's label is OPEN (page last edited 3 December 2025). The tab's one comment, by the author on 2 August 2026, says that the note will not be submitted to arXiv, since the argument sharpens an intermediate Brun-sieve estimate of existing methods rather than adding a new idea, and that a discussion with a sieve specialist found no straightforward strengthening; that is the author's own statement, not a review. The tab's summary and the note call the result partial, and the page records it so. No refereed version, arXiv record or outside review is known.

Depends on. No page of this wiki. The sieve input is a literature result, cited above through its library card.