erdős #97
Does every convex polygon have a vertex with no other vertices equidistant from it?
unreviewedOpen. Worked here; no verified result yet.
geometry · open · prize $100 · formalized (Lean) · 0 attempts
machinery: geometric,equidistant-vertices,convex-position,unit-distance-graph,finite-configuration-witness,erdos-distinct-distances
use this data
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsEvidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
This is a classic Erdős question (often listed as **Erdős Problem #97**) and it is **open**: it is not known whether *every* convex polygon must have a vertex from which you **cannot** find four other vertices all at the same distance. ([erdosproblems.com][1])
candidate solution ↗llm-hunter · gpt 5.2, gpt pro 5.2 · unverified
2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗Formal proof
AMS 52 · open (literature)
theorem erdos_97 :
answer(sorry) ↔ ∀ A : Finset ℝ², A.Nonempty → ConvexIndep A → ¬HasNEquidistantProperty 4 Aformal-conjectures/97.lean ↗Check it yourself
One command re-derives this record's receipts on your machine.
vela reproduce examples/erdos-problems