A String of Pearls: Proofs of Fermat's Little Theorem
Chan, Hing Lun ; Norrish, Michael
Journal of Formalized Reasoning, Tome 6 (2013), / Harvested from Journal of Formalized Reasoning
Link
Link

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 some of the direct number-theoretic approaches.

Publié le : 2013-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/3728 
@article{3728,
     title = {A String of Pearls: Proofs of Fermat's Little Theorem},
     journal = {Journal of Formalized Reasoning},
     volume = {6},
     year = {2013},
     doi = {10.6092/issn.1972-5787/3728},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/3728}
}

Chan, Hing Lun; Norrish, Michael. A String of Pearls: Proofs of Fermat's Little Theorem. Journal of Formalized Reasoning, Tome 6 (2013) . doi : 10.6092/issn.1972-5787/3728. http://gdmltest.u-ga.fr/item/3728/