Reseña: A string of pearls: Proofs of Fermat’s little theorem
En la CPP12 (The Second International Conference on Certified Programs and Proofs), que comienza el 13 de diciembre, se presentará un trabajo de razonamiento formalizado en HOL4 titulado A string of pearls: Proofs of Fermat’s little theorem.
Sus autores son Hing-Lun Chan (de la Australian National University) y Michael Norrish (del Canberra Research Lab., NICTA).
Su resumen es
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.
El código conteniendo las demostraciones en HOL4 se encuentra aquí.
es una tautología syss 
es inconsistente.
syss 
es inconsistente.