Erdős problem 770
For odd n, the values of h n form an unbounded set. This is described as 'easy to see' in [Er74b].
Sources
FormalConjectures/ErdosProblems/
770.lean
Retained formal statement
For odd n, the values of h n form an unbounded set. This is described as 'easy to see' in [Er74b].
Set.Unbounded (fun x1 x2 => x1 ≤ x2) (ENat.toNat '' (Erdos770.h '' Odd))TextbookStatement only, no proof