---

Tao answers the question in the negative. Theorem 1 (pp. 4--5 of arXiv v5): for every $C_0>0$ there is a set $A$ of natural numbers with

$$\sum_{n\in A:\,n\le x}\frac1n=\exp\Bigl(\bigl(\tfrac{C_0}{2}+o(1)\bigr)\mathrm{Log}_2^{1/2}x\,\mathrm{Log}_3x\Bigr) \quad\text{and}\quad \sum_{n,m\in A:\,n,m\le x}\frac{1}{\mathrm{lcm}(n,m)}\ll_{C_0}\Bigl(\sum_{n\in A:\,n\le x}\frac1n\Bigr)^2$$

as $x\to\infty$, where $\mathrm{Log}_2x=\max(\log\max(\log x,1),1)$ and $\mathrm{Log}_3x$ is its iterate. The first quantity grows faster than $\log\log x$, so the hypothesis of the question holds, and the second bound makes the normalized sum of the conclusion bounded. The growth rate is optimal up to the choice of $C_0$, which the site's commentary records as the best possible result. The paper also records the elementary counterexample of the squarefree numbers with exactly $k\ge2$ prime factors, implicit in earlier work of Bergelson and Richter (remark on p. 4). The differences between the paper's conventions (sums over $n\le x$, ordered pairs with the diagonal) and the site's (sums over $[1,x)$, pairs $a<b$ in $(1,x]$) change nothing, as the authored note on the problem page shows.

Acceptance. Refereed: Integers 24 (2024), paper A100 (the journal's volume listing; the journal text was not compared with arXiv v5, which adds an appendix). Reviewed: Thomas Bloom, the site's curator and independent of the author, rests the label DISPROVED (LEAN) on this theorem, which the commentary (page last edited 27 September 2025) attributes to Tao; the thread and the proof-claim tab are empty. The arXiv preprint was first posted on 5 July 2024 (v1), which dates this page. Read depth here: claims checked for Theorem 1 and the p. 4 remark; the proof and the appendix were not read, and nothing is independently reviewed by this project.

The Lean suffix and the formalization link. The site's Lean suffix is a catalog label. The collection formal-conjectures holds the statement only (sorry, category research solved, no formal_proof attribute at the commit the problem page links; the attribute added on 18 September 2026 points at the file described next), which is a statement file and not a formalization link. The referent of the label is the file src/latest/ErdosProblems/Erdos442.lean of the repository plby/lean-proofs (Boris Alexeev), linked above at the repository head of 15 September 2026 and last changed on 23 and 24 August 2026. Its header calls it a formalization of a solution to the problem and names Tao as informal author and Codex and GPT-5.6 Sol as formal authors, so it is a formalization link on this page and not a claim of its own; its not_erdos_442 proves the negation of the collection's proposition with the squarefree semiprimes, the case $k=2$ of the p. 4 remark, importing the repository's Mertens estimate from its file for Problem 469. It was not built or audited here, and so gives no formalized evidence.

Depends on. No page of this wiki. The proof is self-contained in the paper.