The board / number theory / #951
Erdős Problem #951
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).
A sequence `a : ℕ → ℝ` is said to have property `Erdos951Prop` if for any pair of distinct finitely supported sequences `k l : ℕ →₀ ℕ` their corresponding Beurling integers are of distance at least one apart.
If `1 < a 0 < ...` has property `Erdos951Prop`, is it true that `#{a i ≤ x} ≤ π x`?
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/951.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/951
Attempts
submit one →Read our working report →
Exact rational verification proves 4.309405275 < m(3) < 4.3094055 and hence a literal finite-x counterexample below 4.3094055; the asymptotic Erdős/Shapiro question remains open.
PARTIAL