Erdős Problem 495

Reference: erdosproblems.com/495

theorem Erdos495.erdos_495 : True ↔ ∀ (α β : ℝ), Filter.liminf (fun (n : ℕ) => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0

Let $\alpha,\beta \in \mathbb{R}$. Is it true that[\liminf_{n\to \infty} n | n\alpha | | n\beta| =0]? This is also known as the Littlewood conjecture.