Erdős Problem 306

Reference: erdosproblems.com/306

theorem Erdos306.erdos_306 : (∀ (q : ℚ), 0 < q → Squarefree q.den → ∃ (k : ℕ) (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ StrictMono n ∧ (∀ i ∈ Finset.Icc 1 (Fin.last k), ArithmeticFunction.cardDistinctFactors (n i) = 2 ∧ ArithmeticFunction.cardFactors (n i) = 2) ∧ q = ∑ i ∈ Finset.Icc 1 (Fin.last k), 1 / ↑(n i)) ↔ sorry

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}$?

theorem Erdos306.erdos_306.variant.integer_three_primes (m : ℕ) (h : 0 < m) : ∃ k > 0, ∃ (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ ∀ (i : ℕ) (hik : i < k), n ⟨i, ⋯⟩ < n ⟨i + 1, ⋯⟩ ∧ (∀ i ∈ Finset.Icc 1 (Fin.last k), ArithmeticFunction.cardDistinctFactors (n i) = 3 ∧ ArithmeticFunction.cardFactors (n i) = 3) ∧ ↑m = ∑ i ∈ Finset.Icc 1 (Fin.last k), 1 / ↑(n i)

Every positive integer can be expressed as an Egyptian fraction where each denominator is the product of three distinct primes.