@inproceedings{eee8f5e5126743d98a537161d41e0a4d,
title = "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 = "Algorithm, Iteractive Theorem Proving, Number Theory",
author = "Chan, {Hing Lun}",
note = "Publisher Copyright: {\textcopyright} 2022 ACM.; 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022 - co-located with POPL 2022 ; Conference date: 17-01-2022 Through 18-01-2022",
year = "2022",
month = jan,
day = "17",
doi = "10.1145/3497775.3503673",
language = "English",
series = "CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022",
publisher = "Association for Computing Machinery, Inc",
pages = "251--264",
editor = "Andrei Popescu and Steve Zdancewic",
booktitle = "CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022",
}