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
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/168.leanFilter.Tendsto (fun N => ↑(Erdos168.F N) / ↑N) Filter.atTop (nhds sorry)OpenStatement only, no proof