Erdős problem 698
Is there some such that for all
Sources
FormalConjectures/ErdosProblems/
698.lean
Retained formal statement
Is there some such that for all
This was resolved by Bergman [Be11], who proved that for any where the implied constant is absolute.
True ↔ ∃ h, Filter.Tendsto h Filter.atTop Filter.atTop ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → h n ≤ (n.choose i).gcd (n.choose j)SolvedStatement only, no proof