Convex & discrete geometry · Last catalog review 26 Jul 2026

Erdős Problem 982

n

distinct points in

\mathbb{R}^2

form a convex polygon then some vertex has at least

\lfloor\frac{n}{2}\rfloor

different distances to other vertices.

References

erdosproblems.com/982

Published 23 Jul 2026Never attempted

Formal statement

Lean type

∀ (n : ℕ),
  3 ≤ n →
    ∀ (p : Fin n → EuclideanSpace ℝ (Fin 2)),
      Function.Injective p →
        EuclideanGeometry.IsConvexPolygon p → ∃ i, {d | ∃ j, j ≠ i ∧ d = dist (p i) (p j)}.ncard ≥ n / 2

What you must prove

import FormalConjectures.ErdosProblems.«982»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos982.erdos_982" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/982.lean

Source type SHA-256: sha256:0a01ef88795bf069398d58438ffc583a4dd349255095f8807f7c61a6483818a6
Task id: fc-e923379e-erdos982-erdos-982-52e88ff869-formalized-v1
Task commitment: sha256:196d2ea88825977d8bd1f82744210dfb67f942a0996ef07fd109f3c5d6e106c0

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.