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 statement2 of 9

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

(b) Are there infinitely many composite nn such that f(n)>n1/2f(n) > n^{1/2}?

Erdős–Szekeres [ErSz78] could not prove this. (Since f(n)p(n)f(n) \ge p(n), the least prime factor of nn, there are infinitely many nn — those of the form p2p^2 — with f(n)n1/2f(n) \ge n^{1/2}; the question asks for the strict inequality.) Here f(n)>n1/2f(n) > n^{1/2} is written as (f n) ^ 2 > n.

FormalConjectures/ErdosProblems/700.leanErdos700.erdos_700.parts.ii1 lineExact file
True ↔ {n | ¬Nat.Prime n ∧ 1 < nErdos700.f n ^ 2 > n}.Infinite
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page