feat(ErdosProblems): 683

[seewoo5]

Closes #876

[YaelDillies]

Could you state https://www.erdosproblems.com/961 simultaneously?

[seewoo5]

Could you state erdosproblems.com/961 simultaneously?

Do you mean something like

/--
Erdos 961 is equivalent to Erdos 683.
-/
@[category research solved, AMS 11]
theorem erdos_683_equiv_erdos_961 :
    (∃ c > 0, ∀ n k : ℕ, 0 < k ∧ k < n → P n k > min (n - k + 1) (k ^ (1 + c))) ↔
    (∃ C > 0, ∀ᶠ k in atTop, f k < (log (k : ℝ)) ^ C) := by
  sorry

after importing Erdos961?

[YaelDillies]

I was thinking you could prove one in terms of the other