The board / number theory / #1004
Erdős Problem #1004
OPENdatabase updated 2025-09-07
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).
`IsDistinctTotientRun n K` means that the values `φ(n+1), φ(n+2), ..., φ(n+K)` are all distinct.
For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c. This is an open problem.
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/1004.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA079008
Original pageerdosproblems.com/1004
Attempts
submit one →Read our working report →
proved a positive-proportion \(L=10^{-10}(\log x)^2/\log\log x\) theorem modulo PPT, reduced all polylogarithmic lengths to GHP-diagonal coverage, and exactly certified \(A(10^9)=691\); the arbitrary-
PARTIAL