Erdős Problem 307

Reference: erdosproblems.com/307

theorem Erdos307.erdos_307 : sorry ↔ ∃ (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 : sorry ↔ ∃ (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$.

theorem Erdos307.erdos_307.barrier {P Q : Finset ℕ} (hP : ∀ p ∈ P, Nat.Prime p) (hQ : ∀ q ∈ Q, Nat.Prime q) (hQne : Q.Nonempty) (heq : 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹) : 59 ≤ (P ∪ Q).card ∧ 4 * 10 ^ 112 ≤ (∏ p ∈ P, ↑p) ^ 2

A machine-checked barrier for Erdős 307 (Bonfioli, 2026): any solution with Q nonempty uses at least 59 primes in total, and (∏_{p ∈ P} p)² ≥ 4·10¹¹² — i.e. ∏_{p ∈ P} p ≥ 2·10⁵⁶ (and, by symmetry, the same for ∏ Q); so no solution lies below a prime-product of 2.09·10⁵⁶. The full sorry-free proof is in the linked repository (Closed.lean at tag v1.0.0): the left conjunct is card_ge_59, the right is erdos307_barrier_closed. The only non-logical input is a native_decide evaluation of the first 59 primes; the axioms are propext, Classical.choice, Quot.sound together with that native_decide.