The board / number theory / #385
Erdős Problem #385
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 \(F(n) := \max\{m + p(m) \mid \textrm{\)m < n\( composite}\}\}\) where \(p(m)\) is the least prime divisor of \(m\).
Let \(F(n) := \max\{m + p(m) \mid \textrm{\)m < n\( composite}\}\}\) where \(p(m)\) is the least prime divisor of \(m\). Is it true that \(F(n)>n\) for all sufficiently large \(n\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/385.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/385
Attempts
submit one →Read our working report →
Exactly 100 values n<=10^9 have F(n)<=n, all equalities and the last n=267680; also F(n)-n>=16384 for 521111630<=n<=10^9, while the uniform rough-semiprime lemma needed for either asymptotic question
PARTIAL