Windmills of the minds: an algorithm for fermat's two squares theorem
HL Chan�- Proceedings of the 11th ACM SIGPLAN International�…, 2022 - dl.acm.org
HL Chan
Proceedings of the 11th ACM SIGPLAN International Conference on Certified�…, 2022•dl.acm.orgThe 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�…
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�…
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.
ACM Digital Library