FormalConjectures.ErdosProblems.«9»

/-
Copyright 2025 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 9

Reference: erdosproblems.com/9


namespace Erdos9

The set of odd numbers that cannot be expressed as a prime plus two powers of 2.

def Erdos9A : Set ℕ := { n | Odd n ∧ ¬ ∃ (p k l : ℕ), (Nat.Prime p) ∧ n = p + 2 ^ k + 2 ^ l }



@[category test, AMS 5 11]
theorem erdos9A_contains_one : 1 ∈ Erdos9A := by⊢ 1 ∈ Erdos9A
  constructorleft⊢ Odd 1right⊢ ¬∃ p k l, Nat.Prime p ∧ 1 = p + 2 ^ k + 2 ^ l
  ·left⊢ Odd 1 decideAll goals completed! 🐙
  ·right⊢ ¬∃ p k l, Nat.Prime p ∧ 1 = p + 2 ^ k + 2 ^ l push_negright⊢ ∀ (p k l : ℕ), Nat.Prime p → 1 ≠ p + 2 ^ k + 2 ^ l
    intro p krightp:ℕk:ℕ⊢ ∀ (l : ℕ), Nat.Prime p → 1 ≠ p + 2 ^ k + 2 ^ l lrightp:ℕk:ℕl:ℕ⊢ Nat.Prime p → 1 ≠ p + 2 ^ k + 2 ^ l hprightp:ℕk:ℕl:ℕhp:Nat.Prime p⊢ 1 ≠ p + 2 ^ k + 2 ^ l
    linarith [Nat.Prime.two_le hp, @Nat.one_le_two_pow k, @Nat.one_le_two_pow l]All goals completed! 🐙


@[category test, AMS 5 11]
theorem erdos9A_contains_three : 3 ∈ Erdos9A := by⊢ 3 ∈ Erdos9A
  constructorleft⊢ Odd 3right⊢ ¬∃ p k l, Nat.Prime p ∧ 3 = p + 2 ^ k + 2 ^ l
  ·left⊢ Odd 3 decideAll goals completed! 🐙
  ·right⊢ ¬∃ p k l, Nat.Prime p ∧ 3 = p + 2 ^ k + 2 ^ l push_negright⊢ ∀ (p k l : ℕ), Nat.Prime p → 3 ≠ p + 2 ^ k + 2 ^ l
    intro p krightp:ℕk:ℕ⊢ ∀ (l : ℕ), Nat.Prime p → 3 ≠ p + 2 ^ k + 2 ^ l lrightp:ℕk:ℕl:ℕ⊢ Nat.Prime p → 3 ≠ p + 2 ^ k + 2 ^ l hprightp:ℕk:ℕl:ℕhp:Nat.Prime p⊢ 3 ≠ p + 2 ^ k + 2 ^ l
    linarith [Nat.Prime.two_le hp, @Nat.one_le_two_pow k, @Nat.one_le_two_pow l]All goals completed! 🐙


@[category test, AMS 5 11]
theorem erdos9A_not_contains_five : 5 ∉ Erdos9A := by⊢ 5 ∉ Erdos9A
  unfold Erdos9A⊢ 5 ∉ {n | Odd n ∧ ¬∃ p k l, Nat.Prime p ∧ n = p + 2 ^ k + 2 ^ l}
  simp only [exists_and_left, not_exists, not_and, Set.mem_setOf_eq, not_forall, Decidable.not_not]⊢ Odd 5 → ∃ x, ∃ (_ : Nat.Prime x), ∃ x_1 x_2, 5 = x + 2 ^ x_1 + 2 ^ x_2
  introa✝:Odd 5⊢ ∃ x, ∃ (_ : Nat.Prime x), ∃ x_1 x_2, 5 = x + 2 ^ x_1 + 2 ^ x_2
  use 3, Nat.prime_three, 0, 0ha✝:Odd 5⊢ 5 = 3 + 2 ^ 0 + 2 ^ 0
  simp only [pow_zero, Nat.reduceAdd]All goals completed! 🐙

The set is known to be infinite. In [Er77c] Erdős credits Schinzel with proving that there are infinitely many odd integers not of this form, but gives no reference.

[Er77c] Erdős, P., Problems and results on combinatorial number theory. III..

@[category research solved, AMS 5 11]
theorem declaration uses 'sorry'erdos_9.variants.infinite : Erdos9A.Infinite := by⊢ Erdos9A.Infinite
  sorryAll goals completed! 🐙

Is the upper density of the set of odd numbers that cannot be expressed as a prime plus two powers of 2 positive?

@[category research open, AMS 5 11]
theorem declaration uses 'sorry'erdos_9 : answer(sorry) ↔ 0 < Erdos9A.upperDensity := by⊢ True ↔ 0 < Erdos9A.upperDensity
  sorryAll goals completed! 🐙


end Erdos9