Skip to content

Erdős problem 168

Start work

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 statement1 of 9

What is the limit F(N)/NF(N)/N as N→∞N \to \infty?

FormalConjectures/ErdosProblems/168.leanErdos168.erdos_168.parts.i1 lineExact file
Filter.Tendsto (fun N => ↑(Erdos168.F N) / ↑N) Filter.atTop (nhds sorry)
OpenStatement only, no proof