Erdős Problem 213

Reference: erdosproblems.com/213

def Erdos213.Erdos213For (n : ℕ) : Prop

The predicate (on $n$) that there exist $n$ points in $\mathbb{R}^2$, no three on a line and no four on a circle, such that all pairwise distances are integers?

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos213.erdos_213 : (∀ n ≥ 4, Erdos213For n) ↔ sorry

Let $n ≥ 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?

theorem Erdos213.erdos_213.variants.KK08 : Erdos213For 7

The best construction to date, due to Kreisel and Kurz, has $n = 7$.