Erdős Problem 307

Reference: erdosproblems.com/307

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

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.variants.coprime : True ↔ ∃ (P : Finset ℕ) (Q : Finset ℕ), 0 ∉ P ∩ Q ∧ 1 < P.card ∧ 1 < Q.card ∧ (↑P).Pairwise Nat.Coprime ∧ (↑Q).Pairwise Nat.Coprime ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹

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

Cambie has found several examples when this weakened version is true. For example, $$ 1=\left(1+\frac{1}{5}\right)\left(\frac{1}{2}+\frac{1}{3}\right) $$ and $$ 1=\left(1+\frac{1}{41}\right)\left(\frac{1}{2}+\frac{1}{3}+\frac{1}{7}\right). $$

theorem Erdos307.erdos_307.variants.coprime_one_notMem : True ↔ ∃ (P : Finset ℕ) (Q : Finset ℕ), 0 ∉ P ∩ Q ∧ 1 ∉ P ∪ Q ∧ 1 < P.card ∧ 1 < Q.card ∧ (↑P).Pairwise Nat.Coprime ∧ (↑Q).Pairwise Nat.Coprime ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹

There are no examples known of the weakened coprime version if we insist that $1\not\in P\cup Q$.