RISC Forum

Abstract:  In this talk, we will discuss the formalization of a library of mechanizations in PVS of different proofs of the infinitude of primes based on techniques from various areas of mathematics. It contains the formalizations of the proofs selected by (Erdös,) Aigner, and Ziegler in their famous “Proofs from THE BOOK,” including those based on Fermat numbers, Mersenne numbers and algebraic structures, Fürstenberg’s proof based on topological properties, and proofs based on the analysis of harmonic series. The availability of such a variety of proofs is helpful as a didactic tool to attract mathematicians of different areas to the application of interactive theorem provers. The presentation highlights the differences between the analytical proofs and the formalizations and the usefulness of features in the iterative proof assistant to discipline mechanization.