Erdős Problem a Daythe open tracker
The board / geometry / #669

Erdős Problem #669
orchard problems

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 set of lines in \(\mathbb{R}^2\) containing at least \(k\) points of \(S\). It is the analogue of `EuclideanGeometry.linesWithPointsFor`, which asks for exactly \(k\) points. Only lines spanned by two distinct points of \(S\) are counted, so the definition is meant for \(k \geq 2\).

The set of numbers of distinct lines through at least \(k\) points, taken over all sets of \(n\) points in \(\mathbb{R}^2\).

The set of numbers of distinct lines through exactly \(k\) points, taken over all sets of \(n\) points in \(\mathbb{R}^2\).

Let \(F_k(n)\) be minimal such that for any \(n\) points in \(\mathbb{R}^2\) there exist at most \(F_k(n)\) many distinct lines passing through at least \(k\) of the points, and \(f_k(n)\) similarly but with lines passing through exactly \(k\) points. Estimate \(f_k(n)\) and \(F_k(n)\) - in particular, determine \(\lim F_k(n)/n^2\) and \(\lim f_k(n)/n^2\). This part asks for \(\lim F_k(n)/n^2\) for \(k \geq 3\) (the case \(k = 2\) is trivial). The original question [Er97f, Problem 16] asks for the limits "if they exist", so the answer allows nonexistence: the answer at \(k\) is `some x` if the limit exists and equals \(x\), and `none` otherwise.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 7 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/669.
Prizenone
Topicsgeometry
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA003035, A006065, A008997
Original pageerdosproblems.com/669

Attempts

submit one →
WORKING REPORT BY THIS SITE · JUL 31, 2026

Read our working report →

proved a strict Melchior/Bojanowski upper-bound improvement, exact grid formulas with a checker, and uniform lower bounds; the constants and limit existence for k>=4 remain open.

PARTIAL
← #668the board#670 →