---

Claim. There is an infinite set $A$ of positive integers in which no element divides the sum of two distinct larger elements (property P in the reading of Problem 12) with $\liminf|A\cap\{1,\ldots,N\}|/N^{1/2}>0$, and for every $\varepsilon>0$ there is one with $|A\cap\{1,\ldots,N\}|\ge N^{1-\varepsilon}$ for all large $N$. The first set answers the first question yes; the second shows that no absolute $c>0$ makes every such set thinner than $N^{1-c}$ infinitely often, so the second question is answered no. The thread's sharpening, recorded below, gives one set with $|A\cap\{1,\ldots,N\}|\ge N/(\log N)^{O(\log\log\log N)}$ for all large $N$.

The construction. The Lean proof of part (i) of the formal-conjectures statement was first made public on 3 April 2026, as a pull request to that collection from a fork (the pull request linked above, opened at 13:52 UTC and merged on 7 April); the proof of part (ii) followed in a second pull request opened on 7 April 2026. A comment of 7 April 2026 in the site's thread, posted by the first author of the preprint linked above, reports that DeepMind's automated prover produced the two Lean proofs, links them in the fork, and derives informal arguments from them. Both build $A$ as a union of blocks $B_i$, each inside a short interval $[P_i,1.1P_i]$ and each free of three-term arithmetic progressions (a base-three digit set in the first proof, a Behrend sphere in the second), with every element of $B_i$ divisible by the $i$-th odd prime and congruent to $1$ modulo the earlier ones; a relation $a\mid b+c$ across blocks then fails modulo that prime, and within a block it forces $b+c=2a$, which the progression-free design excludes. The first proof takes $|B_i|\gg\sqrt{P_{i+1}}$, which gives the liminf; the second takes $|B_k|\ge(\max B_{k+1})^{1-c}$, which gives $|A\cap\{1,\ldots,N\}|\ge N^{1-\varepsilon}$ for every $\varepsilon>0$ and all large $N$. The thread then simplified and sharpened the construction: Terence Tao observed the same day that distinct $b,c>a$ already have $b+c>2a$, so the progression-free ingredient is unnecessary and a small change to the 1970 construction of Erdős and Sárközy suffices; the site's curator gave the blocks $B_k=\{C^{k\log k}<n<\tfrac32C^{k\log k}:n\equiv1\ (\mathrm{mod}\ p_i)\text{ for }i<k,\ n\equiv0\ (\mathrm{mod}\ p_k)\}$, whose union, for a fixed $C>e$, has $|A\cap[1,N]|\gg(\log N)^{-O(1/\varepsilon)}N^{1-\varepsilon}$ for all large $N$, where $\varepsilon=1/\log C$; the same comment suggests, with a caveat, that the construction gives $|A\cap[1,N]|\gg N/\exp(O(\sqrt{\log N\log\log N}))$, which needs $C$ to grow with $k$, since with $C$ fixed the count is $N^{1-1/\log C+o(1)}$; on 8 April 2026 Tao encoded the block index in binary, so that each block carries congruence conditions at about $\log k$ primes instead of $k$, which gives the bound stated above, and the curator's equivalent form reads the conditions off the binary digits of $k$, with density $\gg1/((\log N)(\log\log N)^{O(1)})$ for infinitely many $N$ when $n\equiv1$ is relaxed to a half-interval of residues. The informal arguments are those given in the thread; they have not been checked step by step.

Covers. The first two questions, for sets in the site's reading (two distinct larger elements): yes to the liminf question and no to the $N^{1-c}$ question. Not covered: the third question, whether $\sum_{n\in A}1/n$ converges for every such set. Every set constructed here has a convergent reciprocal sum, and the thread's barrier remark, recorded on the problem page, says why block constructions with congruence conditions cannot reach divergence.

Acceptance. None. The site labels the problem OPEN, a label that settles neither question this claim answers, and commentary on a problem so labeled is not acceptance; the site's curator, Thomas Bloom, rewrote the commentary on 8 April 2026 to credit DeepMind with a construction answering the second question no and hence the first yes, and to record the improved bound reached in the thread, and that commentary, with the re-derivation of the construction in the thread by Tao and the curator, is credit and not acceptance. The curator's own contribution, the simpler blocks above, came after the claim and is disclosed here. Not refereed: no journal publication was found in the search recorded on the problem page. The preprint arXiv:2605.22763 (21 May 2026, revised 8 June 2026), by twenty-one named authors, reports the prover's work on Erdős problems: Table 1 of its Section 3 (v2) lists parts (i) and (ii) of this problem among the nine problems its agent resolved, Section 3 discusses the first question, and Appendix B.4 gives informal proofs of the first two questions derived from the Lean proofs; it is not refereed and is not acceptance evidence. Not formalized in this corpus's sense: the two Lean proofs in the fork (erdos_12.parts.i at line 810 of the file at the first pinned commit, erdos_12.parts.ii at line 740 of the file at the second) have not been built or audited for statement fidelity by this corpus; the formal-conjectures statement file, linked from the problem page, records both parts as research solved with formal_proof attributes pointing at those proofs and sorry bodies. The arguments are attributed to DeepMind's automated prover, as the site names it, and nothing here is this project's own review.

Depends on. No page of this wiki. The 1970 density-zero theorem and the earlier constructions are context on the problem page.