Erdős problem 434

Let $k \le n$ . What choice of $A\subseteq\{1, \dots, n\}$ (with $\text{gcd}(A) = 1$ ) of size $|A| = k$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed)? Is it $\{n, n - 1, \dots, n - k + 1\}$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

434.lean

Retained formal statement2 of 2

For $2 \le k \le n$ , the interval $A = \{n, n - 1, \dots, n - k + 1\}$ maximises the number of integers not representable as the sum of finitely many elements from $A$ (with repetitions allowed), as proved by Kiss [Ki02].

FormalConjectures/ErdosProblems/434.leanErdos434.erdos_434.parts.ii9 linesExact file

1True ↔2  ∀ n ≥ 1,3    ∀ k ≥ 2,4      k ≤ n →5        IsGreatest6          {x |7            ∃ S,8              ∃ (_ : S ⊆ Finset.Icc 1 n) (_ : S.card = k) (_ : S.gcd id = 1), Erdos434.Nat.NcardUnrepresentable ↑S = x}9          (Erdos434.Nat.NcardUnrepresentable (Set.Icc (n - k + 1) n))

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.