Erdős problem 700 · problems.science

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

FormalConjectures/ErdosProblems/

700.lean

Retained formal statement8 of 9

Each gcd(n, C(n,k)) with 1 < k ≤ n/2 belongs to fSet n.

FormalConjectures/ErdosProblems/700.leanErdos700.f_mem1 lineExact file

1∀ (n k : ℕ), 1 < k → k ≤ n / 2 → n.gcd (n.choose k) ∈ Erdos700.fSet n

APIStatement only, no proof