Zulip Chat Archive

Stream: Is there code for X?

Topic: Fermat's right triangle theorem


view this post on Zulip Ruben Van de Velde (Sep 01 2020 at 17:29):

https://en.wikipedia.org/wiki/Fermat%27s_right_triangle_theorem

view this post on Zulip Johan Commelin (Sep 01 2020 at 17:42):

@Ruben Van de Velde We don't have that, but you can state it using all the material that @Joseph Myers has been adding on affine spaces, triangles and Pythagoras. Afterwards, the reduction to a Diophantine equation shouldn't be too hard. Finally, the infinite descent proof would be fun to do (-;

view this post on Zulip Johan Commelin (Sep 01 2020 at 17:43):

Pythagorean triples have been classified in mathlib some time ago.

view this post on Zulip Joseph Myers (Sep 01 2020 at 20:10):

That seems like something it's most natural to state purely as a number theory problem, without involving geometry at all (just like the classification of Pythagorean triples).

view this post on Zulip Joseph Myers (Sep 01 2020 at 20:13):

There are some geometrical number theory problems that have more geometrical content and so might more naturally be stated in terms of geometrical definitions. E.g. IMO 2016 problem 3, which we can't state at present because it involves areas and I don't think we have two-dimensional Lebesgue measure yet.

view this post on Zulip Joseph Myers (Sep 01 2020 at 20:22):

One question the IMO Grand Challenge will need to consider is how literal the formal versions should be of algebra / combinatorics / number theory problems expressed for humans in geometrical terms: should the formal version also be expressed geometrically so a formal solution needs to include the reduction to algebra / combinatorics / number theory, even if that reduction is both so trivial to humans that they wouldn't mention it in an informal solution, and possibly harder to formalize than the main substance of a solution?

view this post on Zulip Ruben Van de Velde (Sep 01 2020 at 20:41):

I think I'll see if I get anywhere with the infinite descent of x4y4=z2x^4 - y^4 = z^2, I haven't looked at geometry in mathlib yet

view this post on Zulip Reid Barton (Sep 01 2020 at 20:45):

This was one of the first things I ever wrote in Lean. It's a fun project.

view this post on Zulip Ruben Van de Velde (Sep 04 2020 at 08:39):

@Reid Barton do you still have the code, by any chance?


Last updated: May 16 2021 at 05:21 UTC