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

Let f(n)=min1<kn/2gcd(n,(nk))f(n) = \min_{1 < k \le n/2} \gcd(n, \binom{n}{k}) and let P(n)P(n) be the largest prime dividing nn.

(a) Characterise those composite nn such that f(n)=n/P(n)f(n) = n/P(n).

Erdős–Szekeres [ErSz78] note that f(n)=n/P(n)f(n) = n/P(n) when nn is a product of two primes (erdos_700.variants.prime_mul), with n=30n = 30 a further example. The characterisation itself is open; we state it as the (unknown) predicate that is equivalent to being such an n.

FormalConjectures/ErdosProblems/700.leanErdos700.erdos_700.parts.i1 lineExact file
∀ (n : ℕ), ¬Nat.Prime n → 1 < n → (Erdos700.f n = n / Erdos700.P nTrue)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page