Erdős Problem 1143

### What is the conjecture

Let $p_1 < p_2 < \cdots < p_u$ be primes, and let $k \geq 1$ be an integer. Define $F_k(p_1, \ldots, p_u)$ to be the minimum number of multiples of at least one of the primes $p_i$ in any interval of $k$ consecutive positive integers. The problem asks for an estimate of $F_k(p_1, \ldots, p_u)$, particularly when $k = \alpha p_u$ for some constant $\alpha > 2$. When $2 < \alpha < 3$, Erdős and Selfridge determined the exact bound, but for $\alpha > 3$, very little is known.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1143, https://erdos.renyi.hu/

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- Primes and divisibility are foundational in Mathlib (Data.Nat.Prime, NumberTheory.Basic)
- Integer intervals and membership relations are standard (Finset.range, Set.Icc)
- Cardinality and counting operations are available

Missing pieces (exactly 2; unclear/absent from search results):
- The function $F_k(p_1, \ldots, p_u)$ requires a formal definition capturing the minimum density of multiples in intervals
- Asymptotic estimation framework for functions depending on multiple parameters needs to be set up explicitly

Rating justification (1-2 sentences): The statement can be formalized using basic Mathlib definitions of primes, divisibility, and finite sets. The main effort is setting up the function $F_k$ and the interval counting logic, but no deep infrastructure is needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start by reviewing Data.Nat.Prime, NumberTheory.Basic, Finset.range, and Set.Icc, then compare existing formal-conjecture entries for conventions. Define the interval-counting function F_k and establish the requested multi-parameter estimate; done means the conjecture is stated in Lean with its counting and asymptotic components represented.

Written by the indexing model from the issue text.