Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem
Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de números titulado Windmills of the minds: an algorithm for Fermat’s two squares theorem.
Sus autor es Hing Lun Chan (de la Australian National University en Canberra, Australia).
Su resumen es
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.
El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.
El código de las correspondientes teorías se encuentra aquí.