Disproved; the site's label is DISPROVED (LEAN). The disproof is elementary and the site's remarks record two independent arguments, both accepted there: Tong's, for every prime $p$ infinitely many primes $q$ admit no such $n$, and Sampaio's, the pair $p=19$, $q=2$. The site's Lean qualification refers to a Lean file posted in the site's thread. Its main theorem, the 2020 Romanian Master of Mathematics argument that infinitely many primes $q$ make $\{2,q\}$ a strange pair, is a third argument, accepted on its own claim page (Alexeev, 2026): this corpus built a later revision of the file and audited that theorem's statement. The file's formalizations of Tong's and Sampaio's results are links on their pages; their statements were not audited here, so they give no formalized evidence.