Windmills of the minds: an algorithm for Fermat's Two Squares Theorem
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.
Keywords
Cite
@article{arxiv.2112.02556,
title = {Windmills of the minds: an algorithm for Fermat's Two Squares Theorem},
author = {Hing Lun Chan},
journal= {arXiv preprint arXiv:2112.02556},
year = {2022}
}
Comments
14 pages, 6 tables, 10 figures. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), January 17-18, 2022, Philadelphia, PA, USA