---

Claim. The inequality $\max_{m<n}(m+\tau(m))\le n+2$ holds exactly for $n\in\{1,2,3,4,5,6,8,10,12,24\}$, so no $n>24$ exists and the answer to Problem 647 is no. The write-up AI assisted (possible) solution to Erdos Problem 647 by Jamal Agbanwa was published on Zenodo on 2026-01-18 (the first link is the record's concept DOI, which resolves to its latest version) and revised through six versions; the fourth, of 2026-01-27, is the one announced on the site's discussion thread on 2026-01-28. The author names ChatGPT 5.2, Gemini and Deepseek Thinking as the systems used, and the write-up says that its Lean code was generated by ChatGPT 5.2 and kept in a GitHub repository of the author. The January argument writes $F(m)=m+\tau(m)$ and $M(n)=\max_{m<n}F(m)$ and works with the record-holders $h$ of $F$: for $h<n\le F(h)-3$ one has $M(n)\ge F(h)\ge n+3$, and the record-holders up to $60$ cover every $n$ with $25\le n\le69$. For $n>69$ it asserts that the domination intervals of successive record-holders overlap and so cover every large $n$. The two versions of 2026-04-26, titled On a divisor sum inequality: nonexistence beyond 24, replace this argument: for $n>24$ they take $M$, the largest multiple of $6$ below $n$, assert $M\ge n-5$, prove $\tau(M)\ge8$ for $M\ge24$, and conclude $M+\tau(M)\ge n+3$.

Submission note. Posted to the site's forum by Jamal Agbanwa on 28 January 2026:

We claim that the inequality

$$\max_{m<n}\bigl(m+\tau(m)\bigr)\le n+2$$

holds

precisely for

$$n\in\{1,2,3,4,5,6,8,10,12,24\},$$

and in particular has no

solutions for $n>24$.

The argument is based on a domination framework using record-holders of the function

$$m \longmapsto m+\tau(m).$$

Each record-holder produces an explicit

interval of integers $n$ for which

$$\max_{m<n}\bigl(m+\tau(m)\bigr)\ge n+3, >$$

and these domination intervals together cover all integers $n>24$.

A write-up of these results, including a Lean formalization of the main argument, is available at:

https://zenodo.org/records/18390414

The results were formalised in Lean.

(AI tools like ChatGPT 5.2, Gemini and Deepseek Thinking were used.)

Depends on. No page of this wiki.

Standing. Rejected. Terence Tao replied on the thread the same day (2026-01-28) that the asymptotic part of the argument, the case $n>69$, is far from justified, that the overlap of consecutive domination intervals is unproven and likely false, and that the Lean formalization treats the asymptotic case as an axiom rather than proving it, so it certifies nothing unconditionally. The write-up's text bears this out: its asymptotic section cites only the unboundedness of $\tau$ along a sequence of integers and asserts the overlap. The thread does not discuss the April versions. Their step $M\ge n-5$ fails whenever $6$ divides $n$, where $M=n-6$, and every candidate $n>84$ is a multiple of $2520$ by the elementary reduction the problem page records, so the April argument says nothing about the remaining candidates; this is the corpus's own reading, not a reviewed verdict. Neither version proves the negative answer, and the truth of the statement stays open: the problem page records the finite-range searches and density bounds that bear on it.