Erdős problem 494
Selfridge and Straus [SeSt58] also showed that the conjecture is true when 1) and or 2) and . More generally, they proved that is determined by (and ) if is divisible by a prime greater than .
Sources
FormalConjectures/ErdosProblems/
494.lean
Retained formal statement
Selfridge and Straus [SeSt58] proved that is determined by if is divisible by a prime greater than .
∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k cardSolvedStatement only, no proof