---

Chen and Dai answer the second question in the negative: Erdős's construction $B_N$, the integers up to $(N/2)^{1/2}$ together with the even integers in $[(N/2)^{1/2},(2N)^{1/2}]$, is not a largest admissible set for infinitely many $N$, and its deficit is unbounded. In the paper's notation, with $C_x$ a largest set of positive integers whose pairwise least common multiples are at most $x$ and which contains $B_x$, and $|C_x|=|B_x|+R_1(x)$, Theorem 1 (p. 126) states that (i) $R_1(x)=0$ for infinitely many $x$ and (ii) $R_1(x)\ge\mathrm{loc}\,x-2$ for infinitely many $x$, where $\mathrm{loc}\,x$ is the number of iterated logarithms needed to bring $x$ below $1$; Corollary 1 transfers (ii) to the remainder $R(x)=|A_x|-(9x/8)^{1/2}$ of a largest admissible set $A_x$. Since $g(N)\ge|C_N|$, part (ii) gives $g(N)\ge|B_N|+\mathrm{loc}\,N-2$ for infinitely many $N$, which is the claim.

Covers. The construction part of the problem, the second question, answered no; the site's label attaches to this question. The Statement asks it for each $N\ge1$, and the theorem's infinitely many $N$ answer it no, as single values already do (the problem page records $N=4$, $N=12$ and $N=336$); the theorem also answers no the variant asking whether the construction is a largest set for all large $N$. Not covered: the size part, the first question, which Chen's asymptotic settles, $g(N)\sim(9N/8)^{1/2}$, sharpened by Dai and Chen's Theorem of 2006 to $-2\le g(N)-(9N/8)^{1/2}\le45(N/\log N)^{1/2}\log\log N$ for large $N$; the exact value is unknown, and part (i) leaves open whether $g(N)=|B_N|$ holds for infinitely many $N$.

Acceptance. Refereed: Acta Arithmetica 128 (2007), no. 2, 125--133, DOI 10.4064/aa128-2-3 (Crossref record accessed). Reviewed: Thomas Bloom, the site's curator and independent of the authors, rests the label DISPROVED on this theorem, which the problem's commentary (page last edited 27 December 2025) attributes to Chen and Dai, and the thread and the proof-claim tab carry no dispute. Read depth: claims checked for Theorem 1 and Corollary 1 on p. 126; the proof (pp. 127--133) was not read beyond Lemma 1, and nothing is independently reviewed by this project.

Formalization. The repository plby/lean-proofs (Boris Alexeev) holds src/latest/ErdosProblems/Erdos441.lean, linked above at the repository head of 15 September 2026. Its header calls it a formalization of a solution to the problem and names Chen and Dai as informal authors 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 theorem not_erdos_441 asserts that the construction is always admissible and that for every $M$ some $N\ge M$ has $|B_N|<g(N)$, through the family $N=2(6t+4)^2$ with the extra element $2(6t+6)$ (its docstring): an elementary infinite family, which gives the negative answer without formalizing Theorem 1's unbounded excess. The file contains no sorry and no axiom; nothing was built or audited in this corpus, the site's page on 2026-09-18 did not label the problem Lean, and the file gives no formalized evidence. The statement file ErdosProblems/441.lean of formal-conjectures, added on 20 September 2026 and described on the problem page, points its formal_proof attribute at this file at the commit linked above, and the submission package of Collin Yuanjie Ren described on Chen's claim page reuses its definitions and its non-optimality theorem.

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

Date. The paper carries a year only; the page name uses the first day of 2007 for want of an issue date.