Erdős problem 342

$a(3) = 4$ : among sums $> 3$ with a unique representation from $\{1,2,3\}$ , the smallest is $4 = 1 + 3$ . The candidate $5 = 2 + 3$ is ruled out by minimality since $4$ has a unique representation.

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

342.lean

Retained formal statement5 of 7

$a(1) = 2$ by definition.

FormalConjectures/ErdosProblems/342.leanErdos342.erdos_342.test.a11 lineExact file

1∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → a 1 = 2

TestStatement only, no proof