Convex and discrete geometry

Erdős 213

Let

n \geq 4

. Are there

n

points in

\mathbb{R}^2

, no three on a line and no four on a circle, such that all pairwise distances are integers?

References

erdosproblems.com/213

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ n ≥ 4, Erdos213.Erdos213For n

What you must prove

import FormalConjectures.ErdosProblems.«213»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos213.erdos_213" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/213.lean

Source type SHA-256: sha256:c9cf524700e14d4dd7b374b0448dd2ab0eeefde35c4567aba82d9151e52ea302
Task id: fc-379fc029-erdos213-erdos-213-a78924f7ae-formalized-v1
Task commitment: sha256:279abe06a2e1d0197b6c7fc19a047935a1ccbb9df3aa5c52555441f2f05e3796

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.