Erdős problem 306
If and is squarefree, can always be written as a finite sum of reciprocals of distinct products of two distinct primes?
Sources
FormalConjectures/ErdosProblems/
306.lean
Retained formal statement
Let with squarefree. Are there integers , each the product of two distinct primes, such that ?
True ↔ ∀ (q : ℚ), 0 < q → Squarefree q.den → ∃ k n, n 0 = 1 ∧ StrictMono n ∧ (∀ i ∈ Finset.Icc 1 (Fin.last k), ArithmeticFunction.cardDistinctFactors (n i) = 2 ∧ ArithmeticFunction.cardFactors (n i) = 2) ∧ q = ∑ i ∈ Finset.Icc 1 (Fin.last k), 1 / ↑(n i)OpenStatement only, no proof