ICMS 2020 Session

Artificial Intelligence and Mathematical Software

Accepted Talk

Miroslav Olsak (University of Innsbruck)
GeoLogic: Graphical interactive theorem prover for Euclidean geometry
Abstract: Domain of mathematical logic in computers is dominated by automated theorem provers (ATP) and interactive theorem provers (ITP). Both of these are hard to access by AI from the human-immitation approach: ATPs often use human-unfriendly logical foundations while ITPs are meant for formalizing existing proofs rather th an problem solving. We aim to create a simple human-friendly logical system for mathematical problem solving. We picked the case study of Euclidean geometry as it can be easily visualized, has simple logic, and yet potentially offers many high-school problems of various difficulty levels. To make the environment user friendly, we abandoned strict logic required by ITPs, allowing to infer topological facts from pictures. We present our system for Euclidean geometry, together with a graphical application GeoLogic, similar to GeoGebra, which allows users to interactively study and prove properties about the geometrical setup. In the future, we would like to perform experiments with machine learning agents.