Erdős problem 495
Let . Is it true that? This is also known as the Littlewood conjecture.
Sources
FormalConjectures/ErdosProblems/
495.lean
Retained formal statement
Let . Is it true that? This is also known as the Littlewood conjecture.
True ↔ ∀ (α β : ℝ), Filter.liminf (fun n => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0OpenStatement only, no proof