The board / number theory / #962
Erdős Problem #962
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).
`Erdos962Prop n k` : there exists \(m \le n\) such that each of \(m+1, \ldots, m+k\) has a prime divisor strictly larger than \(k\).
Let \(k(n)\) be the maximal \(k\) such that there exists \(m \le n\) with \(m+1, \ldots, m+k\) each divisible by a prime \(> k\).
Main conjecture: \(\log k(n) \le (\log n)^{(1/2 + o(1))}\)
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/962.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA327909
Original pageerdosproblems.com/962
Attempts
submit one →Read our working report →
Via Laishram--Murty's published Grimm-function theorem, \(k(n)<n^{0.46}=n^{1/2-1/25}\) for all sufficiently large \(n\); the main \(\log k(n)\leq(\log n)^{1/2+o(1)}\) conjecture remains open, and the
PARTIAL