erdős #99
Let be a set of points with minimum distance equal to 1, chosen to minimise the diameter of . If is sufficiently large then must there be three points in which form an equilateral triangle of size 1?
Worked, still open.
geometry · open · prize $100 · formalized (Lean) · 0 attempts
machinery: geometric,discrete-geometry-packing,triangular-lattice-rigidity,diameter-minimization,minimum-distance-set,extremal-configuration,Thue-lattice-optimality
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
It is a famous open question of Erdős (often listed as “Erdős Problem #99”): if you choose $n$ points in the plane with **minimum pairwise distance $1$** and you arrange them to make the **diameter as small as possible**, then for large $n$ **must** you get a **unit equilateral triangle** among the points? Nobody has p…
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 52 · open (literature)
theorem erdos_99 :
answer(sorry) ↔ ∀ᶠ n in Filter.atTop, ∀ A : Finset ℝ²,
A.card = n → HasMinDist1 A →
(IsMinOn (fun B: Finset ℝ² => diam (B : Set ℝ²)) {B : Finset ℝ² | B.card = n ∧ HasMinDist1 B} A) →
∃ᵉ (p ∈ A) (q ∈ A) (r ∈ A), FormsEquilateralTriangle p q rformal-conjectures/99.lean ↗status
open