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
Even with such amendments, this problem is false in a strong sense: Alan Tong has provided the following elegant elementary proof that, for any given prime , there are infinitely many primes such that this statement is false: let be the product of all primes , and choose a prime congruent to modulo . If is the greatest prime divisor of then, using quadratic reciprocity, every prime divisor of is a quadratic residue modulo , and hence is a quadratic residue modulo . On the other hand, since we know that is not a quadratic residue modulo , and hence , so it is impossible for .
∀ (p : ℕ), Nat.Prime p → {q | Nat.Prime q ∧ ¬∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Infinite