Windmills of the minds: an algorithm for Fermat's Two Squares Theorem

TL;DR

This paper formalizes Fermat's Two Squares Theorem proof using windmill patterns and involutions, transforming a non-constructive existence proof into a constructive algorithm for finding two squares.

Contribution

It introduces a novel algorithm based on involutions and windmill patterns to explicitly compute the two squares in Fermat's theorem.

Findings

Algorithm successfully computes the two squares for given numbers.

Formalization links windmill patterns with involution fixed points.

Provides a constructive method from a non-constructive proof.

Abstract

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence "proof from the Book". Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.