Erdős Problem #798
PROVED LEANdatabase updated 2026-05-08
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The grid \(\{1,\ldots,n\}^2\), viewed as a set of points of the plane.
`S` is a set of points of \(\{1,\ldots,n\}^2\) such that the lines determined by the pairs of distinct points of `S` cover all points of \(\{1,\ldots,n\}^2\).
The minimum number of points in \(\{1,\ldots,n\}^2\) such that the lines determined by these points cover all points in \(\{1,\ldots,n\}^2\).
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\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/798.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanyes
OEISA116446
Original pageerdosproblems.com/798
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.