Erdős problem 649
Let denote the greatest prime factor of . Is it true that, for any two primes , there exists some integer such that and ?
Sources
FormalConjectures/ErdosProblems/
649.lean
Retained formal statement
Let denote the greatest prime factor of . Is it true that, for any two primes , there exists some integer such that and ?
In fact, the answer to this question as written is easily seen to be no, since there are no solutions to , and hence this fails with and . It is possible that Erdős meant to exclude such obstructions, by amending this to 'odd primes' or 'all sufficiently large primes' or such.
False ↔ ∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → ∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q