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
: the only pair with is , giving .
∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → a 2 = 3TestStatement only, no proof