Erdős #97 — convex polygon vertex with no 4 equidistant

Statement

Does every convex polygon have a vertex with no other $4$ vertices equidistant from it?

Equivalently: is it true that for every finite $A\subset\mathbb R^2$ in convex position, some point $p\in A$ has, for every $r>0$, fewer than $4$ other points of $A$ at distance exactly $r$ from $p$? A "no" answer is witnessed by a single finite convex polygon where *every* vertex has $\geq 4$ other vertices equidistant from it (not necessarily at the same distance $r$ across vertices).

Facts

- Prize \$100; status per erdosproblems.com/97 (site-owner belief, verified by direct fetch 2026-07-02): OPEN, FALSIFIABLE — "Open, but could be disproved with a finite counterexample." - Falsifiable: yes — a single explicit convex $n$-gon where every vertex sees $\geq 4$ equidistant others would settle it (in the negative). No finite computation can *prove* the positive direction (it is a $\forall$-over-all-$n$ statement), only refute it. - Origin: #97 : [Er46b] [Er61] [Er75f,p.100] [Er87b,p.175] [Er90] [Er92e] [Er95] [Er97e]. Erdős originally (1946, [Er46b]) conjectured the *stronger* statement with "$3$" in place of "$4$" — i.e., that some vertex has no other 3 vertices equidistant from it. - The original ($k=3$) conjecture is FALSE, settled by two explicit constructions (both reported on erdosproblems.com/97, cross-confirmed in the AlphaEvolve paper's §33, arXiv:2511.02864): - Danzer (explained in [Er87b], Erdős, "Some combinatorial and metric problems in geometry," *Intuitive Geometry* (Siófok, 1985), 167-177) constructed a convex $9$-gon in which every vertex has $3$ other vertices equidistant from it — but the distance realizing this varies vertex-to-vertex. - Fishburn & Reeds [FiRe92] (P. C. Fishburn, J. A. Reeds, "Unit distances between vertices of a convex polygon," *Computational Geometry* 2(2) (1992), 81-91) strengthened this to a single *uniform* distance: a convex $20$-gon that is "absolutely $3$-uniform," i.e. every vertex has exactly $3$ others at the *same* fixed distance $d_0$ (all pairs literally unit-distance pairs after rescaling). They also proved $n=20$ is the *minimum* size for which a convex polygon can be cut into two parts $A,B$ (disjoint convex hulls) such that every $a\in A$ has $\geq 3$ points of $B$ at distance $1$, and vice versa (formalized as erdos_97.variants.three_unit_distance_cut_min in the Lean file below). - So the genuine open question is exactly the site's current $k=4$ phrasing. - A stray, apparently-mistaken claim: in [Er75f] Erdős wrote that Danzer had in fact proved falsity *for every* constant $k$ (i.e. for any $k$ there's a convex polygon where every vertex has $k$ equidistant others). This claim is not repeated in any of Erdős's later papers on the problem, and erdosproblems.com explicitly flags it as "presumably Erdős was mistaken here" — i.e. it should not be treated as an established result for $k=4$. - Convexity is essential: if the convex-position requirement is dropped, the statement is simply false for every $k$ — take any $d$-regular unit-distance graph in the plane (e.g. the $2^d$-vertex hypercube graph embedded with all edges of length 1) and thread its vertices into a (non-convex) closed polygonal cycle with no 3 collinear consecutive vertices (credited on the page to Boris Alexeev and Dustin Mixon). - AI attempt found no counterexample for $k=4$: DeepMind's AlphaEvolve (Novikov et al., "Mathematical exploration and discovery at scale," arXiv:2511.02864, §33, PDF read directly 2026-07-02) was set up to search for a $k=4$ counterexample. Objective: normalize the polygon to diameter 1; for each vertex, sort its distances to the other vertices, find the 4 consecutive distances $d_1,d_2,d_3,d_4$ with smallest total gap, let $d$ be their mean, and define the vertex's "equidistance error" as $\max_i\{\max(d/d_i,\,d_i/d)\}$ divided by the squared minimum side length; the polygon's score is the min over vertices, maximized by the evolutionary search. Result: AlphaEvolve reproduced configurations with the $k=3$ property (matching Danzer/Fishburn-Reeds) but could not find any configuration achieving $k=4$ for every vertex. This is empirical negative evidence (not a proof) that the conjecture may be true, from a system that in the very same paper (and independently, via an OpenAI internal model in May 2026 — see Erdős #90 — the unit distance conjecture (disproved 2026)) *did* succeed at cracking sibling problems in this same distance-counting family. - Formalized: Yes (per problems.yaml, formalized.state: yes, last update 2025-11-11 — same window as the AlphaEvolve paper). FormalConjectures/ErdosProblems/97.lean (google-deepmind/formal-conjectures, read in full) states the main conjecture erdos_97 (@[category research open], sorry), the already-*solved* $k=3$ existence result erdos_97.variants.three_equidistant (with the Danzer 9-point construction's coordinates spelled out explicitly as algebraic numbers involving $\sqrt3$, but proof itself still sorry'd), a k_equidistant existential variant (does *some* finite $k$ work at all — also open, sorry), the Fishburn-Reeds absolute-3-uniform existence lemma (sorry), and the Fishburn-Reeds cut-minimality theorem = 20 (sorry). So: statements are formalized, but zero machine-checked proofs exist yet, even for the historically-solved $k=3$ sub-results. - **Relation to erdos/96**: Erdős explicitly suggested #97 as an approach to #96 (does every convex $n$-gon have $O(n)$ unit-distance pairs?). By induction, if #97 holds for "$k+1$ vertices" (i.e., no vertex has $k$ others equidistant, for the relevant $k$), this yields an upper bound of $kn$ pairs for #96. So a positive resolution of the $k=4$ case here would give a $\leq 3n$-type bound on #96 (erdosproblems.com/96: "A positive answer would follow from [97]"). - Related problems: erdos/96 (upper bound on # unit-distance pairs in convex $n$-gons — #97's raison d'être), Erdős #90 — the unit distance conjecture (disproved 2026) (the general, non-convex unit-distance problem — recently *disproved*, see Literature state).

Literature state

Not resolved. The $k=4$ statement as currently phrased on erdosproblems.com is exactly the open residual of a problem whose weaker $k=3$ form was killed twice (Danzer 1985-ish / [Er87b]; Fishburn-Reeds 1992, [FiRe92], *Computational Geometry* 2(2):81-91) — both by explicit, hand-built finite constructions, not by a general theory. No paper in the 1992-2026 window claiming a $k=4$ (or higher) counterexample, or a proof of the $k=4$ statement, was found: the most recent and most relevant attempt is DeepMind's AlphaEvolve run (Nov 2025, arXiv:2511.02864 §33), an *evolutionary/LLM-guided numerical search* explicitly targeting a $k=4$ counterexample via a custom "equidistance-error" loss, which failed to find one while easily reproducing the known $k=3$ examples — i.e. the one systematic computational search effort on record came back empirical (not proof-grade) evidence *for* the conjecture. The erdosproblems.com "Partial Solution" section is explicit: "There are no solutions, partial or complete, claimed in the comments" (verified live, 2026-07-02). The problem is formalized in Lean (google-deepmind/formal-conjectures) but every relevant lemma, including the already-published $k=3$ results, is still sorry'd — there is no machine-checked proof of anything here yet, so "formalized" should not be read as "any part is verified."

The closest genuinely *solved* problem in this exact family is Erdős #90 — the unit distance conjecture (disproved 2026) (the general planar unit-distance problem, Erdős 1946): this was long believed to have upper bound $n^{1+o(1)}$, and stood essentially untouched in its polynomial exponent since Spencer-Szemerédi-Trotter's $O(n^{4/3})$ (1984) — until an internal OpenAI reasoning model disproved it in May 2026 by constructing an explicit infinite family with $\geq n^{1+\delta}$ unit-distance pairs (announced by OpenAI: https://openai.com/index/model-disproves-discrete-geometry-conjecture/; human-digested and verified writeup by Alon, Bloom, Gowers, and six coauthors: "Remarks on the disproof of the unit distance conjecture," arXiv:2605.20695, abstract read directly). The abstract credits the underlying ideas to Ellenberg-Venkatesh (bounding the size of point sets with few distinct distances via algebraic-geometric/arithmetic methods), Golod-Shafarevich (towers of number fields / class field towers with bounded root discriminant), and Hajir-Maire-Ramakrishna (explicit tame towers achieving near-optimal root discriminant) — i.e. a genuinely new, deep algebraic-number-theoretic construction, not a search-and-optimize trick. A follow-up (P. Sawin et al., "Optimizing Explicit Unit-Distance Lower-Bound Certificates," arXiv:2606.03419) refined the exponent to an explicit $\delta = 0.014$. This is the single most important precedent for #97: it shows that in *this exact* "how many equal-distance incidences can a planar point configuration force" problem family, the wall that beat 80 years of elementary/combinatorial attack fell not to more search, but to importing a specific, non-obvious piece of algebraic number theory. #97's convex-position constraint is a genuinely different (much more rigid) setting than #90's unrelated point set, so the Ellenberg-Venkatesh/Golod-Shafarevich machinery does not obviously transfer, but it is the strongest available signal that "clever explicit algebraic constructions can beat naive/evolutionary search" in this problem family.

The other close relative, erdos/96 (is the number of unit-distance pairs in a convex $n$-gon $O(n)$?), remains open but has real partial progress via extremal/combinatorial-graph technique, not deep algebra: Füredi ("The maximum number of unit distances in a convex $n$-gon," *J. Combin. Theory Ser. A* 55 (1990), 316-320) proved $O(n\log n)$ via a 0-1 matrix / forbidden-submatrix encoding of the unit-distance graph of a convex polygon; Brass and Pach gave a short alternative proof of the same bound using an antipodal-cut induction (splitting the polygon by an antipodal pair and recursing); the current record, $n\log_2 n + 4n$, is due to Aggarwal ("On Unit Distances in a Convex Polygon," arXiv:1009.2216 / *Discrete Math.* 2015), who additionally identified forbidden cyclic patterns that unit-distance graphs of convex polygons cannot contain (a companion paper, arXiv:1009.2218, bounds the number of isosceles triangles and inscribed regular $k$-gons the same way). Since Erdős's own remark ties #97's $k$-case directly to a $kn$ bound on #96, any future progress squeezing #97's $k$ down (e.g. ruling out $k=4$ only under extra structural hypotheses) would immediately feed a better constant into #96 via the same induction — but the induction runs in that one direction only (#97 $\Rightarrow$ bound on #96), not the reverse.

Attack surface

- Mode: finite-search (primary, since falsifiable) + literature-resolution (secondary — check for post-Nov-2025 arXiv follow-ups to the AlphaEvolve run, since this is a fast-moving area with an active AI-vs-Erdős-problems pipeline in 2026) + derivation (transplant the Ellenberg-Venkatesh/Golod-Shafarevich-style algebraic-construction idea from Erdős #90 — the unit distance conjecture (disproved 2026)'s disproof, or the antipodal-cut/forbidden-pattern combinatorics from erdos/96's upper bound, into the convex-position $k=4$ search). - Concrete first experiment: re-run an AlphaEvolve-style evolutionary/gradient search but seeded structurally rather than from scratch — start from the Fishburn-Reeds absolute-3-uniform 20-gon (or Danzer's 9-gon) and search local perturbations/extensions (adding vertices, relaxing "same distance across all vertices" back to "per-vertex distance," as Danzer's original $k=3$ example does) that push one extra equidistant pair onto every vertex simultaneously; alternatively, a direct MILP/CP-SAT formulation over rational or bounded-algebraic-degree coordinates of $n$-gons ($n$ up to ~30-40) maximizing $\min_v(\text{count of other vertices at some common distance from }v)$, using exact/interval arithmetic to certify any candidate's convexity and the equidistance counts (avoiding the false-positive risk AlphaEvolve's paper explicitly worried about — "naive attempts to cheat by moving points really close/far apart," addressed there by the diameter-normalized loss). - Oracle: fully mechanical — given a candidate finite point set with exact (rational or low-degree-algebraic) coordinates, (a) verify convex position (all points on the convex hull, e.g. via exact-arithmetic cross products), (b) for each vertex compute exact pairwise distances (or squared distances, avoiding square roots, to stay in exact arithmetic) and check whether $\geq 4$ of them coincide. A "yes" instance is a 100%-certain, computer-checkable disproof (this is exactly why the problem is tagged FALSIFIABLE); a Lean formalization already exists (FormalConjectures/ErdosProblems/97.lean) to receive a machine-checked witness once found. - Feasibility: honest read — plausibly in reach for a bounded search effort, but already attempted once by a strong system (AlphaEvolve) and it failed to find $k=4$, which is real (if not conclusive) evidence the true answer is "no counterexample exists" / the conjecture holds, in which case finite search alone cannot resolve it (would need a genuine proof, likely combinatorial/extremal in flavor given #96's precedent, rather than a search win). The most promising *concrete*, low-risk next move is not re-running the same kind of search harder, but (i) structurally seeding the search from the known Fishburn-Reeds/Danzer $k=3$ extremal examples instead of from scratch, and (ii) formalizing the already-published $k=3$ results in Lean (currently all sorry'd) as a well-defined, guaranteed-tractable side task that also produces reusable machinery (exact-distance-equality tactics, convex-position checkers) for any future $k=4$ search.

Related

- erdos/96 — is the number of unit-distance pairs in a convex $n$-gon $O(n)$? #97 was proposed by Erdős himself as the route to this bound (#97 holding for $k+1$ $\Rightarrow$ $\leq kn$ bound on #96); best known bound $n\log_2n+4n$ (Aggarwal, arXiv:1009.2216), open. - Erdős #90 — the unit distance conjecture (disproved 2026) — the general (non-convex) planar unit-distance problem; DISPROVED May 2026 by an OpenAI internal model via deep algebraic-number-theory construction (Golod-Shafarevich towers / Ellenberg-Venkatesh / Hajir-Maire-Ramakrishna, arXiv:2605.20695), showing this exact problem family is amenable to AI-discovered non-search-based constructions. - concept/equidistant-point-configurations — the general object (convex point sets where each point sees $k$ others at a shared distance); the $k=3$ boundary is fully understood (Danzer, Fishburn-Reeds), $k=4$ is the open frontier. - concept/absolute-k-uniform-convex-polygon — Fishburn-Reeds's terminology/construction for a convex polygon where *every* vertex has exactly $k$ others at one shared global distance $d_0$; their 20-gon is absolutely 3-uniform and provably minimal (= 20, formalized as a Lean statement, unproven). - concept/unit-distance-graph-forbidden-patterns — Füredi's 0-1-matrix / forbidden-submatrix encoding and Aggarwal's forbidden-cyclic-pattern refinement, the technique behind every known upper bound on erdos/96 ($O(n\log n)$ down to $n\log_2n+4n$). - concept/antipodal-cut-induction — Brass-Pach's short inductive proof technique for the erdos/96 upper bound, splitting a convex polygon along an antipodal pair; structurally similar in spirit to Fishburn-Reeds's own "cut" construction (IsCut in the Lean file) used for their $n=20$ minimality result. - concept/alphaevolve-combinatorial-construction-search — DeepMind's evolutionary/LLM-guided search (arXiv:2511.02864 §33) with a custom diameter-normalized "equidistance error" loss, run specifically against #97's $k=4$ case; found nothing beyond $k=3$, the strongest empirical (non-proof) evidence currently on record either way. - concept/golod-shafarevich-towers-number-fields — the class-field-tower machinery (Golod-Shafarevich, Ellenberg-Venkatesh, Hajir-Maire-Ramakrishna) that produced the Erdős #90 — the unit distance conjecture (disproved 2026) disproof; not obviously transferable to the convex-position setting of #97, but the strongest available precedent that "import deep algebra, don't just search harder" can crack this problem family. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — FormalConjectures/ErdosProblems/97.lean (google-deepmind/formal-conjectures): main statement plus 4 sub-lemmas (including the Danzer/Fishburn-Reeds $k=3$ results, with Danzer's 9-point coordinates spelled out explicitly), all currently sorry'd.