I have a joint paper with my supervisor, on combinatoric and group-theoretic proofs of Fermat’s Little Theorem in HOL4.
It all started when I came across the Necklace proof of Fermat’s Little Theorem, which is different from the textbook number-theoretic proof. The number-theoretic proof is also standard in automatic theorem provers, e.g. it is a worked example in HOL Light Tutorial. I was wondering how to put a combinatoric proof in HOL4.
It turns out that it is just a matter of counting with sets. There are tricks to set up bijections to establish the sizes of sets. Digging deeper, I find that there is a kind of symmetry underlying the bijections, and I am surprised to find group action is involved. Eventually I use the Orbit-Stabilizer Theorem to prove the Necklace Theorem, thereby proving Fermat’s Little Theorem.
At the end, we did several proofs of the theorem in HOL4, made a comparison, and gave the paper this title: “A String of Pearls: Proofs of Fermat’s Little Theorem”. The paper was accepted by CPP 2012, and I gave a talk at the conference held in Kyoto this December.
During this process, I have build up a library of group theory in HOL4. This should help my further work in finite fields.