PROVED (LEAN). The site records the statement as true: first shown by Klarner in 1982, generalized by Kolpakov and Talambutsa in 2022, and proved independently by an elementary argument posted in the site's thread on 1 December 2025. The three are the claim pages Klarner, Kolpakov and Talambutsa and Barreto; the first two are accepted on refereed publication and the acceptance of the site's curator, Thomas Bloom, the third on that acceptance and Terence Tao's endorsement in the thread. Klarner's paper is not held, and Kolpakov and Talambutsa report that it omits the second part of its proof, which their Theorem 3 supplies in print. The (Lean) suffix is a catalog label: the community database lists the Lean status as of its last update on 1 December 2025, the day of the thread proof, whose comment links a Lean 4 web-editor formalization; a second Lean proof of the statement, with Barreto and Claude Opus 4.5 as its formal authors, sits in Boris Alexeev's lean-proofs repository; formal-conjectures holds only the statement, neither proof is recorded in formal-conjectures or the community database, and nothing was built or checked here (see Formalization). The site notes that the original formulation also required the least element of $A_k$ to be large, a condition that, as the site credits Ryan Alweiss with pointing out, holds automatically, since the least element grows by at least one at each stage. Erdős and Graham, who pose the problem on printed p. 96 of their 1980 monograph, call its difficulty surprising. The thread also relates the problem to a 2002 shortlist problem and generalizes the harmonic-sum argument to non-affine maps whose growth ratios $c_i=\limsup_n f_i(n)/n$ satisfy $\sum_i 1/c_i>1$; those are remarks, not claims on the question.