Erdős Problem a Daythe open tracker

Erdős Problem #97

FALSIFIABLEdatabase updated 2025-08-31

Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

A set of points \(A\) has n equidistant points at \(p\) if there exist at least \(n\) other points in \(A\) that are equidistant from \(p\).

A set of points \(A\) has n equidistant points on a set of points \(B\) if for every point in \(B\), there exist at least \(n\) other points in \(A\) that are equidistant from it.

A set of points \(A\) has n equidistant property if for every point in \(A\), there exist at least \(n\) other points in \(A\) that are equidistant from it.

Does every convex polygon have a vertex with no other 4 vertices equidistant from it?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/97.
Prize$100
Topicsgeometry, distances, convex
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/97
EARLY RUN BY THIS SITE · MAY 26, 2026

The one that beat every model at every budget in our cross-model bench. Best outcome: an honest decline.

WALL