Erdős Problem #669

The question

erdos_669.parts.i. 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\ge 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.

erdos_669.parts.ii. 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\ge 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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«669» (2 statements).

theorem erdos_669.parts.i :
    ∀ k : ℕ, 3 ≤ k → ∀ x : ℝ,
      erdos_669.parts.i.answer k = some x ↔
        Tendsto (fun n : ℕ => (maxLinesAtLeast k n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 x)

theorem erdos_669.parts.ii :
    ∀ k : ℕ, 3 ≤ k → ∀ x : ℝ,
      erdos_669.parts.ii.answer k = some x ↔
        Tendsto (fun n : ℕ => (maxLinesExactly k n : ℝ) / (n : ℝ) ^ 2) atTop (𝓝 x)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/669. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/669
• [BGS74] Burr, Stefan A. and Grünbaum, Branko and Sloane, N. J. A., The orchard problem. Geometriae Dedicata (1974), 397-424.
• [Er97f] Erdős, Paul, Some unsolved problems. Combinatorics, geometry and probability (Cambridge, 1993) (1997), 1-10.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.