---

The file Erdos/Erdos441/solution.lean of the repository AxiomMath/erdos-public, at the commit of 18 June 2026 linked above, states erdos441_disproof: for $N=336$ the 21-element set $\{1,\ldots,10,12,14,15,16,18,21,24,30,36,42,48\}$ has all pairwise least common multiples at most $336$, while the construction $B_{336}=\{1,\ldots,12,14,16,18,20,22,24\}$ has $18$ elements, so the set of the second question is not a largest set at that $N$. The repository, owned by Axiom Math, describes its contents as artifacts generated by AxiomProver, and the thread's one comment (19 June 2026, by the forum user Ashvin) presents the file as AxiomProver's disproof of the second part of the problem. The file contains no sorry or axiom; nothing was built, kernel-checked or audited here, and the site's page did not label the problem Lean.

Covers. The construction part of the problem, the second question, which the Statement asks for each $N\ge1$, so that one value refutes it. The claim says nothing about the variant asking whether the construction is a largest set for all large $N$, which rests on Chen and Dai's theorem, infinitely many $N$ with unbounded excess, and nothing about the size part, the first question. The two facts of the counterexample, the 210 pairwise least common multiples and $|B_{336}|=18$, were recomputed on the problem page, and the set is the one recorded in the comment of 2012 on OEIS A068509; that recomputation is this project's own check and is not acceptance.

Standing. Claimed: no outside acceptance of the file exists, since the site's label predates it and rests on the refereed theorem, and no independent audit of the formal statement was made here.

Depends on. No page of this wiki.

Date. The page is dated by the thread's comment of 19 June 2026, the first posting of the claim to the problem; the repository commit of 18 June 2026 linked above is not a posting to the problem.