Skip to content

Erdős problem 348

For what values of 0m<n0 \leq m < n is there a complete sequence A={a1a2}A = \{a_1 \leq a_2 \leq \cdots\} of integers such that 1. AA remains complete after removing any mm elements, but 2. AA is not complete after removing any nn elements.

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

348.lean

Retained formal statement1 of 1

For what values of 0m<n0 \leq m < n is there a complete sequence A={a1a2}A = \{a_1 \leq a_2 \leq \cdots\} of integers such that 1. AA remains complete after removing any mm elements, but 2. AA is not complete after removing any nn elements.

FormalConjectures/ErdosProblems/348.leanErdos348.erdos_3488 linesExact file
{x |m n,      ∃ (_ : m < n),a,          ∃ (_ : Monotone a) (_ :            ∀ (s : Finset ℕ), s.card = mIsAddComplete (Set.range (Function.updateFinset a s 0))) (_ :            ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} =  sorry
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page