Erdős Problem 855

Reference: erdosproblems.com/855

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

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