Erdős Problem #124

Partial progress by Aristotle (29 Nov 2025): partial result (Lean).

Problem
Erdős problem #124 (number theory, base representations, complete sequences); current status: open
Credit
Aristotle · AI on its own
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2025-11-29 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
PARTIALPer Tao's AI-contributions wiki

The problem

For any d≥1d\geq 1 and k≥0k\geq 0 let P(d,k)P(d,k) be the set of integers which are the sum of distinct powers did^i with i≥ki\geq k. Let 3≤d1<d2<⋯<dr3\leq d_1<d_2<\cdots <d_r be integers such that

∑1≤i≤r1dr−1≥1.\sum_{1\leq i\leq r}\frac{1}{d_r-1}\geq 1.

Can all sufficiently large integers be written as a sum of the shape ∑iciai\sum_i c_ia_i where ci∈{0,1}c_i\in \{0,1\} and ai∈P(di,0)a_i\in P(d_i,0)?

If we further have gcd(d1,…,dr)=1\mathrm{gcd}(d_1,\ldots,d_r)=1 then, for any k≥1k\geq 1, can all sufficiently large integers be written as a sum of the shape ∑iciai\sum_i c_ia_i where ci∈{0,1}c_i\in \{0,1\} and ai∈P(di,k)a_i\in P(d_i,k)?

Statement quoted from erdosproblems.com/124, maintained by Thomas Bloom. Original source: [BEGL96][Er97,p.156][Er97e,p.533]. Current status there: open.

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Outcome
29 Nov, 2025 AI on its own Aristotle 🟡 Partial result (Lean)

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎