Erdős problem 434 · problems.science

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\}$ ?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/434.lean

Formal Conjectures

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

1∀ (n k : ℕ),2  1 ≤ n →3    2 ≤ k →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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:434
PLBY Lean proofsErdosProblems.Erdos434

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 24 Feb-29 May, 2026
Machine
Aristotle, Claude Opus 4.8
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science