If $n$ points in $R^{2}$ form a convex polygon then there are $O (n)$ many pairs which are distance $1$ apart.

Worked, still open.

geometry · open · possible · formalized (Lean) · 0 attempts

machinery: geometric,unit-distance-convex,incidence-geometry,extremal-combinatorics,convex-polygon

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let $f(n)$ be the **maximum** possible number of pairs $\\{p,q\\}$ with (|p-q|=1), where (p_1,\dots,p_n) are the vertices of a convex $n$-gon.

llm-hunter · codex 5.2 extra high, gpt 5.2, gpt pro 5.2 · unverified

3 LLM attack(s) recorded (codex 5.2 extra high, gpt 5.2, gpt pro 5.2); unverified.

AMS 52 · test (literature)

theorem convexUnitDistanceCounts_bddAbove (n : ℕ) : BddAbove <| convexUnitDistanceCounts n

open