Fermat's Last Theorem in Lean 4

I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.

My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)

This is a very impressive result. Bravo to that team.

Front-page discussion: https://news.ycombinator.com/item?id=49568506

Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef

Mine is much shorter though...