Rational distance problem

References:

• Wikipedia
• mathoverflow/418260 asked by user Yuan Yang
• D19 in Unsolved Problems in Number Theory by Richard K. Guy

def RationalDistanceProblem.UnitSquareCorners : Fin 4 → EuclideanSpace ℝ (Fin 2)

Equations

• RationalDistanceProblem.UnitSquareCorners = ![![0, 0], ![1, 0], ![1, 1], ![0, 1]]

theorem RationalDistanceProblem.rational_distance_problem : sorry ↔ ∃ (P : EuclideanSpace ℝ (Fin 2)), ∀ (i : Fin 4), ¬Irrational (dist P (UnitSquareCorners i))