Erdős problem 168 · problems.science

Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S

Sources

Browse retained paths and inspect the exact material available for this Problem.

9 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

168.lean

Retained formal statement3 of 9

The limit $F(N)/N$ as $N \to \infty$ exists. (proved by Graham, Spencer, and Witsenhausen)

FormalConjectures/ErdosProblems/168.leanErdos168.erdos_168.variants.limit_exists1 lineExact file

1∃ x, Filter.Tendsto (fun N => ↑(Erdos168.F N) / ↑N) Filter.atTop (nhds x)

SolvedStatement only, no proof