1209.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

13 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 1209

References:

erdosproblems.com/429
erdosproblems.com/1102
erdosproblems.com/1209
[Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.

Imports (1)

FormalConjecturesUtil

theorem Erdos1209.exists_prime_gt_not_prime_add For every k ≥ 1 and bound m, there is a prime p > m such that k + p is composite: take a prime q > k and, by Dirichlet, a prime p > max m q with p ≡ -k (mod q) line 40 source
Source documentation
For every k ≥ 1 and bound m, there is a prime p > m such that k + p is composite: take a prime q > k and, by Dirichlet, a prime p > max m q with p ≡ -k (mod q).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, LT.lt, Nat.Prime, Not, HAdd.hAdd
Proof uses: Nat.exists_infinite_primes, NeZero, NeZero.mk, Nat.Prime.ne_zero, IsUnit, ZMod, Neg.neg, IsUnit.neg, Eq.mpr, Nat.Coprime, id, Eq, congrArg, propext, ZMod.isUnit_iff_coprime, Iff.mp, Nat.coprime_comm, Iff.mpr, Dvd.dvd, Nat.Prime.coprime_iff_not_dvd and 43 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem exists_prime_gt_not_prime_add (k m : ℕ) (hk : 1 ≤ k) :
    ∃ p, m < p ∧ p.Prime ∧ ¬ (k + p).Prime := by
…
```
def Erdos1209.seq The counterexample sequence: a 0 is a prime at least f 0, and a (k + 1) is a prime larger than a k and f (k + 1) with (k + 1) + a (k + 1) composite line 58 source
Source documentation
The counterexample sequence: a 0 is a prime at least f 0, and a (k + 1) is a prime larger than a k and f (k + 1) with (k + 1) + a (k + 1) composite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def seq (f : ℕ → ℕ) : ℕ → ℕ
  | 0 => Classical.choose (Nat.exists_infinite_primes (f 0))
  | k + 1 => Classical.choose (exists_prime_gt_not_prime_add (k + 1) (max (seq f k) (f (k + 1)))
      (by omega))

/-- The defining properties of `seq f 0`. -/
@[category API, AMS 11]
```
Mentions: Erdos1209.exists_prime_gt_not_prime_add, AMS
theorem Erdos1209.seq_zero_spec The defining properties of seq f 0 line 65 source
Source documentation
The defining properties of seq f 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LE.le, OfNat.ofNat, Erdos1209.seq, Nat.Prime
Proof uses: Classical.choose_spec, Nat.exists_infinite_primes
4 instances, coercions and auxiliary constants left out.
```
theorem seq_zero_spec (f : ℕ → ℕ) : f 0 ≤ seq f 0 ∧ (seq f 0).Prime :=
…
```
Mentions: Erdos1209.seq
theorem Erdos1209.seq_succ_spec The defining properties of seq f (k + 1) line 70 source
Source documentation
The defining properties of seq f (k + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LT.lt, Max.max, Erdos1209.seq, HAdd.hAdd, OfNat.ofNat, Nat.Prime, Not
Proof uses: Classical.choose_spec, Erdos1209.exists_prime_gt_not_prime_add, Decidable.byContradiction, LE.le
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem seq_succ_spec (f : ℕ → ℕ) (k : ℕ) :
    max (seq f k) (f (k + 1)) < seq f (k + 1) ∧ (seq f (k + 1)).Prime ∧
      ¬ ((k + 1) + seq f (k + 1)).Prime :=
…
```
Mentions: Erdos1209.seq
theorem Erdos1209.erdos_1209.parts.i Let $A=\{a_1a_{k-1}$ be a prime such that $a_k+k\equiv 0\pmod{q_k}$, where $q_k$ is some prime not dividing $k$ line 89 source
Source documentation
Let $A=\{a_1<a_2<\cdots\}$ be a sequence of integers which tends to infinity sufficiently fast. If there is an $n$ such that all $n+a_k$ are primes then must there exist infinitely many such $n$?
Erdős [Er80] wrote 'unless I overlook a trivial way of getting a counterexample these questions are quite hopeless'. There is indeed a trivial counterexample (a variant of the construction in [erdosproblems.com/429]): define $a_1=2$ and for $k\geq 2$ let $a_k>a_{k-1}$ be a prime such that $a_k+k\equiv 0\pmod{q_k}$, where $q_k$ is some prime not dividing $k$. This sequence can be made to grow arbitrarily fast
See also [erdosproblems.com/429] and [erdosproblems.com/1102].

L4DEL explanation
Let $A=\{a_1a_{k-1}$ be a prime such that $a_k+k\equiv 0\pmod{q_k}$, where $q_k$ is some prime not dividing $k$. This sequence can be made to grow arbitrarily fast See also [erdosproblems.com/429] and [erdosproblems.com/1102].
Sources and attribution: Pinned Lean source (1646ca16afd6)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Exists, Nat, StrictMono, LE.le, Nat.Prime, HAdd.hAdd, Set.Infinite, Set.ofPred
Proof uses: Iff.intro, False.elim, Erdos1209.seq, strictMono_nat_of_lt_succ, lt_of_le_of_lt, Max.max, OfNat.ofNat, le_max_left, And.left, LT.lt, And, Not, Erdos1209.seq_succ_spec, Nat.casesAuxOn, Eq, Erdos1209.seq_zero_spec, Eq.symm, LT.lt.le, le_max_right, Eq.refl and 15 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.i :
    answer(False) ↔
      ∃ f : ℕ → ℕ, ∀ a : ℕ → ℕ, StrictMono a → (∀ k, f k ≤ a k) →
        (∃ n, ∀ k, (n + a k).Prime) →
        {n | ∀ k, (n + a k).Prime}.Infinite := by
…
```
theorem Erdos1209.exists_prime_gt_not_squarefree_add For every k ≥ 1 and bound m, there is a prime p > m such that k + p is not squarefree: take a prime q > k and, by Dirichlet, a prime p > m with p ≡ -k (mod q ^ 2) line 120 source
Source documentation
For every k ≥ 1 and bound m, there is a prime p > m such that k + p is not squarefree: take a prime q > k and, by Dirichlet, a prime p > m with p ≡ -k (mod q ^ 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, LT.lt, Nat.Prime, Not, Squarefree, HAdd.hAdd
Proof uses: Nat.exists_infinite_primes, NeZero, HPow.hPow, NeZero.mk, pow_ne_zero, Nat.Prime.ne_zero, IsUnit, ZMod, Neg.neg, IsUnit.neg, Eq.mpr, Nat.Coprime, id, Eq, congrArg, propext, ZMod.isUnit_iff_coprime, Nat.Coprime.pow_right, Iff.mp, Nat.coprime_comm and 47 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem exists_prime_gt_not_squarefree_add (k m : ℕ) (hk : 1 ≤ k) :
    ∃ p, m < p ∧ p.Prime ∧ ¬ Squarefree (k + p) := by
…
```
def Erdos1209.seq' The counterexample sequence for the squarefree variant line 139 source
Source documentation
The counterexample sequence for the squarefree variant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def seq' (f : ℕ → ℕ) : ℕ → ℕ
  | 0 => Classical.choose (Nat.exists_infinite_primes (f 0))
  | k + 1 => Classical.choose (exists_prime_gt_not_squarefree_add (k + 1)
      (max (seq' f k) (f (k + 1))) (by omega))

/-- The defining properties of `seq' f (k + 1)`. -/
@[category API, AMS 11]
```
Mentions: Erdos1209.exists_prime_gt_not_squarefree_add, AMS
theorem Erdos1209.seq'_succ_spec The defining properties of seq' f (k + 1) line 146 source
Source documentation
The defining properties of seq' f (k + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LT.lt, Max.max, Erdos1209.seq', HAdd.hAdd, OfNat.ofNat, Nat.Prime, Not, Squarefree
Proof uses: Classical.choose_spec, Erdos1209.exists_prime_gt_not_squarefree_add, Decidable.byContradiction, LE.le
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem seq'_succ_spec (f : ℕ → ℕ) (k : ℕ) :
    max (seq' f k) (f (k + 1)) < seq' f (k + 1) ∧ (seq' f (k + 1)).Prime ∧
      ¬ Squarefree ((k + 1) + seq' f (k + 1)) :=
…
```
Mentions: Erdos1209.seq'
theorem Erdos1209.erdos_1209.parts.ii What if we ask for $n+a_k$ to be squarefree instead of prime? line 158 source
Source documentation
What if we ask for $n+a_k$ to be squarefree instead of prime?
A similar construction provides a counterexample to the squarefree question.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, False, Exists, Nat, StrictMono, LE.le, Squarefree, HAdd.hAdd, Set.Infinite, Set.ofPred
Proof uses: Iff.intro, False.elim, And, OfNat.ofNat, Classical.choose, Nat.Prime, Nat.exists_infinite_primes, Classical.choose_spec, Erdos1209.seq', strictMono_nat_of_lt_succ, lt_of_le_of_lt, Max.max, le_max_left, And.left, LT.lt, Not, Erdos1209.seq'_succ_spec, Nat.casesAuxOn, Eq, Eq.symm and 20 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.ii :
    answer(False) ↔
      ∃ f : ℕ → ℕ, ∀ a : ℕ → ℕ, StrictMono a → (∀ k, f k ≤ a k) →
        (∃ n, ∀ k, Squarefree (n + a k)) →
        {n | ∀ k, Squarefree (n + a k)}.Infinite := by
…
```
theorem Erdos1209.erdos_1209.parts.iii.a Are there $n$ such that $n+2^{2^k}$ is always a prime? sorry line 198 source
Source documentation
Are there $n$ such that $n+2^{2^k}$ is always a prime?
ebarschkis and GPT have proved that there are no $n$ such that $n+2^{2^k}$ is always prime: let $n\geq 3$ be any odd integer. If $k$ is chosen sufficiently large, and $p=n+2^{2^{k}}$ is prime, then the multiplicative order of $2^{2^k}\pmod{p}$, say $m$ is odd, and hence if $l$ is chosen such that $2^l\equiv 1\pmod{m}$ then $p\mid n+2^{2^{k+rl}}$ for all $r\geq 1$.
This was formalized in Lean by Barschkis using ChatGPT.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.iii.a :
    answer(False) ↔ ∃ n : ℕ, ∀ k : ℕ, (n + 2 ^ (2 ^ k)).Prime := by
…
```
theorem Erdos1209.erdos_1209.parts.iii.b Are there $n$ such that $n+2^{2^k}$ is always squarefree? sorry line 206 source
Source documentation
Are there $n$ such that $n+2^{2^k}$ is always squarefree?

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Squarefree, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.iii.b :
    answer(sorry) ↔ ∃ n : ℕ, ∀ k : ℕ, Squarefree (n + 2 ^ (2 ^ k)) := by
…
```
theorem Erdos1209.erdos_1209.parts.iii.c Are there $n$ such that $n+2^{2^k}$ is infinitely often a prime? sorry line 214 source
Source documentation
Are there $n$ such that $n+2^{2^k}$ is infinitely often a prime?

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.iii.c :
    answer(sorry) ↔ ∃ n : ℕ, {k | (n + 2 ^ (2 ^ k)).Prime}.Infinite := by
…
```
theorem Erdos1209.erdos_1209.parts.iii.d Are there $n$ such that $n+2^{2^k}$ is infinitely often squarefree? sorry line 222 source
Source documentation
Are there $n$ such that $n+2^{2^k}$ is infinitely often squarefree?

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, Set.Infinite, Set.ofPred, Squarefree, HAdd.hAdd, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1209.parts.iii.d :
    answer(sorry) ↔ ∃ n : ℕ, {k | Squarefree (n + 2 ^ (2 ^ k))}.Infinite := by
…
```