Claims

../

1995_09_01_lefmann_thiele: Lefmann and Thiele prove that n plane points with no three on a line have sum of squared distance multiplicities O(n^3); the vertices of a convex polygon are such a set, so the bound Erdős conjectured holds.

2026_01_15_dingding: A Lean file generated with Seed-Prover, posted on the site's thread on 15 January 2026 by the account Dingding for the SpringSense Innovation Institute; its proof gives the cubic bound, its theorem a set-dependent bound.

---