Erdős Problem 507

References:

• erdosproblems.com/507
• [CPZ23] Cohen, Alex, Cosmin Pohoata, and Dmitrii Zakharov. "A new upper bound for the Heilbronn triangle problem." arXiv preprint arXiv:2305.18253 (2023).
• [CPZ24] Cohen, Alex, Cosmin Pohoata, and Dmitrii Zakharov. "Lower bounds for incidences." Inventiones mathematicae (2025): 1-74.
• [KPS82] Komlós, János, János Pintz, and Endre Szemerédi. "A lower bound for Heilbronn's problem." Journal of the London Mathematical Society 2.1 (1982): 13-24.
• [KPS81] Komlós, János, János Pintz, and Endre Szemerédi. "On Heilbronn's triangle problem." Journal of the London Mathematical Society 2.3 (1981): 385-396.

noncomputable def Erdos507.minTriangleArea (S : Finset (EuclideanSpace ℝ (Fin 2))) : ℝ

The minimum area of a triangle determined by three distinct points in a set S.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Erdos507.α (n : ℕ) : ℝ

$\alpha(n)$ is the supremum of minTriangleArea S over all sets S of $n$ points in the unit disk.

Equations

• Erdos507.α n = sSup (Erdos507.minTriangleArea '' {S : Finset (EuclideanSpace ℝ (Fin 2)) | S.card = n ∧ ↑S ⊆ Metric.closedBall 0 1 ∧ ¬Collinear ℝ ↑S})

noncomputable def Erdos507.lowerBest (n : ℕ) : ℝ

Current best lower bound [KPS82].

Equations

• Erdos507.lowerBest n = Real.log ↑n / ↑n ^ 2

noncomputable def Erdos507.upperBarrier (n : ℕ) : ℝ

The "Barrier" function: n^(-7/6) used for the best upper bound [CPZ24].

Equations

• Erdos507.upperBarrier n = 1 / ↑n ^ (7 / 6)

theorem Erdos507.erdos_507.equivalent : Asymptotics.IsEquivalent Filter.atTop α sorry

Let $\alpha(n)$ be such that every set of $n$ points in the unit disk contains three points which determine a triangle of area at most $\alpha(n)$. Estimate $\alpha(n)$.

theorem Erdos507.erdos_507.lower : have ans := sorry; lowerBest =o[Filter.atTop] ans ∧ ans =O[Filter.atTop] α

Estimate a lower bound for$\alpha(n)$.

theorem Erdos507.erdos_507.upper : have ans := sorry; α =O[Filter.atTop] ans ∧ ans =o[Filter.atTop] upperBarrier

Estimate an upper bound for$\alpha(n)$.

theorem Erdos507.erdos_507.variants.upper_trivial : α =O[Filter.atTop] fun (n : ℕ) => 1 / ↑n

It is trivial that $\alpha(n) \ll 1/n$.

theorem Erdos507.erdos_507.variants.lower_erdos : (fun (n : ℕ) => 1 / ↑n ^ 2) =O[Filter.atTop] α

Erdős observed that $\alpha(n) \gg 1/n^2$.

theorem Erdos507.erdos_507.variants.lower_kps82 : lowerBest =O[Filter.atTop] α

Current best lower bound [KPS82].

theorem Erdos507.erdos_507.variants.upper_cpz24 : ∃ (o : ℕ → ℝ), Filter.Tendsto o Filter.atTop (nhds 0) ∧ α =O[Filter.atTop] fun (n : ℕ) => upperBarrier n * ↑n ^ o n

Current best upper bound [CPZ24]: $\alpha(n) \ll n^{-7/6 + o(1)}$.