Number theory

Erdős 972

**Erdős problem 972.** Let

\alpha > 1

be irrational. Are there infinitely many primes

p

such that

\lfloor p\alpha \rfloor

is also prime?

References

erdosproblems.com/972

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ α > 1, Irrational α → (Erdos972.primeSet α).Infinite

What you must prove

import FormalConjectures.ErdosProblems.«972»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos972.erdos_972" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/972.lean

Source type SHA-256: sha256:fe66a71034293c43aa557b8675649c983d91a8e18dc27b01b1a08c2f1beb325b
Task id: fc-379fc029-erdos972-erdos-972-58b7112eb2-formalized-v1
Task commitment: sha256:36bb3375d1450c06e04e5a8d4f9614671cfcd4f6ae7c1c9ac042ab068d43d220

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.