Erdős Problem 313

References:

• erdosproblems.com/313
• OEIS: A054377 (Primary pseudoperfect numbers)

def Erdos313.erdos_313_solutions : Set (ℕ × Finset ℕ)

This set contains all solutions (m, P) to the Erdős problem 313. A solution is a pair where m is an integer ≥ 2 and P is a non-empty, finite set of distinct prime numbers, such that the sum of the reciprocals of the primes in P equals 1 - 1/m.

Equations

• Erdos313.erdos_313_solutions = {(m, P) : ℕ × Finset ℕ | 2 ≤ m ∧ P.Nonempty ∧ (∀ p ∈ P, Nat.Prime p) ∧ ∑ p ∈ P, 1 / ↑p = 1 - 1 / ↑m}

theorem Erdos313.erdos_313_conjecture : erdos_313_solutions.Infinite ↔ sorry

Are there infinitely many pairs (m, P) where m ≥ 2 is an integer and P is a set of distinct primes such that the following equation holds: $\sum_{p \in P} \frac{1}{p} = 1 - \frac{1}{m}$?

theorem Erdos313.erdos_313_solution_6_2_3 : (6, {2, 3}) ∈ erdos_313_solutions

theorem Erdos313.erdos_313_solution_42_2_3_7 : (42, {2, 3, 7}) ∈ erdos_313_solutions

def Erdos313.IsPrimaryPseudoperfect (n : ℕ) : Prop

An integer n is a primary pseudoperfect number if it is the denominator m in a solution (m, P) to the Erdős 313 problem.

Equations

• Erdos313.IsPrimaryPseudoperfect n = ∃ (P : Finset ℕ), (n, P) ∈ Erdos313.erdos_313_solutions

theorem Erdos313.erdos_313.variant.primary_pseudoperfect_are_infinite : {n : ℕ | IsPrimaryPseudoperfect n}.Infinite

It is conjectured that the set of primary pseudoperfect numbers is infinite.

theorem Erdos313.exists_at_least_eight_primary_pseudoperfect : 8 ≤ {n : ℕ | IsPrimaryPseudoperfect n}.encard

There are at least 8 primary pseudoperfect numbers.