Erdős Problem 929

### What is the conjecture

https://www.erdosproblems.com/929

Let $k\geq 2$ be large and let $S(k)$ be the minimal $x$ such that there is a positive density set of $n$ where
$$n+1,n+2,\ldots,n+k$$
are all divisible by primes $\leq x$.

Estimate $S(k)$ - in particular, is it true that $S(k)\geq k^{1-o(1)}$?

Status: open

### Choose either option
- [ ] I plan on working on this conjecture
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading the linked Erdős Problems page and the conjecture statement in this issue. Then inspect the repository's existing formalized conjectures to determine the expected structure and conventions; done means adding a Lean formalization of Problem 929 that matches those conventions.

Written by the indexing model from the issue text.