OAI.Problem355.heilbronn_power_lower_bound

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that the Heilbronn exponent δ is positive and that there exist a sequence of natural numbers n(j) tending to infinity and finite sets P(j) of points in the plane, such that for every j, n(j) ≥ 3, P(j) has exactly n(j) points, all lying in the closed unit square [0,1]×[0,1], and every triple of three distinct points of P(j) spans a triangle of area at least n(j)^(−2+δ). Triangle area is |(q₁−p₁)(r₂−p₂)−(q₂−p₂)(r₁−p₁)|/2. Here δ = 1/(100000·K) with K = T²+1, where T = C(M,3), M = C(4·41−1, 41) = C(163,41), so δ is an explicit but extremely small positive rational constant. Thus the statement asserts an infinite family of point sets whose smallest triangle area is at least a power n^(−2+δ).

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/HeilbronnTriangle.lean; bytes 1460..1824
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_HeilbronnTriangle

namespace OAI

noncomputable section

namespace Problem355

attribute [local irreducible] Problem355.heilbronnT
  Problem355.heilbronnM

Formal statement

theorem heilbronn_power_lower_bound :
    0 < heilbronnExponent ∧ ∃ n : ℕ → ℕ, ∃ P : ℕ → Finset Point,
      Filter.Tendsto n Filter.atTop Filter.atTop ∧ ∀ j : ℕ,
        3 ≤ n j ∧ (P j).card = n j ∧ pointsInUnitSquare (P j) ∧
        triangleAreasAtLeast (P j)
          (Real.rpow (n j : ℝ) (-2 + heilbronnExponent)) := by
  sorry

end Problem355
end
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/HeilbronnTriangle.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph