The board / number theory / #354
Erdős Problem #354
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The sequence `⌊a⌋, ⌊γ * a⌋, ⌊γ ^ 2 * a⌋, ..., ⌊γ ^ i * a⌋, ...`.
The sequence `⌊a⌋, ⌊b⌋, ⌊γ * a⌋, ⌊γ * b⌋, ... ⌊γ ^ i * a⌋, ⌊γ ^ i * b⌋, ...`
Let \(\alpha,\beta\in \mathbb{R}_{>0}\) such that \(\alpha/\beta\) is irrational. Is the multiset \[\{ \lfloor \alpha\rfloor,\lfloor 2\alpha\rfloor,\lfloor 4\alpha\rfloor,\ldots\}\cup \{ \lfloor \beta\rfloor,\lfloor 2\beta\rfloor,\lfloor 4\beta\rfloor,\ldots\}\] complete?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/354.Prizenone
Topicsnumber theory, complete sequences
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/354
Attempts
submit one →Read our working report →
exact computer-assisted thresholds are proved for a 16-cell rectangle, including greatest exception 558 for the irrational pair (10√2,10√3), and the remaining uniform finite-interval lemma is isolated
PARTIAL