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] gave counterexamples to the conjecture when and .
∀ (card : ℕ), (∃ l, card = 2 ^ l) → ¬Erdos494.Erdos494Unique 2 cardSolvedStatement only, no proof