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
Erdos168.F 2 = 2APIStatement only, no proof