AUTOMATED VERIFICATION OF INFORMAL PROOFS FROM HIGH SCHOOL GEOMETRY

Abstract

Computer assisted theorem proving has been gaining a lot of attention over the past couple of decades. Programs used for such tasks have steadily been improving, gaining in flexibility and capability to tackle an ever-increasing set of more complex theorems. While the development of these software tools has been guided by the notion of user-friendly interfaces and ease of use, they have not gained much popularity in a broad population which includes high school and university students. The program we present in this paper aims to bridge this gap as it is specifically tailored for this audience. It allows for automated checking of informal proofs that are often found in high school geometry curricula and generates formal, computer verifiable proof along with a proof written in Serbian. We demonstrate its use on a handful of proofs from high school textbooks. The program is very simple to use and does not require a user to have any prior experience with automated theorem proving softwarе. In addition to being a useful educational tool, the program could also be used by mathematicians for producing new original proofs.