Windmills of the Minds: A Hopping Algorithm for Fermat’s Two Squares Theorem

Fermat’s two squares theorem asserts that a prime one more than a multiple of 4 is a sum of two squares. There are many proofs of this gem in number theory, including a remarkable one-sentence proof by Don Zagier based on two involutions on a finite set built from such a prime. Applying the two involutions alternatively leads to an iterative algorithm to find the two squares for the prime. Moreover, a detailed analysis of the computation reveals that it is possible to jump through the iteration nodes, leading to a better hopping algorithm. Here is a formalisation of Zagier’s proof, deriving the involutions using windmill patterns. Theories developed for the formal proof are used to establish the correctness of both algorithms.