Zulip Chat Archive

Stream: general

Topic: Four distance problem


Lars Ericson (Jan 01 2023 at 21:28):

This is a briefly stated open problem in rational numbers for which Lean has the structure built up to check a proof, if one existed: "Given a unit square in the plane. Is it possible for all four distances from any point in the square to the four vertices to be rational numbers?"

References:

http://www.math.bas.bg/smb/kolokvium/2022_11_16-NKM-Jordan_Stoyanov-talk.pdf
https://arxiv.org/pdf/1904.12097.pdf
https://unsolvedproblems.org/index_files/RationalDistance.htm

Heather Macbeth (Jan 01 2023 at 21:39):

Lars Ericson said:

Lean has the structure built up to check a proof, if one existed

Better not to make a claim like that until a proof actually exists and you can see what it uses :)

Junyan Xu (Jan 01 2023 at 21:40):

A similar unsolved problem is https://en.wikipedia.org/wiki/Euler_brick#Perfect_cuboid

Junyan Xu (Jan 01 2023 at 21:51):

https://en.wikipedia.org/wiki/Congruent_number is also about Diophantine equations from elementary geometry.

Let me mention there are rational angle problems as well, but the question is not existence but classification in general:
Planar quadrilateral: https://en.wikipedia.org/wiki/Langley%27s_Adventitious_Angles
Recent work on tetrahedra:
https://github.com/kedlaya/tetrahedra#readme
https://mobile.twitter.com/marty__weissman/status/1333670741590503425

Michael Stoll (Jan 01 2023 at 21:53):

Heather Macbeth said:

Better not to make a claim like that until a proof actually exists and you can see what it uses :)

Cf. Fermat's Last Theorem :smile:

Eric Wieser (Jan 02 2023 at 00:43):

Easy :upside_down: :

import topology.metric_space.basic
import data.real.irrational

lemma no_not_like_that (x :  × ) :
  -- a point within the square
   x (h₁ : (0, 0)  x) (h₂ : x  (1, 1)),
    -- such that the "distance" to every point is rational
    ¬irrational (dist x ((0, 0) :  × )) 
    ¬irrational (dist x ((0, 1) :  × )) 
    ¬irrational (dist x ((1, 1) :  × )) 
    ¬irrational (dist x ((1, 0) :  × )) :=
begin
  refine ⟨(2⁻¹, 2⁻¹), _, _, _⟩,
  { norm_num },
  { norm_num },
  norm_num [prod.dist_eq, real.dist_eq, abs, irrational_inv_iff],
  simp_rw [one_div, irrational_inv_iff],
  exact_mod_cast (2 : ).not_irrational
end

Oisin McGuinness (Jan 02 2023 at 02:58):

Yes, it is easy to prove by hand or in Lean, that in the case when the point is inside the square, that the coordinates are forced to be rational. But following the links referenced by Lars, which have interesting diagrams to illustrate, that the hard problem is when the given point is outside the square, and that case is not proven.... :smile:

Oisin McGuinness (Jan 02 2023 at 03:02):

So the "in the square" in the first post should be "in the plane" to match the references...

Eric Wieser (Jan 02 2023 at 11:45):

@Oisin McGuinness, in case it wasn't obvious; my proof above isn't showing that the problem is trivial, but is instead exploiting an ambiguity in what is meant by distance. It uses the inf norm not the euclidean norm, as that happens to be the default!

Kevin Buzzard (Jan 02 2023 at 12:54):

That's only an ambiguity caused by a really poor default choice on lean's part as opposed to anything a mathematician would care about

Patrick Massot (Jan 02 2023 at 12:56):

Lean didn't choose anything, we did.

Patrick Massot (Jan 02 2023 at 12:57):

And Eric purposefully chose to use the wrong representation of R2\mathbb{R}^2 in his joke.

Kevin Buzzard (Jan 02 2023 at 12:59):

Aah I see. So the version of R^2 with the correct metric is there but under another name? My point still stands that no mathematician would ever say "ah but with what metric on R^2? There are many!"

Patrick Massot (Jan 02 2023 at 13:04):

Sure, the intended one is euclidean_space ℝ (fin 2).

Eric Wieser (Jan 02 2023 at 14:34):

Of course, if they really did mean to talk about the inf metric, the problem would be about points in a unit "circle"...

Eric Wieser (Jan 02 2023 at 14:35):

There has been some discussion about having a euclidean_space version of prod before: (or prod_Lp which is at least sensible for p ∈ {1, 2, ∞}), but it's a lot of boilerplate and mid-port would be a bad time to pursue it.

Mario Carneiro (Jan 02 2023 at 18:19):

Using the euclidean norm on general products doesn't work very well to fix this issue, since then ℝ × (ℝ × ℝ) and (ℝ × ℝ) × ℝ get completely different metrics, and neither one is the one you would expect

Eric Wieser (Jan 02 2023 at 18:30):

I agree, but only when p ∈ {1, 2, ∞} doesn't hold


Last updated: Dec 20 2023 at 11:08 UTC