Skip to content

Erdős problem 649

Let P(m)P(m) denote the greatest prime factor of mm. Is it true that, for any two primes p,qp,q, there exists some integer nn such that P(n)=pP(n)=p and P(n+1)=qP(n+1)=q?

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

649.lean

Retained formal statement1 of 6

Let P(m)P(m) denote the greatest prime factor of mm. Is it true that, for any two primes p,qp,q, there exists some integer nn such that P(n)=pP(n)=p and P(n+1)=qP(n+1)=q?

In fact, the answer to this question as written is easily seen to be no, since there are no solutions to 2k1(mod7)2^k\equiv -1\pmod{7}, and hence this fails with p=2p=2 and q=7q=7. It is possible that Erdős meant to exclude such obstructions, by amending this to 'odd primes' or 'all sufficiently large primes' or such.

FormalConjectures/ErdosProblems/649.leanErdos649.erdos_6491 lineExact file
False ↔ ∀ (p q : ℕ), Nat.Prime pNat.Prime q → ∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page