A String of Pearls: Proofs of Fermat’s Little Theorem

Select |




Print


Chan, Hing-Lun; Norrish, Michael

Chan, Hing-Lun; Norrish, Michael


2012-10-24


Conference Material


Certified Programs and Proofs


Kyoto, Japan


188-207


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.


Springer


http://cpp12.kuis.kyoto-u.ac.jp/


nicta:6061


Chan, Hing-Lun; Norrish, Michael. A String of Pearls: Proofs of Fermat’s Little Theorem. In: Chris Hawblitzel and Dale Miller Editor, editor/s. Certified Programs and Proofs; Kyoto, Japan. Springer; 2012-10-24. 188-207.



Loading citation data...

Citation counts
(Requires subscription to view)