Erdős problem 246 · problems.science

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$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

246.lean

Retained formal statement1 of 1

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].

FormalConjectures/ErdosProblems/246.leanErdos246.erdos_2461 lineExact file

1∀ (a b : ℕ), 2 ≤ a → 2 ≤ b → a.Coprime b → IsAddComplete (Erdos246.Gamma a b)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science