Erdős problem 649 · problems.science

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/649.lean

Formal Conjectures

FormalConjectures/ErdosProblems/649.leanErdos649.erdos_6491 lineExact file

1False ↔ ∀ (p q : ℕ), Nat.Prime p → Nat.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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:649
PLBY Lean proofsErdosProblems.Erdos649

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 7 Feb-1 Jun, 2026
Machine
Aristotle, GPT
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science