Open AccessFormalization of mathematics through proof assistants
Author(s) -
Henrique Yuji Rossetti Ihe,
Walter Carnielli
Publication year - 2019
Publication title -
revista dos trabalhos de iniciação científica da unicamp
Language(s) - English
Resource type - Journals
ISSN - 2596-1969
DOI - 10.20396/revpibic262018600
Subject(s) - notation , computer assisted proof , mathematical practice , proof assistant , proof of concept , structural proof theory , computer science , flexibility (engineering) , mathematical notation , calculus (dental) , proof theory , programming language , automated theorem proving , mathematics education , mathematics , mathematical proof , arithmetic , medicine , statistics , geometry , dentistry , operating system
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.