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

Updated Oct 8

Problem 94

claims/: The 2 claim pages of Problem 94, one per claimant's result; the problem's standing derives from them.

Statement. Suppose $n$ points in $\mathbb{R}^2$ determine a convex polygon and the set of distances between them is $\{u_1,\ldots,u_t\}$ . Suppose $u_i$ appears as the distance between $f(u_i)$ many pairs of points. Then

\sum_i f(u_i)^2 \ll n^3.

Status. Proved. The site's export of 2026-09-04 records the label "PROVED (LEAN)". The proof is Lefmann and Thiele's theorem for point sets with no three on a line, recorded on [[problems/distance_problems/E0094/claims/1995_09_01_lefmann_thiele|its claim page]]; the Lean qualification refers to third-party developments that this corpus has neither built nor audited (see Formalization). Erdős's 1997 attribution of a proof to Fishburn, given without a reference, has no manuscript to page.

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

References.

[Er92e] Erdős, Pál, Some Unsolved problems in Geometry, Number Theory and Combinatorics. Eureka (1992), 44-48.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I, Algorithms Combin. 13, Springer (1997), 47--67; printed p. 65: "I conjectured and Fishburn proved that $\sum_is_i^2<cn^3$ " for the distance multiplicities $s_i$ of a convex polygon, stated without proof or reference. Library home: erdos_1997_some_my_favorite_problems_results; paged at conjecture_p65.
[LeTh95] Lefmann, Hanno and Thiele, Torsten, Point sets with distinct distances. Combinatorica (1995), 379-408.

Formalization. Statement in formal-conjectures, which at the linked commit of 2026-09-18 tags erdos_94 research solved with a pointer to a Lean proof in Boris Alexeev's repository. That proof and the earlier Lean proof posted on 2026-01-15 by the forum account Dingding for the SpringSense Innovation Institute, which it incorporates, are linked at pinned commits on the [[problems/distance_problems/E0094/claims/1995_09_01_lefmann_thiele|Lefmann–Thiele claim page]]; a Seed-Prover development the same account posted that day has its own claim page; this corpus has built and audited none of the three.

Progress

Not yet compiled.

Known Results

Not yet compiled.

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 (11)

Lefmann and Thiele's cubic bound on distance multiplicities A Seed-Prover Lean proof of the convex-polygon bound problems/distance_problems/E0094/claims Problem 95 Guth and Katz's bound on repeated distances Distance Problems Distance Problems Erdős–Fishburn: Multiplicities of interpoint distances in finite planar sets Theorem 4: for n = 4, 6, 8 the regular n-gon does not maximize the sum of squared multiplicities ramsey_theory/erdos_1997_some_my_favorite_problems_results Conjecture (p. 65): Σ s_i^2 < c n^3 for the distance multiplicities of a convex n-gon, stated as proved by Fishburn

Graph