Construction of short formal proofs of primality

Hugo Elbers, CWI, Amsterdam, The Netherlands

Abstract:

In principle, it should be possible to transform any informal mathematical proof into a formal proof. But actually constructing a formal proof can be tedious and time-consuming. We will discuss how term rewriting and computer algebra systems can be used to get more succinct formal proofs. We will illustrate the use of computations in formal proofs by describing a method for constructing short formal proofs of primality.