---

Claim. Let $P(m)$ denote the greatest prime factor of $m$. For every prime $p$ there are infinitely many primes $q$ such that no integer $n$ satisfies $P(n)=p$ and $P(n+1)=q$. The statement of Problem 649, which asks for such an $n$ for every pair of primes, is therefore false, and it stays false when both primes are required to be odd or to be large.

Argument. As the site's remarks record it, credited to Alan Tong: let $m$ be the product of the primes up to $p$ and let $q$ be any prime with $q\equiv-1\pmod{4m}$; Dirichlet's theorem gives infinitely many. Suppose $P(n)=p$. Every prime factor $r$ of $n$ is at most $p$, so $r\mid m$, and quadratic reciprocity together with $q\equiv-1\pmod{4r}$ (or $q\equiv-1\pmod 8$ for $r=2$) makes $r$ a quadratic residue modulo $q$. Hence $n$ itself is a quadratic residue modulo $q$. But $q\equiv3\pmod 4$, so $-1$ is a non-residue, $n\not\equiv-1\pmod q$, and $q\nmid n+1$; in particular $P(n+1)\neq q$. The pair $(p,q)=(2,7)$, which the site records separately as the direct check that $2^k\equiv-1\pmod 7$ has no solution, is the $p=2$ instance of this family, since $7\equiv-1\pmod 8$. The remarks add Tong's question, open there, whether for a given odd prime $q$ there are infinitely many primes $p$ with no such $n$.

Depends on. Nothing in this wiki; the argument uses only Dirichlet's theorem on primes in arithmetic progressions and quadratic reciprocity.

Acceptance. The site's curator, Thomas Bloom, wrote the argument into the problem's remarks, credits it to Tong by name, and labels the problem DISPROVED (LEAN); the community database records the status change to disproved on 2026-02-07. That documented acceptance by the site is the reviewed evidence; Bloom is independent of the claimant. No journal publication exists; the result is a remark on the site, not a paper. The site's remark is undated. The site's revision history shows the remark in its revision of 2025-10-20, and the Internet Archive's capture of the page of 2025-01-16 already prints it with the label SOLVED, where the capture of 2024-07-21 has the problem OPEN without it; this page is dated by that earliest public evidence. The thread post of 2025-08-09 linked above discusses Tong's question.

Lean. Not formalized evidence: this corpus built the development at its pinned commit for Alexeev's page and audited only erdos_649; tong_counterexamples is not compared against a challenge, so the files give this page no formalized evidence. The thread post of 2026-02-07 reports that the results of the site's remarks, this one as tong_counterexamples, were formalized in Lean by ChatGPT and Aristotle. The files live in Boris Alexeev's lean-proofs repository (GitHub plby). An earlier version of the file took Mahler's bound as a hypothesis; the archived copy linked above, of 2026-02-17, is a single file that says the results of the site's page were auto-formalized by ChatGPT and Aristotle, includes part of the Problem 368 formalization in its own namespace, proves the finiteness of the solutions for each fixed pair without Mahler's bound, uses native_decide twice and can be type-checked online. The file at the later pinned revision linked above presents itself as "a Lean formalization of a solution to Erdős Problem 649", names ChatGPT, Aristotle and Alexeev as formal authors and no informal author, lists Tong's theorem among the results it proves, imports a module of the Problem 368 formalization, and ends with a #print axioms line whose recorded output names only propext, Classical.choice and Quot.sound, the file's own record. The links above are recorded as formalizations of tong_counterexamples only; the file's main theorem, the strange-pairs argument of the 2020 Romanian Master of Mathematics competition, is an independent proof with its own claim page. The formal-conjectures statement erdos_649 has a sorry body with a formal_proof attribute pointing at that file's sampaio_counterexample theorem; the statement file is not a formalization link. A thread post of 2026-06-01 reports a revision removing the two uses of native_decide, in the Jayyhk/erdos-lean folder linked above.