Skip to content

Erdős problem 307

Start work

Are there two finite set of primes PP and QQ such that

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

307.lean

Retained formal statement1 of 4

Are there two finite set of primes PP and QQ such that

1=(∑p∈P1p)(∑q∈Q1q) 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._

FormalConjectures/ErdosProblems/307.leanErdos307.erdos_3071 lineExact file
sorry ↔ ∃ P Q, (∀ p ∈ P, Nat.Prime p) ∧ (∀ q ∈ Q, Nat.Prime q) ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹
OpenStatement only, no proof