Skip navigation
Skip navigation

A string of pearls: Proofs of Fermat's Little Theorem

Chan, Hing Lun (Joseph); Norrish, Michael

Description

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.

CollectionsANU Research Publications
Date published: 2012
Type: Conference paper
URI: http://hdl.handle.net/1885/71302
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-642-35308-6_16

Download

File Description SizeFormat Image
01_Chan_A_string_of_pearls:_Proofs_of_2012.pdf371.83 kBAdobe PDF    Request a copy


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator