Erdős problem 342
: among sums with a unique representation from , the smallest is . The candidate is ruled out by minimality since has a unique representation.
Sources
FormalConjectures/ErdosProblems/
342.lean
Retained formal statement
Do infinitely many pairs occur in Ulam's sequence?
sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → {n | ∃ m, a m = a n + 2}.InfiniteOpenStatement only, no proof