heilbronn_triangle_problem
Disprovedcombinatorial-geometrycombinatoricsconjecturediscrete-mathematicsextremal-combinatorics
Heilbronn triangle problem: Among any n points in a unit square, there are 3 forming a triangle of area ≤ C/n². Best known lower bound: Ω(log n / n²). Best upper bound: O(1/n^{8/5}) (Cohen–Settypally 2023). Exact exponent in n^{-2} unknown.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem heilbronn_triangle_problem :
∀ eps : ℝ, 0 < eps →
∃ C : ℝ, 0 < C ∧
∀ (n : ℕ) (pts : Fin n → ℝ × ℝ),
(∀ i : Fin n, ‖pts i‖ ≤ 1) →
∃ i j k : Fin n, i ≠ j ∧ j ≠ k ∧ i ≠ k ∧
|(pts i).1 * ((pts j).2 - (pts k).2) +
(pts j).1 * ((pts k).2 - (pts i).2) +
(pts k).1 * ((pts i).2 - (pts j).2)| / 2 ≤ C / n ^ (2 - eps) := by
sorrySource