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
Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all when is sufficiently large.
∀ k > 2, ∀ᶠ (card : ℕ) in Filter.atTop, Erdos494.Erdos494Unique k cardSolvedStatement only, no proof