Erdős Problem a Daythe open tracker

Erdős Problem #481

PROVED LEANdatabase updated 2025-12-01

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

For a finite sequence of \(n\) (not necessarily distinct) integers \(A = (x_1,\ldots,x_n)\), the sequence `T a b A` of length \(rn\) given by \((a_ix_j+b_i)_{1\leq j\leq n, 1\leq i\leq r}\).

Let \(a_1,\ldots,a_r,b_1,\ldots,b_r\in \mathbb{N}\) such that \(\sum_{i}\frac{1}{a_i}>1\). For any finite sequence of \(n\) (not necessarily distinct) integers \(A=(x_1,\ldots,x_n)\) let \(T(A)\) denote the sequence of length \(rn\) given by \[(a_ix_j+b_i)_{1\leq j\leq n, 1\leq i\leq r}.\] Prove that, if \(A_1=(1)\) and \(A_{i+1}=T(A_i)\), then there must be some \(A_k\) with repeated elements. This is true. This appears to have first been shown by Klarner [Kl82], with a generalisation given by Kolpakov and Talambutsa [KoTa22]. Essentially the same proof was found independently by Barreto in the comment section.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/481.
Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/481
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.