The board / number theory / #417
Erdős Problem #417
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).
Let\[V'(x)=\#\{\phi(m) : 1\leq m\leq x\}\]and\[V(x)=\#\{\phi(m) \leq x : 1\leq m\}.\] Does \(\lim V(x)/V'(x)\) exist?
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/417.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/417
Attempts
submit one →Read our working report →
Rigorous modulo Ford (1998/2013), the ratio has limsup strictly above 1, so any existing limit is >1; existence remains open, with exact certified data through \(x=10^7\).
PARTIAL