Skip to content

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

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

168.lean

Retained formal statement4 of 9
FormalConjectures/ErdosProblems/168.leanErdos168.F_01 lineExact file
Erdos168.F 0 = 0
APIStatement only, no proof