---

Claim. Let $a_1,a_2,\ldots$ be positive integers with $a_n\to\infty$. Then

$$\sum_{n\ge1}\frac{\tau(n)}{a_1\cdots a_n}$$

is irrational. This is Theorem 2 of A short note on Erdős Problem #258, dated 2026-04-14 and posted the same day to the site's discussion thread by Przemek Chojecki, who writes that the note was obtained with GPT-5.4 Pro; it answers the question of Problem 258 yes, for every sequence and with no monotonicity assumption, which is the conjecture of Erdős and Straus (1971, Conjecture 2.24) that the problem restates. The argument is a tail estimate. Lemma 1 of the note: if the sum is $A/B$, choose $M>\Lambda(2B+1)$ and take $N$ with $\tau(N+k)\le\Lambda^k$ for all $k\ge1$ and with $a_n\ge M$ for every $n>N$, which is possible when infinitely many $N$ satisfy the $\tau$ bound, since $a_n\to\infty$; then $B\,a_1\cdots a_N$ times the tail after $n=N$ is a positive integer below $B\sum_{k\ge1}(\Lambda/M)^k<1/2$, a contradiction. Theorem 1.1 of Tao and Teräväinen supplies exactly such $N$: an absolute $C$ with $\Omega(N+k)\le Ck$ for all $k\ge1$ at infinitely many $N$, hence $\tau(N+k)\le2^{Ck}$, and $\Lambda=2^C$ closes the proof. The deep input is the theorem of Tao and Teräväinen; the deduction itself is elementary.

Postings. The note is the preprint link of 2026-04-14. Tao and Teräväinen's own preprint, arXiv:2512.01739 version 2 of 2026-04-25, records the deduction as Remark 1.4 (physical p. 5), credits the observation to Chojecki using GPT 5.4 Thinking, and gives the same short argument; the source card records Remark 1.4 and its attribution. Chojecki's own Lean 4 formalization, which Chojecki writes in the thread on 2026-04-14 was obtained with Aristotle, is the archive linked from that comment (the formalization link of 2026-04-14). It proves the deduction from the bound $\tau(N+k)\le\Lambda^k$ for all $k\ge1$ at infinitely many $N$, a consequence of Theorem 1.1 that it leaves as a sorry. The gist that the user ster (GitHub ster-oc) posted to the thread on 2026-04-21 is the formalization link at its pinned revision. Its header calls it Chojecki's original formalization, but ster writes that Aristotle was used to make it conditional on Theorem 1.1 itself rather than on that corollary. The gist's header says it is "modulo the deep Tao–Teräväinen theorem from analytic number theory (stated here without proof)", and the file declares that theorem as a Lean axiom, so it formalizes the deduction and not the input. formal-conjectures (revision of 2026-10-06) cites that gist as the formal proof of its Erdos258.erdos_258, tagged research solved, and cites the note and the gist in its references.

Acceptance. Reviewed: Thomas Bloom, the site's curator, labels the problem proved (page last edited 28 May 2026) and credits Chojecki and GPT-5.4 Pro, using the work of Tao and Teräväinen, in the problem's remarks; the authors of the input theorem, Tao and Teräväinen, adopted the deduction into their preprint as Remark 1.4 with credit, and Tao's comments in the thread of 2026-04-14 endorse it and explain why the theorem applies. No refereed publication exists as of 2026-10-07: the note is unrefereed and the Tao–Teräväinen paper is a preprint. Neither Lean formalization has been built or audited here, and both leave the input unproved (the archive as a sorry, the gist as an axiom), so the claim carries no formalized evidence and the site's (LEAN) qualifier describes a conditional formalization. This corpus has not reproved the input theorem and awards no tier of its own, and records only the remark and its attribution, not a check of the input theorem.

Depends on. Problem 248, whose settling result is Theorem 1.1 of Tao and Teräväinen, the only input beyond the elementary tail argument.

The monotone case, Theorem 2.23 of Erdős and Straus 1971, and their Lemma 2.14 for sequences with $|a_n|>c(\log n)^{3/4}$ are the accepted partial claim on their claim page; the fixed-base case $\sum\tau(n)/t^n$, Erdős 1948, is an adjacent result outside the question, since a constant sequence does not tend to infinity.