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

Date

2012

Authors

Chan, Hing Lun (Joseph)
Norrish, Michael

Journal Title

Journal ISSN

Volume Title

Publisher

Conference Organising Committee

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.

Description

Keywords

Keywords: Artificial intelligence; Theorem proving

Citation

Source

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

Type

Conference paper

Book Title

Entity type

Access Statement

License Rights

DOI

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

Restricted until

2037-12-31