Erdős problem 913

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?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

913.lean

Retained formal statement2 of 3

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

FormalConjectures/ErdosProblems/913.leanErdos913.erdos_913.variants.conditional2 linesExact file

1{p | Nat.Prime p ∧ Nat.Prime (8 * p ^ 2 - 1)}.Infinite →2  {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite

SolvedStatement only, no proof