{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:28:29Z","timestamp":1772119709650,"version":"3.50.1"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T00:00:00Z","timestamp":1729468800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T00:00:00Z","timestamp":1729468800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000995","name":"Australian National University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000995","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Fermat\u2019s two squares theorem asserts that a prime one more than a multiple of 4 is a sum of two squares. There are many proofs of this gem in number theory, including a remarkable one-sentence proof by Don Zagier based on two involutions on a finite set built from such a prime. Applying the two involutions alternatively leads to an iterative algorithm to find the two squares for the prime. Moreover, a detailed analysis of the computation reveals that it is possible to jump through the iteration nodes, leading to a better hopping algorithm. Here is a formalisation of Zagier\u2019s proof, deriving the involutions using windmill patterns. Theories developed for the formal proof are used to establish the correctness of both algorithms.<\/jats:p>","DOI":"10.1007\/s10817-024-09708-3","type":"journal-article","created":{"date-parts":[[2024,10,21]],"date-time":"2024-10-21T12:03:49Z","timestamp":1729512229000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Windmills of the Minds: A Hopping Algorithm for Fermat\u2019s Two Squares Theorem"],"prefix":"10.1007","volume":"68","author":[{"given":"Hing Lun","family":"Chan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,21]]},"reference":[{"key":"9708_CR1","unstructured":"Arthan, R.: Mathematical Case Studies: Some Number Theory, Supplementary ProofPower Examples (2016). http:\/\/www.lemma-one.com\/ProofPower\/examples\/wrk074.pdf. Accessed 22 July 2024"},{"issue":"7","key":"9708_CR2","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BF02839014","volume":"4","author":"B Bagchi","year":"1999","unstructured":"Bagchi, B.: Fermat\u2019s two squares theorem revisited. Resonance 4(7), 59\u201367 (1999). https:\/\/doi.org\/10.1007\/BF02839014","journal-title":"Resonance"},{"key":"9708_CR3","doi-asserted-by":"publisher","unstructured":"Chan, H.L.: Windmills of the minds: an algorithm for Fermat\u2019s two squares theorem. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022, pp. 251\u2013264. ACM, New York (2022). https:\/\/doi.org\/10.1145\/3497775.3503673","DOI":"10.1145\/3497775.3503673"},{"key":"9708_CR4","doi-asserted-by":"publisher","unstructured":"Chapter 4: representing numbers as sums of two squares. In: Aigner, M., Ziegler, G.M. (eds.) Proofs from THE BOOK, 6th Edition, pp. 19\u201326. Springer, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-662-57265-8","DOI":"10.1007\/978-3-662-57265-8"},{"key":"9708_CR5","unstructured":"Dijkstra, E.W.: A derivation of a proof by D. Zagier. Manuscript EWD 1154 (1993). https:\/\/www.cs.utexas.edu\/~EWD\/ewd11xx\/EWD1154.PDF. Accessed 22 July 2024"},{"key":"9708_CR6","unstructured":"Dubach, G., Muehlboeck, F.: Formal verification of Zagier\u2019s one-sentence proof (2021). arXiv:2103.11389. Accessed 22 July 2024"},{"key":"9708_CR7","unstructured":"Harrison, J.: Representation of Primes $$\\equiv 1 ({\\rm mod} 4)$$ as Sum of $$2$$ Squares., Formalizing 100 Theorems in HOL Light (2010). https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/100\/two_squares.ml. Accessed 22 July 2024"},{"key":"9708_CR8","unstructured":"Heath-Brown, R.: Fermat\u2019s two squares theorem. Invariant 11, 3\u20135 (1984). In Oxford University Research Archive https:\/\/ora.ox.ac.uk\/objects\/uuid:c91a3bdd-7d8a-4bea-9734-28caf66f0914. Accessed 22 July 2024"},{"issue":"3","key":"9708_CR9","doi-asserted-by":"publisher","first-page":"243","DOI":"10.4169\/amer.math.monthly.120.03.243","volume":"120","author":"A Malter","year":"2013","unstructured":"Malter, A., Schleicher, D., Zagier, D.: New looks at old number theory. Am. Math. Monthly 120(3), 243\u2013264 (2013). https:\/\/doi.org\/10.4169\/amer.math.monthly.120.03.243","journal-title":"Am. Math. Monthly"},{"key":"9708_CR10","unstructured":"Narkawicz, A.: primes_sum_squares: THEORY, NASA PVS Library 6.0.9 (2012). https:\/\/github.com\/nasa\/pvslib\/blob\/master\/numbers\/primes_sum_squares.pvs. Accessed 22 July 2024"},{"key":"9708_CR11","unstructured":"Polster, B.: Why Was this Visual Proof Missed for 400 Years? (Fermat\u2019s Two Square Theorem), Mathologer (2020). YouTube: https:\/\/www.youtube.com\/watch?v=DjI1NICfjOk. Accessed 22 July 2024"},{"key":"9708_CR12","doi-asserted-by":"publisher","unstructured":"Poorten, A.: The Hermite-Serret Algorithm and $$12^{2} + 33^{2} = 1233$$. In: Lam, K.-Y., Shparlinski, I., Wang, H., Xing, C. (eds.) Cryptography and Computational Number Theory, pp. 129\u2013136. Birkh\u00e4user, Basel (2001). https:\/\/doi.org\/10.1007\/978-3-0348-8295-8_12","DOI":"10.1007\/978-3-0348-8295-8_12"},{"key":"9708_CR13","unstructured":"Riccardi, M.: theorem : NAT_5:23, Formalizing 100 Theorems in Mizar (2009). https:\/\/mizar.uwb.edu.pl\/100\/index.html. Accessed 22 July 2024"},{"issue":"3","key":"9708_CR14","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF02838970","volume":"2","author":"SA Shirali","year":"1997","unstructured":"Shirali, S.A.: On Fermat\u2019s two-square theorem. Resonance 2(3), 69\u201373 (1997). https:\/\/doi.org\/10.1007\/BF02838970","journal-title":"Resonance"},{"key":"9708_CR15","unstructured":"Shiu, P.: Involutions associated with sums of two squares. Publ. l\u2019Institut Math\u00e9matique 59, 18\u201339 (1996). https:\/\/eudml.org\/doc\/257994. Accessed 22 July 2024"},{"key":"9708_CR16","unstructured":"Spivak, A.: Winged Squares [in Russian]. Popular lectures in mathematics, 2006\u20132007 academic year, Lecture 15 (165) (2007). http:\/\/mmmf.msu.ru\/lect\/spivak\/zagir_!.pdf. Accessed 22 July 2024"},{"issue":"2","key":"9708_CR17","doi-asserted-by":"publisher","first-page":"125","DOI":"10.2307\/2323912","volume":"97","author":"S Wagon","year":"1990","unstructured":"Wagon, S.: Editor\u2019s corner: the Euclidean algorithm strikes again. Am. Math. Monthly 97(2), 125\u2013129 (1990). https:\/\/doi.org\/10.2307\/2323912","journal-title":"Am. Math. Monthly"},{"key":"9708_CR18","doi-asserted-by":"publisher","unstructured":"Zagier, D.: A one-sentence Proof that every prime $$p\\equiv 1 ({\\rm mod}\\,\\, 4)$$ is a sum of two squares. Am. Math. Monthly 97(2), 144 (1990). https:\/\/doi.org\/10.2307\/2323918","DOI":"10.2307\/2323918"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09708-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09708-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09708-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,14]],"date-time":"2024-12-14T02:06:57Z","timestamp":1734142017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09708-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,21]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["9708"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09708-3","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-4428033\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,21]]},"assertion":[{"value":"16 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 July 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The author declares no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"22"}}