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 the direct number-theoretic approach. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Chan, H. L., & Norrish, M. (2012). A string of pearls: Proofs of Fermat’s Little Theorem. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 188–207). https://doi.org/10.1007/978-3-642-35308-6_16
Mendeley helps you to discover research relevant for your work.