E495: “Littlewood's simultaneous Diophantine approximation conjecture.”

Open

Statement	User	Model	Harness	Time
2)V2Littlewood's liminf is zero for every real β when the first parameter α is an integer.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every pair of real numbers α and β, liminf as n tends to infinity of n times the distance from nα to the…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Littlewood's liminf is zero for every real β when the first parameter α is an integer.

kernel-checked, filed Tue Aug 25 2026 05:23:48 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Every integer z embedded in the reals and every real β, with the exact root distance and liminf definitions.

1) V1 For every pair of real numbers α and β, liminf as n tends to infinity of n times the distance from nα to the nearest integer times the distance from nβ to the nearest integer is zero.

open, filed Tue Aug 25 2026 05:21:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Canonical root statement. `distToNearestInt x := |x-round x|` is copied exactly from FormalConjecturesForMathlib. The quantifiers are universal, the asymptotic operation is liminf rather than limit/limsup, and the scale is n rather than n².

Scope. All real α,β; natural n tends to infinity; `round` breaks ties toward positive infinity, which does not affect the distance.

E495:Erdős Problem #495 “Littlewood's simultaneous Diophantine approximation conjecture.”

E495: “Littlewood's simultaneous Diophantine approximation conjecture.”