Stream: Is there code for X?
Ruben Van de Velde (Sep 01 2020 at 17:29):
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 (-;
Johan Commelin (Sep 01 2020 at 17:43):
Pythagorean triples have been classified in mathlib some time ago.
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).
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.
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?
Ruben Van de Velde (Sep 01 2020 at 20:41):
I think I'll see if I get anywhere with the infinite descent of , I haven't looked at geometry in mathlib yet
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.
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