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))

Does there exist a point in the plane at rational distance from all four vertices of the unit square?