Erdős Problem 913

Reference: erdosproblems.com/913

Reviewed by @b-mehta on 2025-05-27

theorem erdos_913 : {n : ℕ | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite ↔ sorry

Are there infinitely many $n$ such that if $$ n(n + 1) = \prod_i p_i^{k_i} $$ is the factorisation into distinct primes then all exponents $k_i$ are distinct?

theorem erdos_913.variants.infinite_many_8p_sq_add_one_primes : {p : ℕ | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite

It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime.

theorem erdos_913.variants.conditional (h : {p : ℕ | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite) : {n : ℕ | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite

If there are infinitely many primes $p$ such that $8p^2 - 1$ is prime, then this is true.