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
by definition.
∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → a 1 = 2TestStatement only, no proof