Erdős problem 700
f n is a lower bound: f n ≤ gcd(n, C(n,k)) for every 1 < k ≤ n/2.
Sources
FormalConjectures/ErdosProblems/
700.lean
Retained formal statement
Let .
(b) Are there infinitely many composite such that ?
Erdős–Szekeres [ErSz78] could not prove this. (Since , the least prime factor of , there are infinitely many — those of the form — with ; the question asks for the strict inequality.) Here is written as (f n) ^ 2 > n.
True ↔ {n | ¬Nat.Prime n ∧ 1 < n ∧ Erdos700.f n ^ 2 > n}.InfiniteOpenStatement only, no proof