---

Claim. Let $P(m)$ denote the greatest prime factor of $m$. There is no integer $n$ with $P(n)=19$ and $P(n+1)=2$. One pair of primes without a solution disproves the statement of Problem 649, and this pair has $q=2$, which [[problems/arithmetic_functions/E0649/claims/2025_01_16_tong|Tong's family]] of odd $q$ does not reach.

Argument. As the site's remarks record it, credited to Euro Vidal Sampaio: if $P(n+1)=2$ then $n+1=2^k$, and if $19\mid n$ then $2^k\equiv1\pmod{19}$; since $2$ is a primitive root modulo $19$ this forces $18\mid k$, so $2^{18}-1\mid n$, and $73\mid 2^{18}-1$ gives $P(n)\ge73>19$. The remarks extend the argument from $19$ to every prime above $13$ having $2$ as a primitive root, through a statement they attribute to Rotkiewicz [Ro64b]: each prime $p>13$ has a prime divisor $q>p$ of $2^{p-1}-1$; the Rotkiewicz note that the site's key resolves to does not contain that statement, and the extension is recorded here as the site states it. The pair $(19,2)$ alone needs only the factorization $2^{18}-1=3^3\cdot7\cdot19\cdot73$.

Depends on. Nothing in this wiki.

Acceptance. The site's curator, Thomas Bloom, wrote the observation into the problem's remarks, credits it to Sampaio by name, and labels the problem DISPROVED (LEAN); that documented acceptance by the site is the reviewed evidence, and Bloom is independent of the claimant. No journal publication exists. 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 2026-02-07 linked above announces the Lean formalization below.

Lean. Not formalized evidence: this corpus built the development at its pinned commit for Alexeev's page and audited only erdos_649; sampaio_counterexample is not compared against a challenge, so the files give this page no formalized evidence. The thread post of 2026-02-07 reports that Sampaio's counterexample, as sampaio_counterexample, is among the results of the site's remarks formalized in Lean by ChatGPT and Aristotle. The files live in Boris Alexeev's lean-proofs repository (GitHub plby); 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, and lists Sampaio's theorem among the results it proves. The links above are recorded as formalizations of sampaio_counterexample 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 archived copy linked above, of 2026-02-17, is a single file that 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 and uses native_decide twice; the file at the later pinned revision linked above imports a module of the Problem 368 formalization instead, and the formal-conjectures statement erdos_649, a sorry body, points at its sampaio_counterexample theorem through a formal_proof attribute. 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, which also proves this counterexample; the details are on Tong's page.