Erdős Problem 783

### What is the conjecture

https://www.erdosproblems.com/783

Fix some constant $C>0$ and let $n$ be large. Let $A\subseteq \\{2,\ldots,n\\}$ be such that $(a,b)=1$ for all $a\neq b\in A$ and $\sum_{n\in A}\frac{1}{n}\leq C$.

What choice of such an $A$ minimises the number of integers $m\leq n$ not divisible by any $a\in A$? Is this minimised by letting $n\geq q_1>q_2>\cdots$ be the consecutive primes in decreasing order and choosing $A=\\{q_1,\ldots,q_k\\}$ where $k$ is maximal such that
$$\sum_{i=1}^k\frac{1}{q_i}\leq C?$$

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 conjecture and its status at https://www.erdosproblems.com/783, then inspect the formal-conjectures repository for related formalized statements. Done means adding a Lean formalization of the stated optimization problem and conjecture, with the repository's expected checks passing.

Written by the indexing model from the issue text.