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

11 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 1142

References:

erdosproblems.com/1142
A039669
[Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
[MiWe69] Mientka, W. E. and Weitzenkamp, R. C., On f-plentiful numbers, Journal of Combinatorial Theory, Volume 7, Issue 4, December 1969, pages 374-377.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Erdos1142.Erdos1142Prop The property that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$ line 46 source
Source documentation
The property that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$.
Following the OEIS A039669 convention ("Numbers n > 2 such that ..."), we require $n > 2$ to exclude the trivial cases $n \leq 2$, for which the primality condition is vacuously satisfied.

L4DEL explanation
The property that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$. Following the OEIS A039669 convention ("Numbers n > 2 such that ..."), we require $n > 2$ to exclude the trivial cases $n \leq 2$, for which the primality condition is vacuously satisfied.
Sources and attribution: Pinned Lean source (1646ca16afd6)

standard axioms: propext what this means
Statement uses: Nat
Proof uses: And, LT.lt, OfNat.ofNat, HPow.hPow, Nat.Prime, HSub.hSub
8 instances, coercions and auxiliary constants left out.
```
def Erdos1142Prop (n : ℕ) : Prop :=
…
```
theorem Erdos1142.erdos_1142 Are there infinitely many $n > 2$ such that $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$? sorry line 55 source
Source documentation
Are there infinitely many $n > 2$ such that $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$?
The only known such $n$ are $4, 7, 15, 21, 45, 75, 105$ (OEIS A039669).

L4DEL explanation
Are there infinitely many $n > 2$ such that $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$? The only known such $n$ are $4, 7, 15, 21, 45, 75, 105$ (OEIS A039669).
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Infinite, Nat, Set.ofPred, Erdos1142.Erdos1142Prop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142 :
    answer(sorry) ↔ Infinite { n | Erdos1142Prop n } := by
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.variants.mientka_weitzenkamp Mientka and Weitzenkamp [MiWe69] proved that the only $n \leq 2^{44}$ such that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$ are $4, 7, 15, 21, 45, 75, 105$ sorry line 64 source
Source documentation
Mientka and Weitzenkamp [MiWe69] proved that the only $n \leq 2^{44}$ such that $n > 2$ and $n - 2^k$ is prime for all $k \geq 1$ with $2^k < n$ are $4, 7, 15, 21, 45, 75, 105$.

depends on sorry what this means
Statement uses: Eq, Set, Nat, Set.ofPred, And, LE.le, HPow.hPow, OfNat.ofNat, Erdos1142.Erdos1142Prop, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.variants.mientka_weitzenkamp :
    { n : ℕ | n ≤ 2 ^ 44 ∧ Erdos1142Prop n } = {4, 7, 15, 21, 45, 75, 105} := by
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_4 $4$ satisfies the Erdős 1142 property: $4 - 2 = 2$ is prime line 78 source
Source documentation
$4$ satisfies the Erdős 1142 property: $4 - 2 = 2$ is prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm, le_antisymm and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_4 : Erdos1142Prop 4 := by prove_erdos_1142_prop 1
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_7 $7$ satisfies the Erdős 1142 property: $7 - 2 = 5$ and $7 - 4 = 3$ are prime line 82 source
Source documentation
$7$ satisfies the Erdős 1142 property: $7 - 2 = 5$ and $7 - 4 = 3$ are prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_7 : Erdos1142Prop 7 := by prove_erdos_1142_prop 2
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_15 $15$ satisfies the Erdős 1142 property: $15 - 2 = 13$, $15 - 4 = 11$, $15 - 8 = 7$ line 86 source
Source documentation
$15$ satisfies the Erdős 1142 property: $15 - 2 = 13$, $15 - 4 = 11$, $15 - 8 = 7$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_15 : Erdos1142Prop 15 := by prove_erdos_1142_prop 3
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_21 $21$ satisfies the Erdős 1142 property: $21 - 2 = 19$, $21 - 4 = 17$, $21 - 8 = 13$, $21 - 16 = 5$ line 91 source
Source documentation
$21$ satisfies the Erdős 1142 property: $21 - 2 = 19$, $21 - 4 = 17$, $21 - 8 = 13$, $21 - 16 = 5$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_21 : Erdos1142Prop 21 := by prove_erdos_1142_prop 4
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_45 $45$ satisfies the Erdős 1142 property: $45 - 2 = 43$, $45 - 4 = 41$, $45 - 8 = 37$, $45 - 16 = 29$, $45 - 32 = 13$ line 96 source
Source documentation
$45$ satisfies the Erdős 1142 property: $45 - 2 = 43$, $45 - 4 = 41$, $45 - 8 = 37$, $45 - 16 = 29$, $45 - 32 = 13$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_45 : Erdos1142Prop 45 := by prove_erdos_1142_prop 5
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_75 $75$ satisfies the Erdős 1142 property: $75 - 2 = 73$, $75 - 4 = 71$, $75 - 8 = 67$, $75 - 16 = 59$, $75 - 32 = 43$, $75 - 64 = 11$ line 101 source
Source documentation
$75$ satisfies the Erdős 1142 property: $75 - 2 = 73$, $75 - 4 = 71$, $75 - 8 = 67$, $75 - 16 = 59$, $75 - 32 = 43$, $75 - 64 = 11$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_75 : Erdos1142Prop 75 := by prove_erdos_1142_prop 6
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_105 $105$ satisfies the Erdős 1142 property: the largest known example line 107 source
Source documentation
$105$ satisfies the Erdős 1142 property: the largest known example. $105 - 2 = 103$, $105 - 4 = 101$, $105 - 8 = 97$, $105 - 16 = 89$, $105 - 32 = 73$, $105 - 64 = 41$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: And.intro, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, Not, LE.le, absurd, Nat.succ, False, Nat.pow_le_pow_right, Eq.mp, dite, of_eq_true, eq_true_of_decide, Eq.refl, Bool, Bool.true, Eq.symm and 8 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_105 : Erdos1142Prop 105 := by prove_erdos_1142_prop 6
…
```
Mentions: Erdos1142.Erdos1142Prop
theorem Erdos1142.erdos_1142.test_not_106 $106$ does not satisfy the Erdős 1142 property ($106 - 2 = 104 = 8 \times 13$) line 111 source
Source documentation
$106$ does not satisfy the Erdős 1142 property ($106 - 2 = 104 = 8 \times 13$).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Erdos1142.Erdos1142Prop, OfNat.ofNat, Nat
Proof uses: False, LT.lt, HPow.hPow, Nat.Prime, HSub.hSub, Decidable.byContradiction, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_1142.test_not_106 : ¬ Erdos1142Prop 106 := by
…
```
Mentions: Erdos1142.Erdos1142Prop