Erdős Problem 348

Reference: erdosproblems.com/348

@[reducible, inline]

abbrev Function.IsCompleteNatSeq (a : ℕ → ℕ) : Prop

A sequence of naturals is complete if any positive natural can be written as a finite sum of distinct values in the sequence.

Equations

• Function.IsCompleteNatSeq a = ∀ n > 0, ∃ (s : Finset ℕ), Set.InjOn a ↑s ∧ s.sum a = n

theorem erdos_348 : {x : ℕ × ℕ | ∃ (m : ℕ) (n : ℕ) (_ : m < n) (a : ℕ → ℕ) (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → Function.IsCompleteNatSeq (Function.updateFinset a s 0)) (_ : ∀ (t : Finset ℕ), t.card = n → ¬Function.IsCompleteNatSeq (Function.updateFinset a t 0)), (m, n) = x} = sorry

For what values of $0 \leq m < n$ is there a complete sequence $A = \{a_1 \leq a_2 \leq \cdots\}$ of integers such that

1. $A$ remains complete after removing any $m$ elements, but
2. $A$ is not complete after removing any $n$ elements.