Erdős problem 798

Let $t(n)$ be the minimum number of points in $\{1,\ldots,n\}^2$ such that the $\binom{t}{2}$ lines determined by these points cover all points in $\{1,\ldots,n\}^2$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

798.lean

Retained formal statement2 of 3

A problem of Erdős and Purdy, who proved $t(n) \gg n^{2/3}$ .

FormalConjectures/ErdosProblems/798.leanErdos798.erdos_798.variants.lower_bound1 lineExact file

1(fun n => ↑n ^ (2 / 3)) =O[Filter.atTop] fun n => ↑(Erdos798.t n)

SolvedStatement only, no proof