Erdős Problem 1059

Reference: erdosproblems.com/1059

def Erdos1059.IsFactorial (d : ℕ) : Prop

Equations

• Erdos1059.IsFactorial d = (d ∈ Set.range Nat.factorial)

def Erdos1059.factorialsLessThanN (n : ℕ) : Set ℕ

Equations

• Erdos1059.factorialsLessThanN n = {d : ℕ | d < n ∧ Erdos1059.IsFactorial d}

def Erdos1059.AllFactorialSubtractionsComposite (n : ℕ) : Prop

Equations

• Erdos1059.AllFactorialSubtractionsComposite n = ∀ d ∈ Erdos1059.factorialsLessThanN n, (n - d).Composite

theorem Erdos1059.erdos_1059 : {p : ℕ | Nat.Prime p ∧ AllFactorialSubtractionsComposite p}.Infinite ↔ sorry

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

@[reducible, inline]

abbrev Erdos1059.DecidableIsFactorial (d : ℕ) : Prop

Equations

• Erdos1059.DecidableIsFactorial d = {k ∈ Finset.Icc 0 d | k.factorial = d}.Nonempty

def Erdos1059.decidableFactorialsLessThanN (n : ℕ) : Finset ℕ

Equations

• Erdos1059.decidableFactorialsLessThanN n = Finset.filter Erdos1059.DecidableIsFactorial (Finset.range n)

def Erdos1059.DecidableAllFactorialSubtractionsComposite (n : ℕ) : Prop

Equations

• Erdos1059.DecidableAllFactorialSubtractionsComposite n = ∀ d ∈ Erdos1059.decidableFactorialsLessThanN n, (n - d).Composite

theorem Erdos1059.isFactorial_equivalent (d : ℕ) : IsFactorial d ↔ DecidableIsFactorial d

theorem Erdos1059.factorialsLessThanN_equivalent (n : ℕ) : factorialsLessThanN n = ↑(decidableFactorialsLessThanN n)

theorem Erdos1059.allFactorialSubtractionsComposite_equivalent (d : ℕ) : DecidableAllFactorialSubtractionsComposite d ↔ AllFactorialSubtractionsComposite d

theorem Erdos1059.allFactorialSubtractionsComposite_101 : AllFactorialSubtractionsComposite 101

theorem Erdos1059.allFactorialSubtractionsComposite_211 : AllFactorialSubtractionsComposite 211

theorem Erdos1059.notAllFactorialSubtractionsComposite_89 : ¬AllFactorialSubtractionsComposite 89

theorem Erdos1059.testFactorialsLessThanN : factorialsLessThanN 100 = {1, 2, 6, 24}