Erdős Problem 306

Reference: erdosproblems.com/306

theorem erdos_306 : (∀ (q : ℚ), 0 < q → Squarefree q.den → ∃ (k : ℕ) (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ StrictMono n ∧ (∀ i ∈ Finset.Icc 1 k, ArithmeticFunction.cardDistinctFactors (n ↑i) = 2 ∧ ArithmeticFunction.cardFactors (n ↑i) = 2) ∧ q = ∑ i ∈ Finset.Icc 1 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 erdos_306.variant.integer_three_primes (m : ℕ) (h : 0 < m) : ∃ (k : ℕ) (n : Fin (k + 1) → ℕ), n 0 = 1 ∧ ∀ i < k, n ↑i < n (↑i + 1) ∧ (∀ i ∈ Finset.Icc 1 k, ArithmeticFunction.cardDistinctFactors (n ↑i) = 3 ∧ ArithmeticFunction.cardFactors (n ↑i) = 3) ∧ ↑m = ∑ i ∈ Finset.Icc 1 k, 1 / ↑(n ↑i)

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