Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles

This paper focuses on how to use Pocklington’s criterion to produce efficient formal proof-objects for showing primality of large positive numbers. First, we describe a formal development of Pocklington’s criterion, done using the proof assistant . Then we present an algorithm in which computer algebra software is employed as oracle to the proof assistant to generate the necessary witnesses for applying the criterion. Finally, we discuss the implementation of this approach and tackle the proof of primality for some of the largest numbers expressible in .