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
Part (iii), is the density of the sequence 0?
sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → (Set.range a).upperDensity = 0OpenStatement only, no proof