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 statement3 of 4

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=(1+15)(12+13) 1=\left(1+\frac{1}{5}\right)\left(\frac{1}{2}+\frac{1}{3}\right) and 1=(1+141)(12+13+17). 1=\left(1+\frac{1}{41}\right)\left(\frac{1}{2}+\frac{1}{3}+\frac{1}{7}\right).

FormalConjectures/ErdosProblems/307.leanErdos307.erdos_307.variants.coprime5 linesExact file
True ↔  ∃ P Q,    0 ∉ P ∩ Q ∧      1 < P.card ∧        1 < Q.card ∧ (↑P).Pairwise Nat.Coprime ∧ (↑Q).Pairwise Nat.Coprime ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹
TextbookStatement only, no proof