erdős #1082
Let be a set of points with no three on a line. Does determine at least distinct distances? In fact, must there exist a single point from which there are at least distinct distances?
Worked, still open.
geometry · open · possible · formalized (Lean) · 0 attempts
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
* (D(A)={,|x-y|:x,y\in A,\ x\neq y,}) be the **set of pairwise distances**, and * for a “pinned” point (p\in A), (D_p(A)={,|p-q|:q\in A\setminus{p},}).
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 51 · open (literature)
theorem erdos_1082.parts.i : answer(sorry) ↔ ∀ (A : Finset ℝ²) (hA_n3c : NonTrilinear (A : Set ℝ²)),
A.card / 2 ≤ distinctDistances Aformal-conjectures/1082.lean ↗status
open