AN INDUCTIVE APPROACH TO FORMALIZING NOTIONS OF NUMBER THEORY PROOFS
Thomas Marthedal Rasmussen · 2001
Abstract. In certain proofs of theorems of, e.g., number theory and the algebra of finite fields, one-to-one correspondences and the “pairing off” of elements often play an important role. In textbook proofs these con-cepts are often not made precise but if one wants to develop a rigorous formalization they have to be. We have, using an inductive approach, developed constructs for handling these concepts. We illustrate their usefulness by considering formalizations of Euler-Fermat’s and Wilson’s Theorems. The formalizations have been mechanized in Isabelle/HOL, making a comparison with other approaches possible. 1