Erdős Problem 246

References:

• erdosproblems.com/246
• [Bi59] Birch, B. J., Note on a problem of Erd\H{o}s. Proc. Cambridge Philos. Soc. (1959), 370-373.
• [Ca60] Cassels, J. W. S., On the representation of integers as the sums of distinct summands taken from a fixed set. Acta Sci. Math. (Szeged) (1960), 111-124.
• [FaCh17] Fang, Jin-Hui and Chen, Yong-Gao, A quantitative form of the {E}rd\H{o}s-{B}irch theorem. Acta Arith. (2017), 301--311.
• [He00b] Hegyv'{a}ri, N., On the completeness of an exponential type sequence. Acta Math. Hungar. (2000), 127--135.
• [Yu24] Yu, Wang-Xing, On the representation of an exponential type sequence. Publ. Math. Debrecen (2024), 253--261.

def Erdos246.Gamma (a b : ℕ) : Set ℕ

The set $\{a^k b^l : k,l \geq 0\}$.

Equations

• Erdos246.Gamma a b = {x : ℕ | ∃ (k : ℕ) (l : ℕ), x = a ^ k * b ^ l}

theorem Erdos246.erdos_246 (a b : ℕ) (ha : 2 ≤ a) (hb : 2 ≤ b) (hab : a.Coprime b) : IsAddComplete (Gamma a b)

Let $(a,b)=1$. The set $\{a^kb^l: k,l\geq 0\}$ is complete - that is, every large integer is the sum of distinct integers of the form $a^kb^l$ with $k,l\geq 0$.

We state the nontrivial case $a,b\geq 2$, proved by Birch [Bi59].