头脑的风车:费马两方理论的算法 (Windmills of the minds: an algorithm for Fermat's Two Squares Theorem)

from arxiv, 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

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.

翻译：Fermat 的两个方形理论是数字理论中的宝石, 具有惊人的一则句子“ 校对于书中 ” 。这是对这一证据的正规化, 并使用风车模式进行解释。后面的理论涉及一定数目的进化, 特别是进化中固定点数的对等。作为非建构性的存在证据, 有一种巧妙的方法将它变成一个建设性的。这提供了一种算法, 将两个进化点从已知固定点转来计算这两个方形。