Trustworthy Systems

A string of pearls: Proofs of fermat’s little theorem

Authors

Hing-Lun Chan and Michael Norrish

NICTA, Sydney, Australia
UNSW, Australia

Abstract

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.

BibTeX Entry

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

Download