Erdős Problem 123

References:

• erdosproblems.com/123
• [ErLe96] Erdős, P. and Lewin, Mordechai, $d$-complete sequences of integers. Math. Comp. (1996), 837-840.
• [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240.

def Erdos123.IsDComplete (A : Set ℕ) : Prop

A set A of natural numbers is d-complete if every sufficiently large integer is the sum of distinct elements of A such that no element divides another.

Reference: [ErLe96] Erdős, P. and Lewin, M., $d$-complete sequences of integers. Math. Comp. (1996).

Equations

• Erdos123.IsDComplete A = ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (s : Finset ℕ), ↑s ⊆ A ∧ IsAntichain (fun (x1 x2 : ℕ) => x1 ∣ x2) ↑s ∧ s.sum id = n

def Erdos123.IsSnug (ε : ℝ) (A : Finset ℕ) : Prop

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

Equations

• Erdos123.IsSnug ε A = ∃ (hA : A.Nonempty), ∀ a ∈ A, ↑a < (1 + ε) * ↑(A.min' hA)

def Erdos123.PairwiseCoprime (a b c : ℕ) : Prop

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

Equations

• Erdos123.PairwiseCoprime a b c = Pairwise (Function.onFun Nat.Coprime ![a, b, c])

theorem Erdos123.erdos_123 : sorry ↔ ∀ a > 1, ∀ b > 1, ∀ c > 1, PairwiseCoprime a b c → IsDComplete (↑(Submonoid.powers a) * ↑(Submonoid.powers b) * ↑(Submonoid.powers c))

Erdős Problem #123

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.

theorem Erdos123.erdos_123.variants.erdos_lewin_3_5_7 : IsDComplete (↑(Submonoid.powers 3) * ↑(Submonoid.powers 5) * ↑(Submonoid.powers 7))

Erdős and Lewin proved this conjecture when $a = 3$, $b = 5$, and $c = 7$.

Reference: [ErLe96] Erdős, P. and Lewin, Mordechai, $d$-complete sequences of integers. Math. Comp. (1996), 837-840.

theorem Erdos123.erdos_123.variants.powers_2_3 : IsDComplete (↑(Submonoid.powers 2) * ↑(Submonoid.powers 3))

A simpler case: the set of numbers of the form $2^k 3^l$ ($k, l ≥ 0$) is d-complete.

This was initially conjectured by Erdős in 1992, who called it a "nice and difficult" problem, but it was quickly proven by Jansen and others using a simple inductive argument:

• If $n = 2m$ is even, apply the inductive hypothesis to $m$ and double all summands.
• If $n$ is odd, let $3^k$ be the largest power of $3$ with $3^k ≤ n$, and apply the inductive hypothesis to $n - 3^k$ (which is even).

Reference: [Er92b] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) (1992), 231-240.

theorem Erdos123.erdos_123.variants.powers_2_3_5_snug : sorry ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ (A : Finset ℕ), ↑A ⊆ ↑(Submonoid.powers 2) * ↑(Submonoid.powers 3) * ↑(Submonoid.powers 5) ∧ IsSnug ε A ∧ ∑ x ∈ A, x = n

A stronger conjecture for numbers of the form $2^k 3^l 5^j$.

For any $ε > 0$, all large integers $n$ can be written as the sum of distinct integers $b_1 < ... < b_t$ of the form $2^k 3^l 5^j$ where $b_t < (1 + ϵ) b_1$.