A String of Pearls: Proofs of Fermat's Little Theorem
DOI:
https://doi.org/10.6092/issn.1972-5787/3728Keywords:
number theory, automated reasoningAbstract
We discuss mechanised proofs of Fermat's Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial ``necklace'' proof that has not been mechanised previously.What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for some of the direct number-theoretic approaches.
References
[AA08]
Andrea Asperti and Cristian Armentano. A page in number theory. Journal of Formal Reasoning, 1(1):1–23, 2008.
[ABR05]
Peter G. Anderson, Arthur T. Benjamin, and Jeremy A. Rouse. Combinatorial proofs of Fermat’s, Lucas’s, and Wilson’s Theorems. The American Mathematical Monthly, 112(3):266–
, 2005.
[AKS04]
Manindra Agrawal, Neeraj Kayal, and Nitin Saxena. PRIMES is in P. Annals of Mathematics, 160(2):781–793, 2004.
[Bur02]
Bob Burn. Fermat’s Little Theorem: Proofs that Fermat might have used. The Mathematical Gazette, 86(507):415–422, November 2002.
[CN12]
Hing-Lun Chan and Michael Norrish. A String of Pearls: Proofs of Fermat’s Little Theorem. In Chris Hawblitzel and Dale Miller, editors, Proceedings of Certified Programs and Proofs,
number 7679 in LNCS, pages 188–207. Springer, December 2012.
[Con08]
Keith Conrad. Group actions. http://www.math.uconn.edu/˜kconrad/blurbs/grouptheory/gpaction.pdf, 2008.
[Dic19]
Leonard Eugene Dickson. History of the Theory of Numbers: Volume 1: Divisibility and Primality. Carnegie Institution of Washington, 1919.
[Gol56]
Solomon W. Golomb. Combinatorial proof of Fermat’s “Little” Theorem. The American Mathematical Monthly, 63(10):718, 1956.
[Gun89]
Elsa. L. Gunter. Doing algebra in simple type theory. Technical Report MS-CIS-89-38, Department of Computer and Information Science, Moore School of Engineering,University of
Pennsylvania, June 1989.
[Har11]
John Harrison. HOL Light Tutorial (for version 2.20). Intel JF1-13, 2011. Section 18.2: Fermat’s Little Theorem.
[HE]
Benjamin V. Holt and Tyler J. Evans. A group action proof of Fermat’s Little Theorem. http://arxiv.org/abs/math/0508396.
[HGF06]
Joe Hurd, Mike Gordon, and Anthony Fox. Formalized elliptic curve cryptography. In High Confidence Software and Systems: HCSS 2006, April 2006.
[Hur01]
Joe Hurd. Predicate subtyping with predicate sets. In Richard J. Boulton and Paul B. Jackson, editors, 14th International Conference on Theorem Proving in Higher Order Logics: TPHOLs
, volume 2152 of Lecture Notes in Computer Science, pages 265–280. Springer, September 2001.
[Mah94]
Michael S. Mahoney. The Mathematical Career of Pierre de Fermat, 1601-1665. Princeton University Press, 1994.
[MOS06]
David Marshell, Edward Odell, and Michael Starbird. Number Theory Through Inquiry. Mathematical Association of America Textbooks, 2006. Chapter 4: Fermat’s Little Theorem and
Euler’s Theorem.
[Oos]
Martijn Oostdijk. Library pocklington.fermat. http://coq.inria.fr/pylons/contribs/files/Pocklington.fermat.html.
[Rou03]
Jeremy Rouse. Combinatorial proofs of congruences. Master’s thesis, Harvey Mudd College, 2003.
[Rus07]
David Russinoff. ACL2 Version 3.2 source: books/quadratic-reciprocity/fermat.lisp, 2007.
[San03]
Edward Sandifer. How Euler Did It: Fermat’s Little Theorem. MAA Online, November 2003.
[Smy86]
Chris J. Smyth. A coloring proof of a generalisation of Fermat’s Little Theorem. The American Mathematical Monthly, 93(6):469–471, 1986.
[SN08]
Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César Mu˜ noz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, volume 5170 of Lecture Notes in Computer Science, pages 28–32. Springer, 2008.
[Wei84]
André Weil. Number Theory: An Approach Through History from Hammurapi to Legendre. Birkhäuser Boston, 1984.
[Wik]
Wikipedia: Proofs of Fermat’s Little Theorem. http://en.wikipedia.org/wiki/Proofs_of_Fermat’s_little_theorem.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2013 Hing Lun Chan, Michael Norrish
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
