Erdős problem 94 · problems.science

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.$

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

94.lean

Retained formal statement1 of 4

In [Er97c] Erdős claims that Fishburn solved this, but gives no reference.

FormalConjectures/ErdosProblems/94.leanErdos94.erdos_944 linesExact file

1∃ C > 0,2  ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),3    EuclideanGeometry.ConvexIndep ↑P →4      ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3

SolvedProof has a holelean4formal statement referenceexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science