 Authors

João F. Ferreira
 Downloads

 Paper: PDF (the original publication will be made available at SpringerLink)
 Status

Presented at the Tenth International Conference on Mathematics of Program Construction (MPC'10) in June 2010
 Abstract

We show a new and constructive proof of the twosquares theorem, based on a somewhat unusual but very effective, way of rewriting the socalled extended Euclid's algorithm. Rather than simply verifying the resultas it is usually done in the mathematical communitywe use Euclid's algorithm as an interface to investigate which numbers can be written as sums of two squares. The precise formulation of the problem as an algorithmic problem is the key, since it allows us to use algorithmic techniques and to avoid guessing. The notion of invariance, in particular, plays a central role in our development: it is used initially to observe that Euclid's algorithm can actually be used to represent a given number as a sum of two squares, and then it is used throughout the argument to prove other relevant properties. We also show how the use of program inversion techniques can make mathematical arguments more precise.
 Keywords

sum of two squares, Girard, Fermat, Euler, Gauss, Wagon, Brilhart, SmithCornacchia, Serret, Hermite, program inversion, number theory, calculational method, greatest common divisor, Euclid's algorithm, invariant, algorithm derivation
 Bibtex entry

@inproceedings{jff09:sumsquares, author = {Jo{\~a}o F. Ferreira}, title = {Designing an Algorithmic Proof of the TwoSquares Theorem}, booktitle = {Mathematics of Program Construction (MPC)} series = {LNCS}, volume = {5846}, year = {2010}, pages = {140156}, url = {http://joaoff.com/publications/2010/sumtwosquares}, }
 Related

 Our paper on Euclid's Algorithm and Number Theory: On Euclid's Algorithm and Elementary Number Theory
 Our MPC 2008 paper: Recounting the Rationals: Twice!
 History

 17 March 2010 — uploaded the cameraready version
 20 February 2010 — notification of acceptance
 14 December 2009 — submitted the paper for publication
Designing an Algorithmic Proof of the TwoSquares Theorem
[ CiteULike link ]