Erdős Problem 855

Reference: erdosproblems.com/855

This is an "eventually" formulation of the Second Hardy–Littlewood conjecture.

theorem Erdos855.erdos_855 : True ↔ ∀ᶠ (x : ℕ) (y : ℕ) in Filter.atTop, (x + y).primeCounting ≤ x.primeCounting + y.primeCounting

Erdős Problem 855 (Segal's conjecture): $\pi(x + y) \le \pi(x) + \pi(y)$ for sufficiently large $x, y$.