1. FormalConjectures
  2. ErdosProblems
  3. «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 Erdos1059def IsFactorial (d : ℕ) : Prop := d ∈ Set.range Nat.factorialdef 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 erdos_1059 : answer(sorry) ↔ Set.Infinite {p | p.Prime ∧ AllFactorialSubtractionsComposite p} := ⊢ True ↔ {p | Nat.Prime p ∧ AllFactorialSubtractionsComposite p}.Infinite All goals completed! 🐙abbrev DecidableIsFactorial (d : ℕ) : Prop := ((Finset.Icc 0 d).filter (λ k => Nat.factorial k = d)).Nonemptydef decidableFactorialsLessThanN (n : ℕ) : Finset ℕ := (Finset.range n).filter DecidableIsFactorialdef DecidableAllFactorialSubtractionsComposite (n : ℕ) : Prop := ∀ d ∈ decidableFactorialsLessThanN n, (n - d).Composited:ℕk:ℕhk:k ∈ Finset.Icc 0 d ∧ k.factorial = d⊢ k.factorial = d All goals completed! 🐙@[category test, AMS 11] lemma factorialsLessThanN_equivalent (n : ℕ) : factorialsLessThanN n = ↑(decidableFactorialsLessThanN n) := n:ℕ⊢ factorialsLessThanN n = ↑(decidableFactorialsLessThanN n) n:ℕd:ℕ⊢ d ∈ factorialsLessThanN n ↔ d ∈ ↑(decidableFactorialsLessThanN n) n:ℕd:ℕ⊢ d ∈ {d | d < n ∧ IsFactorial d} ↔ d ∈ ↑(Finset.filter DecidableIsFactorial (Finset.range n)) n:ℕd:ℕ⊢ d < n → (IsFactorial d ↔ DecidableIsFactorial d) All goals completed! 🐙d:ℕ⊢ (∀ d_1 ∈ decidableFactorialsLessThanN d, (d - d_1).Composite) ↔ ∀ d_1 ∈ ↑(decidableFactorialsLessThanN d), (d - d_1).Composite All goals completed! 🐙h:DecidableAllFactorialSubtractionsComposite 101⊢ AllFactorialSubtractionsComposite 101 All goals completed! 🐙h:DecidableAllFactorialSubtractionsComposite 211⊢ AllFactorialSubtractionsComposite 211 All goals completed! 🐙h:¬DecidableAllFactorialSubtractionsComposite 89⊢ ¬AllFactorialSubtractionsComposite 89 h:¬AllFactorialSubtractionsComposite 89⊢ ¬AllFactorialSubtractionsComposite 89 All goals completed! 🐙h:decidableFactorialsLessThanN 100 = {1, 2, 6, 24}⊢ ↑(decidableFactorialsLessThanN 100) = {1, 2, 6, 24} All goals completed! 🐙end Erdos1059