Littlewood's conjecture: is $\liminf n\,\|n\alpha\|\,\|n\beta\| = 0$ for all reals $\alpha,\beta$? (Erdős #495)
Statement
Let $\alpha, \beta \in \mathbb{R}$, and let $\|x\|$ denote the distance from $x$ to the nearest integer. Is it true that $$\liminf_{n\to\infty} n\,\|n\alpha\|\,\|n\beta\| = 0?$$ That is, can every pair of reals be simultaneously approximated so that the product of the two approximation errors beats the $1/n$ rate by an arbitrary factor: for every $\epsilon>0$ there exist infinitely many $n$ with $n\,\|n\alpha\|\,\|n\beta\| < \epsilon$?
Acceptance. FULLY RESOLVES: a complete proof that the liminf is $0$ for all real pairs (machine-checkable Lean/Coq preferred, else a full written proof with all steps); OR a disproof: an explicitly defined pair $(\alpha,\beta)$ together with a proof that $\liminf_n n\|n\alpha\|\|n\beta\| > 0$. Numerical evidence alone can never close either direction. ADVANCES: (a) a proof of the conjecture for a new explicit family of pairs not covered by the results stated in the background (e.g. pairs from specified higher-degree fields, or specified classes of badly approximable numbers), with proof; (b) a quantitative or effective strengthening of a frontier result stated in the background (e.g. an effective version of the dimension-zero exceptional-set theorem, or explicit rates), with proof; (c) a machine-verified (Lean) formalization of a frontier result — the Cassels–Swinnerton-Dyer theorem or the Pollington–Velani theorem — building on the already-formalised statement; (d) as a weakest tier, a reproducible certified computation (interval arithmetic, code included) of $\min_{n\le N} n\|n\alpha\|\|n\beta\|$ for named badly approximable pairs such as $(\sqrt2,\sqrt3)$ to a record height $N$, clearly presented as evidence rather than resolution. Deliver the proof file (or compiling Lean sources), or the certified computation code plus its output table.
Background
This is the Littlewood conjecture (posed by J. E. Littlewood around 1930), included by Erdős in his 1961 problem collection [Er61] and listed as open on erdosproblems.com/495 (fetched 2026-07-13, status 'open', tagged 'diophantine approximation | number theory'); the page calls it 'the infamous Littlewood conjecture'. The one-variable analogue is classical: $\liminf n\|n\alpha\| \le 1$ always, and $=0$ unless $\alpha$ is badly approximable (bounded continued-fraction partial quotients), so the conjecture is only at stake when BOTH $\alpha$ and $\beta$ are badly approximable — e.g. the pair $(\sqrt2, \sqrt3)$ is already open. Known frontier (standard literature): Cassels and Swinnerton-Dyer (1955) proved the conjecture when $\alpha$ and $\beta$ lie in the same cubic number field; Pollington and Velani (2000) showed that for every badly approximable $\alpha$ the set of badly approximable $\beta$ satisfying the conjecture with $\alpha$ has full Hausdorff dimension; and the landmark result of Einsiedler, Katok, and Lindenstrauss (Annals of Mathematics, 2006), via measure rigidity for the diagonal action on $\mathrm{SL}_3(\mathbb{R})/\mathrm{SL}_3(\mathbb{Z})$, proved that the set of exceptional pairs $(\alpha,\beta)$ has Hausdorff dimension zero. The conjecture is equivalent to a statement about unbounded excursions of diagonal orbits in the space of unimodular lattices, which is why homogeneous dynamics owns the modern frontier. The statement has been formalised in Lean in the google-deepmind/formal-conjectures repository. Note the problem class is OPEN: no finite computation can resolve it — even a counterexample pair would require a proof that the liminf is positive. The attacker's tool: measure rigidity and effective equidistribution in homogeneous dynamics, continued-fraction/Ostrowski machinery for explicit families, Lean formalization of frontier results, and certified interval-arithmetic computation of $\min_{n\le N} n\|n\alpha\|\|n\beta\|$ for candidate extremal pairs as an evidence-grade side-channel.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #495 (T. F. Bloom) | website |
| REF-02 | Littlewood conjecture — Wikipedia (survey of known results) | website |
| REF-03 | Formalised Lean statement of Erdős #495 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.