FormalConjectures.ErdosProblems.«1142»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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.

open Nat Setnamespace Erdos1142

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.

def Erdos1142Prop (n : ℕ) : Prop :=
  2 < n ∧ ∀ k, 0 < k → 2 ^ k < n → (n - 2 ^ k).Prime

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

@[category research open, AMS 11]
theorem erdos_1142 :
    answer(sorry) ↔ Infinite { n | Erdos1142Prop n } := by⊢ True ↔ Infinite ↑{n | Erdos1142Prop n}
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 11]
theorem erdos_1142.variants.mientka_weitzenkamp :
    { n : ℕ | n ≤ 2 ^ 44 ∧ Erdos1142Prop n } = {4, 7, 15, 21, 45, 75, 105} := by⊢ {n | n ≤ 2 ^ 44 ∧ Erdos1142Prop n} = {4, 7, 15, 21, 45, 75, 105}
  sorryAll goals completed! 🐙

Helper tactic for proving Erdos1142Prop for small concrete values.

local macro "prove_erdos_1142_prop" bound:num : tactic =>
  `(tactic| (
    refine ⟨by omega, fun k hk hlt => ?_⟩
    have : k ≤ $bound := by
      by_contra! h
      exact absurd (Nat.pow_le_pow_right (by omega : 1 ≤ 2) h) (by omega)
    interval_cases k <;> simp_all (config := { decide := true })))

$4$ satisfies the Erdős 1142 property: $4 - 2 = 2$ is prime.

@[category test, AMS 11]
theorem erdos_1142.test_4 : Erdos1142Prop 4 := by⊢ Erdos1142Prop 4 prove_erdos_1142_prop 1All goals completed! 🐙

$7$ satisfies the Erdős 1142 property: $7 - 2 = 5$ and $7 - 4 = 3$ are prime.

@[category test, AMS 11]
theorem erdos_1142.test_7 : Erdos1142Prop 7 := by⊢ Erdos1142Prop 7 prove_erdos_1142_prop 2All goals completed! 🐙

$15$ satisfies the Erdős 1142 property: $15 - 2 = 13$, $15 - 4 = 11$, $15 - 8 = 7$.

@[category test, AMS 11]
theorem erdos_1142.test_15 : Erdos1142Prop 15 := by⊢ Erdos1142Prop 15 prove_erdos_1142_prop 3All goals completed! 🐙

$21$ satisfies the Erdős 1142 property: $21 - 2 = 19$, $21 - 4 = 17$, $21 - 8 = 13$, $21 - 16 = 5$.

@[category test, AMS 11]
theorem erdos_1142.test_21 : Erdos1142Prop 21 := by⊢ Erdos1142Prop 21 prove_erdos_1142_prop 4All goals completed! 🐙

$45$ satisfies the Erdős 1142 property: $45 - 2 = 43$, $45 - 4 = 41$, $45 - 8 = 37$, $45 - 16 = 29$, $45 - 32 = 13$.

@[category test, AMS 11]
theorem erdos_1142.test_45 : Erdos1142Prop 45 := by⊢ Erdos1142Prop 45 prove_erdos_1142_prop 5All goals completed! 🐙

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

@[category test, AMS 11]
theorem erdos_1142.test_75 : Erdos1142Prop 75 := by⊢ Erdos1142Prop 75 prove_erdos_1142_prop 6All goals completed! 🐙

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

@[category test, AMS 11]
theorem erdos_1142.test_105 : Erdos1142Prop 105 := by⊢ Erdos1142Prop 105 prove_erdos_1142_prop 6All goals completed! 🐙

$106$ does not satisfy the Erdős 1142 property ($106 - 2 = 104 = 8 \times 13$).


@[category test, AMS 11]
theorem erdos_1142.test_not_106 : ¬ Erdos1142Prop 106 := by⊢ ¬Erdos1142Prop 106
  intro ⟨_, h⟩left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ False
  have := h 1 (byleft✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ 0 < 1left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)this:Nat.Prime (106 - 2 ^ 1)⊢ False omegaAll goals completed! 🐙left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)this:Nat.Prime (106 - 2 ^ 1)⊢ False) (byleft✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ 2 ^ 1 < 106left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)this:Nat.Prime (106 - 2 ^ 1)⊢ False omegaAll goals completed! 🐙left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)this:Nat.Prime (106 - 2 ^ 1)⊢ False)left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)this:Nat.Prime (106 - 2 ^ 1)⊢ False
  revert thisleft✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ Nat.Prime (106 - 2 ^ 1) → False; decideAll goals completed! 🐙

end Erdos1142