Erdős problem 307

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

307.lean

Retained formal statement4 of 4

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

FormalConjectures/ErdosProblems/307.leanErdos307.erdos_307.variants.coprime_one_notMem6 linesExact file

1sorry ↔2  ∃ P Q,3    0 ∉ P ∩ Q ∧4      1 ∉ P ∪ Q ∧5        1 < P.card ∧6          1 < Q.card ∧ (↑P).Pairwise Nat.Coprime ∧ (↑Q).Pairwise Nat.Coprime ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹

OpenStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures4
statement retained
VibeMathed0
not observed here
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean0
not observed here
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki0
not observed here
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 307.lean4