---

Claim. Suppose every $A_k$ has distinct entries and put $\Sigma_k=\sum_{x\in A_k}1/x$. Since $A_k$ then consists of $r^{k-1}$ distinct positive integers, $\Sigma_k\le H_{r^{k-1}}=O(k)$. In the other direction, with $C=\sum_i 1/a_i>1$ and $B=\sum_i b_i/a_i^2$, the identity $1/(a_ix+b_i)=1/(a_ix)-b_i/(a_ix(a_ix+b_i))$ gives $\Sigma_{k+1}\ge C\Sigma_k-B\sum_{x\in A_k}1/x^2$; the least entry of $A_k$ is at least $k$, because it grows by at least one at each stage, so $\Sigma_{k+1}\ge(C-B/k)\Sigma_k$, and for $k$ large the factor exceeds a fixed $C'>1$. Hence $\Sigma_k$ grows geometrically, contradicting the $O(k)$ bound. So some $A_k$ has a repeated entry.

Submission note. Posted to the site's forum by Kevin Barreto on 1 December 2025:

Below we give a proof:

Assume, for contradiction, that all entries of $A_k$ are distinct. Write

$$> \Sigma_k:=\sum_{x\in A_k}\frac{1}{x}, >$$

and set

$$> C:=\sum_{i=1}^r\frac{1}{a_i}>1\qquad\text{and}\qquad B:=\sum_{i=1}^r\frac{b_i}{a_i^2}. >$$

Since $A_k$ then has $r^{k-1}$ distinct positive integers,

$$> \Sigma_k\leq\sum_{j=1}^{r^{k-1}}\frac{1}{j}=H_{r^{k-1}}\leq 1+\log(r^{k-1})=1+(k-1)\log(r), >$$

so $\Sigma_k=\mathcal{O}(k)$. From $A_{k+1}={a_ix+b_i: x\in A_k,\ 1\leq i\leq r}$ and the identity

$$> \frac{1}{a_ix+b_i}=\frac{1}{a_i x}-\frac{b_i}{a_ix(a_ix+b_i)}, >$$

we obtain \begin{align*}\Sigma_{k+1} &= C\Sigma_k - \sum_{i=1}^r\sum_{x\in A_k}\frac{b_i}{a_i x(a_i x+b_i)}\ &\geq C\Sigma_k-\sum_{i=1}^r\sum_{x\in A_k}\frac{b_i}{a_i^2 x^2} = C\Sigma_k - B\sum_{x\in A_k}\frac{1}{x^2}.\end{align*} Let $m_k:=\min(A_k)$. As $m_1=1$ and $m_{k+1}=\min_{i,x}(a_ix+b_i)\geq m_k+1$, we have $m_k\geq k$. Hence, for every $x\in A_k$, we have $x\geq k$, and therefore

$$> \Sigma_{k+1}\geq C\Sigma_k-B\sum_{x\in A_k}\frac{1}{x^2}\geq C\Sigma_k-\frac{B}{k}\sum_{x\in A_k}\frac{1}{x}=\left(C-\frac{B}{k}\right)\Sigma_k. >$$

Now choose $K\in\mathbb{N}$ with $K>\frac{B}{C-1}$. Then, $\forall k\geq K$, set $C':=C-\frac{B}{K}>1$, giving

$$> \Sigma_{k+1}\geq C'\Sigma_k\qquad\forall k\geq K\implies\Sigma_k\geq\left(C'\right)^{k-K}\Sigma_K\qquad\forall k\geq K. >$$

So, $\Sigma_k$ grows exponentially for large $k$. This contradicts the harmonic upper bound $\Sigma_k=\mathcal{O}(k)$. Thus, for some $k$, the sequence $A_k$ contains repeated elements. $\square$

I have also taken the liberty to formalise the statement and my proof in Lean 4 here.

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

Postings. A comment in the site's thread, 1 December 2025, which also links a Lean 4 web-editor formalization of the statement and the proof (a share link to the Lean web editor, carrying the source in its URL; not retained, built or checked here). A second Lean 4 proof, the file ErdosProblems/Erdos481.lean of Boris Alexeev's lean-proofs repository linked above (added 5 May 2026, pinned to its last change of 2026-08-10), declares itself a formalization of Barreto's proof: it names Kevin Barreto as the informal author and Claude Opus 4.5 and Barreto as the formal authors, describes the result as proved and formalized by Barreto with assistance from Claude Opus 4.5, proves erdos_481 (hr : 0 < r) (hC : 1 < C a) : ∃ k, 1 ≤ k ∧ ¬(A a b k).Nodup with no sorry, and closes with a comment recording the axioms propext, Classical.choice and Quot.sound; it was neither built nor audited here. The site's commentary was updated on 1 December 2025 to credit Barreto, as Barreto's comment notes, and again on 3 December 2025, after a thread comment pointed to Klarner's paper, to attribute the first proof to Klarner and to record Barreto's as an independent rediscovery; a later thread comment generalizes the argument to arbitrary maps $f_i$ whose growth ratios $c_i=\limsup f_i(n)/n$ satisfy $\sum_i 1/c_i>1$, and another relates it to a Dirichlet-series proof of a 2002 shortlist problem.

Acceptance. The site's curator, Thomas Bloom, accepted the proof into the commentary, crediting Barreto, and labeled the problem PROVED; the community database lists that label as of its last update on 1 December 2025. Terence Tao's thread comment of 1 December 2025 endorses the argument and explains it as a harmonic weighting of the integers; the same comment reports that, asked for a literature review, ChatGPT DeepResearch declared the problem open while Gemini DeepResearch reproduced essentially the same argument without recognizing it as a proof. Those documented acceptances are the reviewed evidence. The formalizations are not listed as evidence: nothing was built or audited here, and the site's (Lean) suffix is explained on the problem page.

Depends on. No page of this wiki.