Chan, Hing Lun (Joseph)Norrish, Michael2015-12-13December 19783642353079http://hdl.handle.net/1885/71302We 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.Keywords: Artificial intelligence; Theorem proving201210.1007/978-3-642-35308-6_162016-02-24