Skip to content

Erdős problem 683

There exists c>0c > 0 such that P(n,k)>min⁡{n−k+1,k1+c}P(n, k) > \min\{n-k+1, k^{1 + c}\} for all 0<k<n0 < k < n.}

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

683.lean

Retained formal statement2 of 4

Erdos [Er55d] improved this to P(n,k)≫klog⁡kP(n, k) \gg k \log k for k≤n/2k \le n/2.

FormalConjectures/ErdosProblems/683.leanErdos683.erdos_683.variant.erdos_log1 lineExact file
∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k ≤ n / 2 → ↑(Erdos683.P n k) > c * ↑k * Real.log ↑k
SolvedStatement only, no proof