Conjectures.io

Convex and discrete geometry

Erdős 96

If nn points in R2\mathbb{R}^2 form a convex polygon then there are O(n)O(n) many pairs which are distance 11 apart.

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ (fun n => ↑(Erdos96.maxConvexUnitDistances n)) =O[Filter.atTop] fun n => ↑n

What you must prove

import FormalConjectures.ErdosProblems.«96»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos96.erdos_96" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/96.lean

Source type SHA-256
sha256:4f0d18cb094f2f8abff1478bf1dfbcdc2c1372dc6a46e485897c9edba23664db
Task id
fc-379fc029-erdos96-erdos-96-69ee2f50c8-formalized-v1
Task commitment
sha256:03d85a305123a49cdbb0fa6b3200c05b23acacd76f76dcbd0bf36d84d68b4520

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.