PVS formalization of proofs of the infinitude of primes

Abstract

Este trabalho apresenta a mecanização de cinco abordagens diferentes para provar a infinitude dos números primos usando o assistente de prova Prototype Verification System (PVS). As técnicas de prova analítica abrangem várias áreas da matemática, como álgebra, teoria dos números, topologia e análise, e são baseadas nas elegantes provas selecionadas por Martin Aigner e Günter Ziegler no seu famoso livro "Proofs from THE BOOK". Nesse livro, são apresentadas seis diferentes provas da infinitude dos números primos, sendo a primeira a prova clássica de Euclides, que já está formalizada na biblioteca NASALib da NASA. Como resultado, nosso trabalho concentra-se na especificação e formalização das cinco provas restantes. A mecanização das provas faz uso de outras bibliotecas de PVS, como NASALib e prelude, que abstraem estruturas matemáticas como grupos, produtos Cartesianos, series e conjuntos, entre outras. No entanto, a importação de provas que assumem a infinitude dos números primos foram evitadas para prevenir circularidade. Além disso, o trabalho visa corrigir abusos notacionais e informalidades presentes nas provas do livro, se aproveitando do sistema de tipos do PVS, que é robusto o suficiente para revelar falhas nas formulações.