---

Claim. The statement of Problem 93 is true. E. Altman, On a problem of P. Erdős, Amer. Math. Monthly 70 (1963), no. 2, 148--157, proves the Theorem of its p. 149, whose heading names Erdős as the proposer: the vertices of any convex $n$-gon in the plane determine at least $\lfloor n/2\rfloor$ distinct distances. The bound is attained, by the regular $(2N+1)$-gon for odd $n$ and by a regular $(2N+1)$-gon with one vertex removed for even $n$ (the Remark, p. 157). The proof takes, among the diagonals of maximum length, one that cuts off the fewest consecutive sides, $x$ of them; it splits the polygon into an $(x+1)$-gon in which that diagonal is strictly the longest segment and an $(n-x+1)$-gon in which it is of maximum length. Lemma 2 (p. 151) gives at least $n-1$ distinct distances in a convex $n$-gon with a strictly longest side and at least $n-2$ with a side of maximum length, by repeated use of Lemma 1 (p. 149), which produces, from a diagonal of a polygon whose side $A_1A_n$ is longest, a strictly shorter diagonal sharing a vertex with it. The two parts supply at least $x$ and $n-x-1$ distances of the original polygon, and fewer than $\lfloor n/2\rfloor$ in all would force an impossible integer $x$. The theorem is paged at Theorem, p. 149 of the source card altman_1963_problem_p_erdos, which records the proof coverage.

Depends on. No page of this wiki.

Acceptance. The result is refereed: it appeared in the American Mathematical Monthly. The site's curator, Thomas Bloom, marks the problem proved and credits Altman with the solution (problem page last edited 19 October 2025). The corpus's proof coverage of the paper is local and is not counted as acceptance evidence here.

Formalization. Boris Alexeev's lean-proofs repository holds, at the pinned commit linked above, a Lean 4 file whose header declares it a formalization of a solution to Problem 93 with Altman as the informal author and, as formal authors, Gemini 3.0 Flash and Pro, Claude Opus 4.5 and 4.6, the Numina Lean Agent, Aristotle and the site's forum user JoshuaB, who announced it on the discussion thread on 17 February 2026 as a formalization of Altman's paper; the site's label carries a Lean marker. Its theorem Erdos93.altman_erdos takes a finite set s of n ≥ 3 points in a real inner product space of dimension two that is convex independent and concludes that the set of distances between distinct points of s has at least n / 2 elements, natural-number division giving the floor; the cases $n\le2$ are trivial. The file prints the axioms of that theorem as propext, Classical.choice and Quot.sound. This corpus has not built the file, audited its axioms or reviewed its statement, so the file is a link here and not formalized evidence.