Erdős Problem #102
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The number of points of `P` that lie on `L`.
The number of lines that contain more than three points of `P`.
`P` has \(n\) points and at least \(c n^2\) lines that each contain more than three points of `P`.
Let \(c > 0\) and let \(h_c(n)\) be such that for any \(n\) points in \(\mathbb{R}^2\) with at least \(cn^2\) lines that each contain more than three of the points, some line contains \(h_c(n)\) of the points. Is it true that, for fixed \(c > 0\), \(h_c(n) \to \infty\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/102.Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/102
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.