Resumo
The formalization of mathematics in practice relies heavily on proof assistants and automatic theorem provers, therefore we studied what are the state of the art proof assitants and their limitations to understand what are the main challenges in making formalized mathematics common practice among mathematicians. We found out that curretly the two major dificulties in formalizing mathematics with proof assistants are due to steep learning curves in how to use these tools and due to a wide gap between the notation employed in these proof assistants and the currently used mathematical notation. We also developed a C++ library to develop proof assistants with great notational flexibility.
Todos os trabalhos são de acesso livre, sendo que a detenção dos direitos concedidos aos trabalhos são de propriedade da Revista dos Trabalhos de Iniciação Científica da UNICAMP.