Conjectures.io

Convex and discrete geometry

Erdős 982

If nn distinct points in R2\mathbb{R}^2 form a convex polygon then some vertex has at least ⌊n2⌋\lfloor\frac{n}{2}\rfloor different distances to other vertices.

References

No one has attempted this yet.

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-379fc029-erdos982-erdos-982-1d8ab9506a-formalized-v1
Task commitment
sha256:1dc37f6aa8ca6066e659a5ce79d3b79765f2effc8f07968551231ffec6f0e7db

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.