FormalConjectures.ErdosProblems.«1059»

/-
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 1059

Reference: erdosproblems.com/1059


namespace Erdos1059


def IsFactorial (d : ℕ) : Prop :=
  d ∈ Set.range Nat.factorial


def factorialsLessThanN (n : ℕ) : Set ℕ :=
  { d | d < n ∧ IsFactorial d }


def AllFactorialSubtractionsComposite (n : ℕ) : Prop :=
  ∀d ∈ factorialsLessThanN n, (n - d).Composite

Are there infinitely many primes $p$ such that $p - k!$ is composite for each $k$ such that $1 ≤ k! < p$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_1059 :
    answer(sorry) ↔ Set.Infinite {p | p.Prime ∧ AllFactorialSubtractionsComposite p} := by⊢ True ↔ {p | Nat.Prime p ∧ AllFactorialSubtractionsComposite p}.Infinite
  sorryAll goals completed! 🐙


abbrev DecidableIsFactorial (d : ℕ) : Prop :=
  ((Finset.Icc 0 d).filter (λ k => Nat.factorial k = d)).Nonempty


def decidableFactorialsLessThanN (n : ℕ) : Finset ℕ :=
  (Finset.range n).filter DecidableIsFactorial


def DecidableAllFactorialSubtractionsComposite (n : ℕ) : Prop :=
  ∀ d ∈ decidableFactorialsLessThanN n, (n - d).Composite


@[category test, AMS 11]
lemma isFactorial_equivalent (d : ℕ) :
  IsFactorial d ↔ DecidableIsFactorial d := byd:ℕ⊢ IsFactorial d ↔ DecidableIsFactorial d
  unfold IsFactorial DecidableIsFactoriald:ℕ⊢ d ∈ Set.range Nat.factorial ↔ {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty
  simpd:ℕ⊢ (∃ y, y.factorial = d) ↔ {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty
  constructormpd:ℕ⊢ (∃ y, y.factorial = d) → {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonemptymprd:ℕ⊢ {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty → ∃ y, y.factorial = d
  ·mpd:ℕ⊢ (∃ y, y.factorial = d) → {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty rintro ⟨k, hk⟩mpd:ℕk:ℕhk:k.factorial = d⊢ {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty
    use khd:ℕk:ℕhk:k.factorial = d⊢ k ∈ {k ∈ Finset.Icc 0 d | k.factorial = d}
    rw [Finset.mem_filter]hd:ℕk:ℕhk:k.factorial = d⊢ k ∈ Finset.Icc 0 d ∧ k.factorial = d
    constructorh.leftd:ℕk:ℕhk:k.factorial = d⊢ k ∈ Finset.Icc 0 dh.rightd:ℕk:ℕhk:k.factorial = d⊢ k.factorial = d
    ·h.leftd:ℕk:ℕhk:k.factorial = d⊢ k ∈ Finset.Icc 0 d have hk : k <= d := byd:ℕ⊢ IsFactorial d ↔ DecidableIsFactorial d
        rw [← hk]d:ℕk:ℕhk:k.factorial = d⊢ k ≤ k.factorial
        apply Nat.self_le_factorialAll goals completed! 🐙
      rw [Finset.mem_Icc]h.leftd:ℕk:ℕhk✝:k.factorial = dhk:k ≤ d := Eq.mpr (id (congrArg (fun _a => k ≤ _a) (Eq.symm hk✝))) (Nat.self_le_factorial k)⊢ 0 ≤ k ∧ k ≤ d
      exact ⟨Nat.zero_le k, hk⟩All goals completed! 🐙
    ·h.rightd:ℕk:ℕhk:k.factorial = d⊢ k.factorial = d exact hkAll goals completed! 🐙
  ·mprd:ℕ⊢ {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty → ∃ y, y.factorial = d rintro ⟨k, hk⟩mprd:ℕk:ℕhk:k ∈ {k ∈ Finset.Icc 0 d | k.factorial = d}⊢ ∃ y, y.factorial = d
    use khd:ℕk:ℕhk:k ∈ {k ∈ Finset.Icc 0 d | k.factorial = d}⊢ k.factorial = d
    rw [Finset.mem_filter] at hkhd:ℕk:ℕhk:k ∈ Finset.Icc 0 d ∧ k.factorial = d⊢ k.factorial = d
    exact hk.2All goals completed! 🐙


@[category test, AMS 11]
lemma factorialsLessThanN_equivalent (n : ℕ) :
  factorialsLessThanN n = ↑(decidableFactorialsLessThanN n) := byn:ℕ⊢ factorialsLessThanN n = ↑(decidableFactorialsLessThanN n)
  ext dhn:ℕd:ℕ⊢ d ∈ factorialsLessThanN n ↔ d ∈ ↑(decidableFactorialsLessThanN n)
  unfold factorialsLessThanN decidableFactorialsLessThanNhn:ℕd:ℕ⊢ d ∈ {d | d < n ∧ IsFactorial d} ↔ d ∈ ↑(Finset.filter DecidableIsFactorial (Finset.range n))
  simphn:ℕd:ℕ⊢ d < n → (IsFactorial d ↔ DecidableIsFactorial d)
  exact λ _ => isFactorial_equivalent dAll goals completed! 🐙


@[category test, AMS 11]
lemma allFactorialSubtractionsComposite_equivalent (d : ℕ) :
    DecidableAllFactorialSubtractionsComposite d ↔ AllFactorialSubtractionsComposite d := byd:ℕ⊢ DecidableAllFactorialSubtractionsComposite d ↔ AllFactorialSubtractionsComposite d
  unfold AllFactorialSubtractionsComposite DecidableAllFactorialSubtractionsComposited:ℕ⊢ (∀ d_1 ∈ decidableFactorialsLessThanN d, (d - d_1).Composite) ↔ ∀ d_1 ∈ factorialsLessThanN d, (d - d_1).Composite
  rw [factorialsLessThanN_equivalent d]d:ℕ⊢ (∀ d_1 ∈ decidableFactorialsLessThanN d, (d - d_1).Composite) ↔
  ∀ d_1 ∈ ↑(decidableFactorialsLessThanN d), (d - d_1).Composite
  simpAll goals completed! 🐙


@[category test, AMS 11]
theorem allFactorialSubtractionsComposite_101 : AllFactorialSubtractionsComposite 101 := by⊢ AllFactorialSubtractionsComposite 101
  have h : DecidableAllFactorialSubtractionsComposite 101 := by⊢ AllFactorialSubtractionsComposite 101
    norm_num [DecidableAllFactorialSubtractionsComposite, decidableFactorialsLessThanN]⊢ ∀ d < 101, DecidableIsFactorial d → (101 - d).Composite
    decide +kernelAll goals completed! 🐙
  exact (allFactorialSubtractionsComposite_equivalent 101).mp hAll goals completed! 🐙


@[category test, AMS 11]
theorem allFactorialSubtractionsComposite_211 : AllFactorialSubtractionsComposite 211 := by⊢ AllFactorialSubtractionsComposite 211
  have h : DecidableAllFactorialSubtractionsComposite 211 := by⊢ AllFactorialSubtractionsComposite 211
    norm_num [DecidableAllFactorialSubtractionsComposite, decidableFactorialsLessThanN]⊢ ∀ d < 211, DecidableIsFactorial d → (211 - d).Composite
    decide +kernelAll goals completed! 🐙
  exact (allFactorialSubtractionsComposite_equivalent 211).mp hAll goals completed! 🐙


@[category test, AMS 11]
theorem notAllFactorialSubtractionsComposite_89 : ¬(AllFactorialSubtractionsComposite 89) := by⊢ ¬AllFactorialSubtractionsComposite 89
  have h : ¬(DecidableAllFactorialSubtractionsComposite 89) := by⊢ ¬AllFactorialSubtractionsComposite 89
    unfold DecidableAllFactorialSubtractionsComposite decidableFactorialsLessThanN⊢ ¬∀ d ∈ Finset.filter DecidableIsFactorial (Finset.range 89), (89 - d).Composite
    intro hh:∀ d ∈ Finset.filter DecidableIsFactorial (Finset.range 89), (89 - d).Composite⊢ False
    specialize h 6h:6 ∈ Finset.filter DecidableIsFactorial (Finset.range 89) → (89 - 6).Composite⊢ False
    have : Nat.Prime (89 - 6) := by⊢ ¬AllFactorialSubtractionsComposite 89 norm_numAll goals completed! 🐙
    contradictionAll goals completed! 🐙
  simp [allFactorialSubtractionsComposite_equivalent] at hh:¬AllFactorialSubtractionsComposite 89⊢ ¬AllFactorialSubtractionsComposite 89
  exact hAll goals completed! 🐙


@[category test, AMS 11]
theorem testFactorialsLessThanN : factorialsLessThanN 100 = {1, 2, 6, 24} := by⊢ factorialsLessThanN 100 = {1, 2, 6, 24}
  have h : decidableFactorialsLessThanN 100 = {1, 2, 6, 24} := by⊢ factorialsLessThanN 100 = {1, 2, 6, 24}
    norm_num [decidableFactorialsLessThanN]⊢ Finset.filter DecidableIsFactorial (Finset.range 100) = {1, 2, 6, 24}
    decide +kernelAll goals completed! 🐙
  rw [factorialsLessThanN_equivalent]h:decidableFactorialsLessThanN 100 = {1, 2, 6, 24} := id testFactorialsLessThanN._proof_1⊢ ↑(decidableFactorialsLessThanN 100) = {1, 2, 6, 24}
  simp [h]All goals completed! 🐙


end Erdos1059