Erdős problem 348

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.

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

348.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/348.leanErdos348.erdos_3488 linesExact file

1{x |2    ∃ m n,3      ∃ (_ : m < n),4        ∃ a,5          ∃ (_ : Monotone a) (_ :6            ∀ (s : Finset ℕ), s.card = m → IsAddComplete (Set.range (Function.updateFinset a s 0))) (_ :7            ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} =8  sorry

OpenStatement only, no proof