Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 93

claims/: The 1 claim page of Problem 93, one per claimant's result; the problem's standing derives from them.

Statement. If $n$ distinct points in $\mathbb{R}^2$ form a convex polygon then they determine at least $\lfloor \frac{n}{2}\rfloor$ distinct distances.

Status. Proved. The site's export of 2026-09-04 labels the problem "PROVED (LEAN)" (page last edited 19 October 2025) and credits Altman's 1963 proof; see the claim page.

Source. erdosproblems.com/93, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #93, https://www.erdosproblems.com/93.

References.

[Al63] Altman, E., On a problem of P. Erdős. Amer. Math. Monthly 70 (1963), no. 2, 148--157, JSTOR 2312883; the Theorem, printed p. 149, with Lemmas 1 and 2 and its proof, pp. 149--153; the regular polygon and the Remark, p. 157. Library home: altman_1963_problem_p_erdos, result page Theorem, p. 149.

Formalization. Statement in formal-conjectures. Boris Alexeev's repository holds a Lean 4 file, produced with Gemini 3.0 Flash and Pro, Claude Opus 4.5 and 4.6, the Numina Lean Agent and Aristotle and announced on the site's discussion thread on 17 February 2026, whose header declares it a formalization of Altman's solution; it is a formalization link on Altman's claim page, not a claim of its own, and this corpus has not built it. There is no native Lean coverage.

Current assessment

Proved. The site formulation above (page last edited 19 October 2025) is Erdős's conjecture that the vertices of a convex $n$ -gon in the plane determine at least $\lfloor n/2\rfloor$ distinct distances. Altman (Amer. Math. Monthly 1963, refereed; credited by the site's curator) proved it, and the regular polygon shows the bound is sharp; the Lean formalization the site flags is linked on the claim page. The standing derives from this accepted claim.

Related questions are separate problems. Whether some single vertex of a convex $n$ -gon determines at least $\lfloor n/2\rfloor$ distinct distances is Problem 982, open; Altman's introduction records Moser's bound $\lfloor(n+2)/3\rfloor$ for it. Fishburn's conjecture that the numbers $R(x)$ of distinct distances from the vertices sum to at least $\binom n2$ , and Szemerédi's variant with convexity replaced by no three points on a line (Problem 1082), are stronger statements the site records as open; the three-dimensional analog is Problem 660.

Compiled proof coverage. The Theorem is paged at Theorem, p. 149 of the source card, which records the proof coverage. Nothing here is independently reviewed, and no native L-claim covers the result.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (19)

Altman's proof of the convex polygon distance bound problems/distance_problems/E0093/claims Problem 660 Problem 1082 Altman's convex polygon bound settles convex position Distance Problems distance_problems/altman_1963_problem_p_erdos Theorem (p. 149): a plane convex n-gon determines at least [n/2] distinct distances distance_problems/erdos_1946_sets_distances_points Conjectures (p. 248): a convex n-gon determines at least [n/2] distances, and has a vertex with no three vertices equidistant from it distance_problems/erdos_1975_problems_elementary_combinatorial_geometry Section 1, the three convex-polygon conjectures (p. 100): Altman's theorem, the single-vertex form, and Danzer's counterexample Erdős–Fishburn: Multiplicities of interpoint distances in finite planar sets Erdős–Fishburn: Maximum planar sets that determine k distances Lemma 2 (p. 118): a convex n-gon has at least ⌊n/2⌋ distances, with the extremal and near-extremal polygons Fishburn: Convex polygons with few intervertex distances Theorem 1 (p. 66, Altman): a convex n-gon has at least floor(n/2) intervertex distances, with equality for odd n only at the regular n-gon distance_problems/sheffer_2014_distinct_distances_open_problems_current_bounds Problem 7 (p. 6): the exact value of the single-point distance count for convex position

Graph