A String of Pearls: Proofs of Fermat's Little Theorem
Hing Lun Chan (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2012-10-30
TIME: 14:00:00 - 14:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
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
Reference: http://www.nicta.com.au/pub?doc=6061
