Erdős problem 434
Let . What choice of (with ) of size maximises the number of integers not representable as the sum of finitely many elements from (with repetitions allowed)? Is it ?
Sources
FormalConjectures/ErdosProblems/
434.lean
Retained formal statement
Let . What choice of (with ) of size maximises the number of integers not representable as the sum of finitely many elements from (with repetitions allowed)? Is it ?
The maximal choice is indeed , as proved by Kiss [Ki02].
The Lean theorem assumes . When , the proposed singleton does not have gcd ; the gcd condition instead forces the unique admissible choice .
∀ (n k : ℕ), 1 ≤ n → 2 ≤ k → k ≤ n → IsGreatest {x | ∃ S, ∃ (_ : S ⊆ Finset.Icc 1 n) (_ : S.card = k) (_ : S.gcd id = 1), Erdos434.Nat.NcardUnrepresentable ↑S = x} (Erdos434.Nat.NcardUnrepresentable (Set.Icc (n - k + 1) n))