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

Hing Lun Chan; Michael Norrish

doi:10.1007/978-3-642-35308-6_16

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

Hing Lun Chan^*
, Michael Norrish

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

2 Citations (Scopus)

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.

Original language	English
Title of host publication	Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Pages	188-207
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-642-35308-6_16
Publication status	Published - 2012
Event	2nd International Conference on Certified Programs and Proofs, CPP 2012 - Kyoto, Japan Duration: 13 Dec 2012 → 15 Dec 2012

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7679 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Conference on Certified Programs and Proofs, CPP 2012
Country/Territory	Japan
City	Kyoto
Period	13/12/12 → 15/12/12

Access to Document

10.1007/978-3-642-35308-6_16

Cite this

Chan, H. L., & Norrish, M. (2012). A string of pearls: Proofs of Fermat's Little Theorem. In Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings (pp. 188-207). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7679 LNCS). https://doi.org/10.1007/978-3-642-35308-6_16

@inproceedings{395b85e96d7040da999446c13f1984d3,

title = "A string of pearls: Proofs of Fermat's Little Theorem",

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.",

author = "Chan, \{Hing Lun\} and Michael Norrish",

year = "2012",

doi = "10.1007/978-3-642-35308-6\_16",

language = "English",

isbn = "9783642353079",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "188--207",

booktitle = "Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings",

note = "2nd International Conference on Certified Programs and Proofs, CPP 2012 ; Conference date: 13-12-2012 Through 15-12-2012",

}

Chan, HL & Norrish, M 2012, A string of pearls: Proofs of Fermat's Little Theorem. in Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7679 LNCS, pp. 188-207, 2nd International Conference on Certified Programs and Proofs, CPP 2012, Kyoto, Japan, 13/12/12. https://doi.org/10.1007/978-3-642-35308-6_16

A string of pearls: Proofs of Fermat's Little Theorem. / Chan, Hing Lun; Norrish, Michael.
Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. 2012. p. 188-207 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7679 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

TY - GEN

T1 - A string of pearls

T2 - 2nd International Conference on Certified Programs and Proofs, CPP 2012

AU - Chan, Hing Lun

AU - Norrish, Michael

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84869772757

U2 - 10.1007/978-3-642-35308-6_16

DO - 10.1007/978-3-642-35308-6_16

M3 - Conference Paper

SN - 9783642353079

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 188

EP - 207

BT - Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings

Y2 - 13 December 2012 through 15 December 2012

ER -

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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this