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

Select |


Chan, Hing-Lun; Norrish, Michael

Chan, Hing-Lun; Norrish, Michael


Conference Material

Certified Programs and Proofs

Kyoto, Japan


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.




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)