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 and let be the largest prime dividing .
(a) Characterise those composite such that .
Erdős–Szekeres [ErSz78] note that when is a product of two primes (erdos_700.variants.prime_mul), with a further example. The characterisation itself is open; we state it as the (unknown) predicate that is equivalent to being such an n.
∀ (n : ℕ), ¬Nat.Prime n → 1 < n → (Erdos700.f n = n / Erdos700.P n ↔ True)OpenStatement only, no proof