Erdős problem 306

If $a/b \in \mathbb{Q}_{>0}$ and $b$ is squarefree, can $a/b$ always be written as a finite sum of reciprocals of distinct products of two distinct primes?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

306.lean

Retained formal statement1 of 2

Let $\frac a b\in \mathbb{Q}_{>0}$ with $b$ squarefree. Are there integers $1 < n_1 < \dots < n_k$ , each the product of two distinct primes, such that $\frac{a}{b}=\frac{1}{n_1}+\cdots+\frac{1}{n_k}$ ?

FormalConjectures/ErdosProblems/306.leanErdos306.erdos_30610 linesExact file

1True ↔2  ∀ (q : ℚ),3    0 < q →4      Squarefree q.den →5        ∃ k n,6          n 0 = 1 ∧7            StrictMono n ∧8              (∀ i ∈ Finset.Icc 1 (Fin.last k),9                  ArithmeticFunction.cardDistinctFactors (n i) = 2 ∧ ArithmeticFunction.cardFactors (n i) = 2) ∧10                q = ∑ i ∈ Finset.Icc 1 (Fin.last k), 1 / ↑(n i)

OpenStatement only, no proof