NICTA, Sydney, Australia
UNSW, Australia
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.
@inproceedings{Chan_Norrish_12, month = oct, paperurl = {https://trustworthy.systems/publications/nicta_full_text/6061.pdf}, publisher = {Springer}, booktitle = {International Conference on Certified Programs and Proofs}, editor = {{Chris Hawblitzel and Dale Miller}}, author = {Chan, Hing-Lun and Norrish, Michael}, year = {2012}, pages = {188--207}, title = {A String of Pearls: Proofs of Fermat’s Little Theorem}, address = {Kyoto, Japan} }