Skip to content

Erdős problem 700

f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.

Sources

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

9 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

700.lean

Retained formal statement3 of 9

Let f(n)=min1<kn/2gcd(n,(nk))f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k}).

(c) Is it true that, for every composite nn, f(n)An/(logn)Af(n) \ll_A n/(\log n)^A for every A>0A > 0?

Erdős–Szekeres [ErSz78] prove the weaker bound f(n)(1+o(1))n/lognf(n) \le (1 + o(1)) n/\log n (the case A=1A = 1). Here f(n)An/(logn)Af(n) \ll_A n/(\log n)^A is spelled out as: for every A > 0 there is a constant C (depending on A) with f(n) ≤ C · n/(log n)^A for every composite n.

FormalConjectures/ErdosProblems/700.leanErdos700.erdos_700.parts.iii1 lineExact file
True ↔ ∀ (A : ℝ), 0 < A → ∃ C, 0 < C ∧ ∀ (n : ℕ), ¬Nat.Prime n → 1 < n → ↑(Erdos700.f n) ≤ C * ↑n / Real.logn ^ A
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page