Erdős problem 123 · problems.science

Let $a,b,c>1$ be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form $a^k b^l c^m$ ( $k,l,m\ge 0$ ), none dividing another?

Sources

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

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

123.lean

Retained formal statement1 of 4

Let $a, b, c$ be three integers which are pairwise coprime. Is every large integer the sum of distinct integers of the form $a^k b^l c^m$ ( $k, l, m ≥ 0$ ), none of which divide any other?

Equivalently: is the set $\{a^k b^l c^m : k, l, m \geq 0\}$ d-complete?

Note: For this not to reduce to the two-integer case, we need the integers to be greater than one and distinct.

The prize of 250 is offered by Erdős in [Er97] and [Er97e] for a 'proof or disproof'.

The main problem was resolved in the affirmative by GPT 5.6 (prompted by Snyder).

This was formalized in Lean by Alexeev.

FormalConjectures/ErdosProblems/123.leanErdos123.erdos_1236 linesExact file

1True ↔2  ∀ a > 1,3    ∀ b > 1,4      ∀ c > 1,5        Erdos123.PairwiseCoprime a b c →6          Erdos123.IsDComplete (↑(Submonoid.powers a) * ↑(Submonoid.powers b) * ↑(Submonoid.powers c))

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