Erdős problem 798 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

798.lean

Retained formal statement1 of 3

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$ .

Estimate $t(n)$ . In particular, is it true that $t(n)=o(n)$ ?

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

Resolved by Alon [Al91] who proved $t(n) \ll n^{2/3}\log n$ .

FormalConjectures/ErdosProblems/798.leanErdos798.erdos_7981 lineExact file

1True ↔ (fun n => ↑(Erdos798.t n)) =o[Filter.atTop] fun n => ↑n

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science