1. FormalConjectures
  2. ErdosProblems
  3. «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 Set namespace 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 declaration uses 'sorry'erdos_1142 : answer(sorry) ↔ Infinite { n | Erdos1142Prop n } := ⊢ True ↔ Infinite ↑{n | Erdos1142Prop n} All 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 declaration uses 'sorry'erdos_1142.variants.mientka_weitzenkamp : { n : ℕ | n ≤ 2 ^ 44 ∧ Erdos1142Prop n } = {4, 7, 15, 21, 45, 75, 105} := ⊢ {n | n ≤ 2 ^ 44 ∧ Erdos1142Prop n} = {4, 7, 15, 21, 45, 75, 105} All 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; push_neg at 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 := ⊢ Erdos1142Prop 4 All 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 := ⊢ Erdos1142Prop 7 All 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 := ⊢ Erdos1142Prop 15 All 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 := ⊢ Erdos1142Prop 21 All 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 := ⊢ Erdos1142Prop 45 All 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 := ⊢ Erdos1142Prop 75 All 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 := ⊢ Erdos1142Prop 105 All 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 := ⊢ ¬Erdos1142Prop 106 left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ False have := h 1 (left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ 0 < 1 All goals completed! 🐙) (left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ 2 ^ 1 < 106 All goals completed! 🐙) left✝:2 < 106h:∀ (k : ℕ), 0 < k → 2 ^ k < 106 → Nat.Prime (106 - 2 ^ k)⊢ Nat.Prime (106 - 2 ^ 1) → False; All goals completed! 🐙 end Erdos1142