Skip to content

Erdős problem 1063

Estimate nkn_k by finding a better upper bound.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1063.lean

Retained formal statement3 of 6

Erdős and Selfridge noted that, for n≥2kn \ge 2k with k≥2k \ge 2, at least one of the numbers n−in - i for 0≤i<k0 \le i < k fails to divide (nk)\binom{n}{k} ([ErSe83]).

FormalConjectures/ErdosProblems/1063.leanErdos1063.erdos_1063.variants.exists_exception1 lineExact file
∀ {n k : ℕ}, 2 ≤ k → 2 * k ≤ n → ∃ i < k, ¬n - i ∣ n.choose k
SolvedStatement only, no proof