Erdős Problem #123

PROVED LEANdatabase updated 2025-08-31

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

A sequence is said to be $d$-complete if every large integer is the sum of distinct integers from the sequence, none of which divide any other. This particular case of $d$-completeness was conjectured by Erdős and Lewin [ErLe96], who (among other related results) prove this when $a=3$, $b=5$, and $c=7$.

Characterizes a "snug" finite set of natural numbers: all elements are within a multiplicative factor $(1 + ε)$ of the minimum. Specifically, for a finite set $A$ and $ε > 0$, all $a ∈ A$ satisfy $a < (1 + ε) · min(A)$.

Predicate for pairwise coprimality of three integers. Requires all three input values to be pairwise coprime to each other.

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.

Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/123.

Prize$250

Topicsnumber theory

Statement in LeanFormal Conjectures

Solution in Leanyes

Original pageerdosproblems.com/123

Attempts

submit one →

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.

← #122 the board #124 →