Documentation

FormalConjectures.ErdosProblems.«273»

Erdős Problem 273 #

Reference: erdosproblems.com/273

theorem erdos_273 :
(∃ (c : StrictCoveringSystem ), ∀ (i : c.ι), ∃ (p : ), Nat.Prime p 5 p c.moduli i = Ideal.span {↑(p - 1)}) sorry

Is there a covering system all of whose moduli are of the form $p-1$ for some primes $p\geq 5$?

theorem erdos_273.variants.three :
(∃ (c : StrictCoveringSystem ), ∀ (i : c.ι), ∃ (p : ), Nat.Prime p 3 p c.moduli i = Ideal.span {p - 1}) True

Is there a covering system all of whose moduli are of the form $p-1$ for some primes $p\geq 3$?