649.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 649

References:

erdosproblems.com/649
[Ma35] Mahler, Kurt, Über den grössten Primteiler spezieller Polynome zweiten Grades. Archiv für math. og naturvid (1935).
[Ro64b] Rotkiewicz, André, Sur les nombres naturels $n$ et $k$ tels que les nombres $n$ et $nk$ sont à la fois pseudopremiers. Atti Accad. Naz. Lincei Rend. Cl. Sci. Fis. Mat. Nat. (8) (1964), 816-818.

Imports (1)

FormalConjecturesUtil

theorem Erdos649.erdos_649 Let $P(m)$ denote the greatest prime factor of $m$ sorry line 49 source
Source documentation
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$?
In fact, the answer to this question as written is easily seen to be no, since there are no solutions to $2^k\equiv -1\pmod{7}$, and hence this fails with $p=2$ and $q=7$. It is possible that Erdős meant to exclude such obstructions, by amending this to 'odd primes' or 'all sufficiently large primes' or such.
The statement below assumes $p \neq q$: for $p = q$ no such $n$ exists, because $p$ would divide both $n$ and $n+1$.

depends on sorry what this means
Statement uses: Iff, False, Nat, Nat.Prime, Ne, Exists, And, Eq, Nat.maxPrimeFac, HAdd.hAdd, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649 : answer(False) ↔
    ∀ p q : ℕ, p.Prime → q.Prime → p ≠ q →
      ∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q := by
…
```
theorem Erdos649.erdos_649.variants.no_solution_two_seven In fact, the answer to this question as written is easily seen to be no, since there are no solutions to $2^k\equiv -1\pmod{7}$, and hence this fails with $p=2$ and $q=7$ line 59 source
Source documentation
In fact, the answer to this question as written is easily seen to be no, since there are no solutions to $2^k\equiv -1\pmod{7}$, and hence this fails with $p=2$ and $q=7$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Exists, Nat, And, Eq, Nat.maxPrimeFac, OfNat.ofNat, HAdd.hAdd
Proof uses: False, LT.lt, Iff.mp, Nat.one_lt_maxPrimeFac_iff, Decidable.byContradiction, HPow.hPow, Exists.intro, List.length, Nat.primeFactorsList, Nat.eq_prime_pow_of_unique_prime_dvd, Nat.Prime, Dvd.dvd, le_antisymm, Eq.rec, LE.le, Nat.le_maxPrimeFac, Nat.Prime.two_le, Nat.maxPrimeFac_dvd, HMod.hMod, Eq.mpr and 39 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649.variants.no_solution_two_seven :
    ¬ ∃ n : ℕ, n.maxPrimeFac = 2 ∧ (n + 1).maxPrimeFac = 7 := by
…
```
theorem Erdos649.erdos_649.variants.tong Even with such amendments, this problem is false in a strong sense: Alan Tong has provided the following elegant elementary proof that, for any given prime sorry line 91 source
Source documentation
Even with such amendments, this problem is false in a strong sense: Alan Tong has provided the following elegant elementary proof that, for any given prime $p$, there are infinitely many primes $q$ such that this statement is false: let $m$ be the product of all primes $\leq p$, and choose a prime $q$ congruent to $-1$ modulo $4m$. If $p$ is the greatest prime divisor of $n$ then, using quadratic reciprocity, every prime divisor of $n$ is a quadratic residue modulo $q$, and hence $n$ is a quadratic residue modulo $q$. On the other hand, since $q\equiv 3\pmod{4}$ we know that $-1$ is not a quadratic residue modulo $q$, and hence $n\not\equiv -1\pmod{q}$, so it is impossible for $q\mid n+1$.

depends on sorry what this means
Statement uses: Nat, Nat.Prime, Set.Infinite, Set.ofPred, And, Not, Exists, Eq, Nat.maxPrimeFac, HAdd.hAdd, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649.variants.tong (p : ℕ) (hp : p.Prime) :
    {q : ℕ |
      q.Prime ∧ ¬ ∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Infinite := by
…
```
theorem Erdos649.erdos_649.variants.tong_question Tong asks whether, for any given odd prime $q$, there are infinitely many primes $p$ such that there is no integer $n$ with $P(n)=p$ and $P(n+1)=q$ sorry line 101 source
Source documentation
Tong asks whether, for any given odd prime $q$, there are infinitely many primes $p$ such that there is no integer $n$ with $P(n)=p$ and $P(n+1)=q$.

depends on sorry what this means
Statement uses: Iff, True, Nat, Nat.Prime, Odd, Set.Infinite, Set.ofPred, And, Not, Exists, Eq, Nat.maxPrimeFac, HAdd.hAdd, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649.variants.tong_question : answer(sorry) ↔
    ∀ q : ℕ, q.Prime → Odd q →
      {p : ℕ |
        p.Prime ∧ ¬ ∃ n : ℕ, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q}.Infinite := by
…
```
theorem Erdos649.erdos_649.variants.sampaio Documented declaration: sampaio sorry line 114 source
Source documentation
Sampaio independently observed that the answer to Erdős' original problem is no if one of the primes can be $2$ - for example this is false with $p=19$ and $q=2$, since if $n+1=2^k$ and $19\mid n$ then (since $2$ is a primitive root modulo $19$) we must have $18\mid k$, and hence $73\mid 2^{18}-1\mid n$.

depends on sorry what this means
Statement uses: Not, Exists, Nat, And, Eq, Nat.maxPrimeFac, OfNat.ofNat, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649.variants.sampaio :
    ¬ ∃ n : ℕ, n.maxPrimeFac = 19 ∧ (n + 1).maxPrimeFac = 2 := by
…
```
theorem Erdos649.erdos_649.variants.rmm_2020 Problem 6 in the 12th Romanian Master of Mathematics Competitions in 2020 was to prove that there exist infinitely many odd primes sorry line 123 source
Source documentation
Problem 6 in the 12th Romanian Master of Mathematics Competitions in 2020 was to prove that there exist infinitely many odd primes $p$ such that, for every $n$, $P(n)P(n+1)\neq 2p$.

depends on sorry what this means
Statement uses: Set.Infinite, Nat, Set.ofPred, And, Nat.Prime, Odd, Ne, HMul.hMul, Nat.maxPrimeFac, HAdd.hAdd, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_649.variants.rmm_2020 :
    {p : ℕ | p.Prime ∧ Odd p ∧
      ∀ n : ℕ, n.maxPrimeFac * (n + 1).maxPrimeFac ≠ 2 * p}.Infinite := by
…
```