---

Submission note. Posted to the site's forum by Quanyu Tang on 6 March 2026:

I think ChatGPT 5.4 Pro may have solved this problem! Together with my friends Yixin He and Yanyang Li, we have written up a proof that $f(m)\ll m^{1/2}$, in fact showing $f(m)\le 2\lceil \sqrt m\rceil$, which would match the known lower bound up to constants. The proof was generated by GPT 5.4 Pro, and I have also checked it myself and with several independent GPT 5.4 Pro sessions. We have not found any error.

The proof is available here: pdf here.

The LaTeX source is here: tex here.

Comments, corrections, and verification would be very welcome.

(The site has been updated to address this comment.)

Posted to the site's forum by Quanyu Tang on 7 March 2026:

My GPT just claimed to have a proof that $f(m) = \lceil 2\sqrt m \rceil$ for $m\geq 4$, but I'm going to sleep now and don't have time to check it at the moment. I just had another GPT 5.4 Pro, check the proof, and it said the proof is fine. I'm now putting the proof, which I haven't had time to verify myself, along with the TeX, in the link below. You can check it first.

The claimed proof is available here: pdf here.

The LaTeX source is here: tex here.

The claim. For every positive integer $m$, $f(m)=\min(m,\lceil2\sqrt m\rceil)$, and so $f(m)=\lceil2\sqrt m\rceil$ for $m\ge4$ (Theorem 2.1 and Remark 2.2), where $f(m)$ is the largest $r$ such that every set $A$ of $m$ positive integers and every interval of length $2\max A$ contain $r$ distinct integers matched to $r$ distinct members of $A$ dividing them. This is the estimate asked for by Problem 650, whose $f$ (sets $A\subseteq\{1,\ldots,N\}$ and intervals of length $2N$) agrees with the paper's by the remark under Formulation on the problem page; and it answers the displayed question $f(m)\le\sqrt m$ in the negative for every $m\ge2$, with equality only at $m=1$. The upper bound is Theorem 3.1, $f(st)\le s+t$ for all positive $s,t$, by a Chinese-remainder set of $st$ integers with at most $s+t$ matched multiples in an interval of length $2\max A$; the lower bound is Theorem 4.1, $f(m)\ge\min(m,\lceil2\sqrt m\rceil)$, by the defect form of Hall's theorem and the neighborhood bound $\lvert\Gamma(S)\rvert\ge2\sqrt{\lvert S\rvert}$ in the divisibility graph. The source is W. van Doorn, Y. Li and Q. Tang, Optimal bounds for an Erdős problem on matching integers to distinct multiples, arXiv:2603.28636v1 (30 March 2026; the only version and no journal reference on 2026-09-18), paged as the source digest of van Doorn, Li and Tang (2026). Read depth: the definition, Theorem 2.1, Remark 2.2, Lemma 2.3, Theorems 3.1 and 4.1 and the interval remark are checked against the paper; the proofs (Sections 3 and 4) are not.

Dating. The result was first posted in the site's thread: the equality $f(m)=\lceil2\sqrt m\rceil$ for $m\ge4$ with a proof draft on 7 March 2026 (the date this page is named by; the post and the draft, Tang's note on Problem 650 in Tang's repository, are linked above), after the upper bound $f(m)\le2\lceil\sqrt m\rceil$ on 6 March (a reproof of the Erdős–Selfridge bound, later improved to $f(m)\le\lceil2\sqrt m\rceil$ through $f(st)\le s+t$), whose write-up Tang posted with Yixin He and Yanyang Li (also linked above), matching the site's credit to GPT 5.4 Pro prompted by He, Li and Tang; the formalization of the equality followed on 8 March in van Doorn's post (linked above) and was extended to $\min(m,\lceil2\sqrt m\rceil)$; the paper was posted on 30 March. The paper's Section 5 and the thread record that the draft's lower bound argued, in one case, as if the next multiple after the largest multiple in one block had to lie in the other, which is false, and that the formalization found a working variant of the injection, which the paper adopts. Tang's note on the gap, added to the same repository on 21 March 2026, is linked above; both repository links are pinned to its commit of that day.

Acceptance. Reviewed: the site's curator, Thomas Bloom, independent of the authors, labels the problem SOLVED (LEAN), last edited 2 April 2026, and the commentary states the formula with a citation of the corrected paper; reviewed rests on that label and commentary. The thread's outline review of 7 March 2026 by Terence Tao and the site's curator, Thomas Bloom, the curator reproducing the injection $a\mapsto(c_a,c_a+a)$ and the neighborhood bound in a few lines, was of that day's draft and did not catch the gap in its Case 2 injection (Dating, above), so it is not counted as acceptance evidence. Not refereed: the paper has no journal record (the arXiv listing carried no journal reference, a Crossref query for the title returned nothing, and Semantic Scholar listed one citing preprint, all on 2026-09-18). The formalization link is the Lean file the formal-conjectures formal_proof attribute names, pinned to the repository head of 10 September 2026 (the file last changed 31 March 2026): it defines the paper's $f$ and proves erdos_f_eq with no sorry, axiom or native_decide in its text; it is neither built nor audited in this corpus, so formalized is not listed and no kernel credit is claimed. The second formalization link is the copy in Boris Alexeev's lean-proofs repository (added 6 May 2026), which declares itself a formalization of the solution and names GPT-5.4 Pro, van Doorn, He, Li and Tang as informal authors and Aristotle and van Doorn as formal authors; it is not built here either. Provenance, recorded not judged: the paper declares that its proof strategy was proposed by ChatGPT (GPT-5.4 Pro) and that Aristotle, Harmonic's automated theorem-proving system, made the argument rigorous and formally verified it, with the exposition human-written; the site's commentary credits the upper bound to GPT 5.4 Pro, prompted by He, Li and Tang, and the lower bound to GPT 5.4 Pro and Aristotle, before citing the paper. A refereed version or an independent review of the argument is the reopening condition for the preprint qualification. The claim value is answered: the question asks for an estimate of $f(m)$, which the theorem gives exactly, so the result is neither a proof nor a disproof.

Depends on. Nothing in this wiki: the theorem is proved within the paper, whose card is linked above.