Erdős problem 698 · problems.science

Is there some $h(n)\to \infty$ such that for all $2\leq i<j\leq n/2$ $\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \geq h(n)?$

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

698.lean

Retained formal statement2 of 4

This was resolved by Bergman [Be11], who proved that for any $2\leq i<j\leq n/2$ $\textrm{gcd}\left( \binom{n}{i},\binom{n}{j}\right) \gg n^{1/2}\frac{2^i}{i^{3/2}},$ where the implied constant is absolute.

FormalConjectures/ErdosProblems/698.leanErdos698.erdos_698.variants.bergman2 linesExact file

1∃ c,2  0 < c ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → c * (√↑n * 2 ^ i / (↑i * √↑i)) ≤ ↑((n.choose i).gcd (n.choose j))

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science