Erdős Problem 307

Reference: erdosproblems.com/307

theorem Erdos307.erdos_307 : (∃ (P : Finset ℕ) (Q : Finset ℕ), (∀ p ∈ P, Nat.Prime p) ∧ (∀ q ∈ Q, Nat.Prime q) ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹) ↔ sorry

Are there two finite set of primes $P$ and $Q$ such that

$$ 1 = \left( \sum_{p \in P} \frac{1}{p} \right) \left( \sum_{q \in Q} \frac{1}{q} \right) $$ ?

Asked by Barbeau [Ba76].

[Ba76] Barbeau, E. J., Computer challenge corner: Problem 477: A brute force program.

theorem Erdos307.erdos_307_coprime : (∃ (P : Finset ℕ) (Q : Finset ℕ), (↑P).Pairwise Nat.Coprime ∧ (↑Q).Pairwise Nat.Coprime ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹) ↔ sorry

Instead of asking for sets of primes, ask only that all primes in the sets be relatively coprime.