Skip to content

Erdős problem 100

Start work

From [Piepmeyer]: 9 points with diameter <5< 5. TODO: find reference

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/100.lean

Formal Conjectures

FormalConjectures/ErdosProblems/100.leanErdos100.erdos_1004 linesExact file
True ↔  ∃ C > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑n
OpenStatement only, no proof

Continue

Start a contributionBrowse the source filesOpen the collection entry