---

Claim. Let $P(m)$ denote the greatest prime factor of $m$, and call a pair of distinct primes $\{p,q\}$ strange when no integer $n\ge2$ has $P(n)P(n+1)=pq$. The main theorem of the Lean file, erdos_649 (alias infinite_strange_pairs): there are infinitely many primes $q$ such that $\{2,q\}$ is a strange pair. For such a $q$ no $n$ has $P(n)=2$ and $P(n+1)=q$, so the statement of Problem 649, which asks for such an $n$ for every pair of primes, is false. The statement proved is the one Problem 6 of the 12th Romanian Master of Mathematics competition (2020) asked for, which the site's commentary records beside Tong's and Sampaio's arguments without an author or a citation of its published solution; the competition result has no claim page of its own, for the reason the problem page records, and this page carries it through the Lean file, which declares itself a formalization of the competition's solution and names no informal author.

Submission note. Posted to the site's forum by Boris Alexeev on 7 February 2026:

[This comment has been updated.]

All of the results from the problem description above have been formalized by ChatGPT and Aristotle.

This includes $(2,7)$, Tong's counterexamples, Tong's question (no answer), Sampaio's counterexample, and a solution to Problem 6 in the 12th Romanian Master of Mathematics Competitions in 2020.

Previously, this file assumed Mahler's result (mentioned parenthetically), but it has been updated to avoid that dependence. Now it uses the formalization of part of Problem 368. Because that file is imported, it cannot be typechecked on "Lean 4 Web". But I still have an old version around. Type-check it online!

Argument. As the file's docstrings describe it: if $2<q_1<q_2$ are primes with the same multiplicative order of $2$, then $\{2,q_1\}$ is strange. For suppose $n\ge2$ has $P(n)P(n+1)=2q_1$: the term with greatest prime factor $2$ is a power $2^k$, and the other term is divisible by $q_1$, so $2^k\equiv-1$ or $2^k\equiv1\pmod{q_1}$; since $2$ has the same order modulo $q_2$, the same congruence holds modulo $q_2$, so $q_2$ divides that term, which contradicts its greatest prime factor being $q_1<q_2$. And for every prime $p>5$ the number $2^{2p}+1$ has at least two prime factors $q_1,q_2>5$, each with $2$ of order $4p$. The primes $q$ so produced grow with $p$, which gives infinitely many strange pairs $\{2,q\}$.

Companion theorems. The same file proves conjecture_false, the pair $(p,q)=(2,7)$; tong_counterexamples, the family of Tong's claim; and sampaio_counterexample, the pair of Sampaio's claim; it states Tong's question as the proposition tong_question without an answer. Those two theorems are formalizations of the named claimants' results and are recorded as links on their pages; this page records only the strange-pairs theorem, which has no named informal author.

Depends on. Nothing in this wiki.

Acceptance. Formalized. This corpus's verification built Alexeev's lean-proofs repository at the pinned commit 8822f7dd of 2026-09-15, the third link above, in its src/latest folder (Lean v4.33.0, Mathlib v4.33.0, the folder's toolchain), compiling the module ErdosProblems.Erdos649 of the file src/latest/ErdosProblems/Erdos649.lean, the module ErdosProblems.Erdos368b that it imports, and the repository's comparator challenge for the problem, src/latest/ComparatorChallenges/ErdosProblems/Erdos649.lean, and checked the axioms of Erdos649.erdos_649, which are exactly propext, Classical.choice and Quot.sound. The challenge states that theorem without proof together with the definitions Erdos649.P and Erdos649.StrangePair that its type reaches, and the fingerprint of the theorem and of both definitions was found identical in the module and the challenge; the module's definitions and statement are textually the challenge's, the imported module defines nothing in the Erdos649 namespace, and neither file contains sorry, axiom or native_decide. The statement was audited clause by clause against the problem's Statement: P is the greatest prime factor for $n\ge2$, with the junk value $0$ at $n=0$ and $n=1$, and StrangePair is the definition stated above, so each $q$ in the theorem's set is a prime other than $2$ with $P(n)P(n+1)\ne2q$ for every $n\ge2$. Hence no natural number $n$ has $P(n)=2$ and $P(n+1)=q$: for $n\ge2$ the product would be $2q$, and $P(0)=P(1)=0$. A negative $n$ reduces to the swapped pair, $P(m)=q$ and $P(m+1)=2$ with $m=-n-1$, which is excluded in the same way. So the theorem gives infinitely many pairs of distinct primes, $2$ and such a $q$, with no such $n$, and refutes the Statement whether or not it allows $p=q$: the full-scope disproof this page claims. The build certifies erdos_649 alone: the same file proves conjecture_false, tong_counterexamples and sampaio_counterexample, but no challenge compares them, so this build gives no formalized evidence for Tong's page or Sampaio's page. Boris Alexeev published the file in that repository (GitHub plby) and announced it in the site's thread on 2026-02-07 as a formalization, by ChatGPT and Aristotle, of every result in the problem's description, the Romanian Master of Mathematics solution among them; Alexeev is the claimant as the publisher. An earlier version of the file took Mahler's bound as a hypothesis; the archived copy linked above, of 2026-02-17, names ChatGPT and Aristotle as the systems that formalized the results, 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, uses native_decide twice and can be type-checked online; its main theorem is infinite_strange_pairs. The revision built presents itself as "a Lean formalization of a solution to Erdős Problem 649" with ChatGPT, Aristotle and Boris Alexeev as formal authors and no informal author named, imports a module of the Problem 368 formalization instead, and names its main theorem erdos_649; its #print axioms line for erdos_649 (line 1123) is followed by a comment recording the output, the file's own record and written for the alias, which names only propext, Classical.choice and Quot.sound, and its last line (1126) declares infinite_strange_pairs an alias of erdos_649. The build is of that revision, not of the file announced on 2026-02-07 or of the archived copy. The formal-conjectures statement erdos_649 has a sorry body whose formal_proof attribute points at line 488 of the revision built, the sampaio_counterexample theorem, and the collection's variant erdos_649.variants.rmm_2020 states the competition's result with a sorry body; the statement file is not a formalization link. A thread post of 2026-06-01 reports a revision removing the proof's two uses of native_decide, in the Jayyhk/erdos-lean folder linked above. Not reviewed: the site's label refers to the file and its remarks record the competition's result without an author, but no outside reviewer of the file is named and no examination of it is published. Not refereed: the file has no journal publication.