Erdős Problem 972

Reference: erdosproblems.com/972

def Erdos972.primeSet (α : ℝ) : Set ℕ

The set of primes p such that Nat.floor (α * p) is also prime.

Equations

• Erdos972.primeSet α = {p : ℕ | Nat.Prime p ∧ Nat.Prime ⌊α * ↑p⌋₊}

theorem Erdos972.erdos_972 : sorry ↔ ∀ α > 1, Irrational α → (primeSet α).Infinite

Erdős problem 972. Let $\alpha > 1$ be irrational. Are there infinitely many primes $p$ such that $\lfloor p\alpha \rfloor$ is also prime?