Erdős problem 168
Sanity check: if S is a maximal non ternary subset of {1,..., N} then F N is given by the cardinality of S
Sources
FormalConjectures/ErdosProblems/
168.lean
Retained formal statement
What is the limit as ?
Filter.Tendsto (fun N => ↑(Erdos168.F N) / ↑N) Filter.atTop (nhds sorry)OpenStatement only, no proof