Convex and discrete geometry

Erdős 100

Is the diameter of

A

at least

Cn

for some constant

C > 0

References

erdosproblems.com/100

Kanold
GuKa15
Piepmeyer

No one has attempted this yet.

Formal statement

Lean type

True ↔
  ∃ C > 0,
    ∀ᶠ (n : ℕ) in Filter.atTop,
      ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑n

What you must prove

import FormalConjectures.ErdosProblems.«100»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos100.erdos_100" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/100.lean

Source type SHA-256: sha256:67345968121f038b64220e15ea294c9eace0ba0bb2ae2304143d4bb2d3bae514
Task id: fc-379fc029-erdos100-erdos-100-4054f0a606-formalized-v1
Task commitment: sha256:5fa1ea821d76a926b36ae97740d139cb9eb4bf0e871b95b6001d954a4e6132a1

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.