Fermat's right triangle theorem

Stream: Is there code for X?

[Ruben Van de Velde]

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

[Johan Commelin]

@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 (-;

[Johan Commelin]

Pythagorean triples have been classified in mathlib some time ago.

[Joseph Myers]

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

[Joseph Myers]

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.

[Joseph Myers]

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?

[Ruben Van de Velde]

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

[Reid Barton]

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

[Ruben Van de Velde]

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