Claims

../

1974_01_01_harborth: For every n at least 2, the largest number of unit distances among n planar points at mutual distance at least one is the floor of 3n minus the square root of 12n-3, attained by pieces of the triangular lattice.

2013_04_01_bezdek_reid: Among n points of 3-space at mutual distance at least one, fewer than 6n - 0.926 n^{2/3} pairs are at distance one, for every n at least 2; the upper half of Erdős's two-sided estimate for d = 3.

2026_06_11_sanexxxx777: A Lean proof contributed to formal-conjectures shows that n points of the line at mutual distance at least one have at most n-1 pairs at distance one, with equality attained; this corpus has not built it.

---