Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry
Pedro Quaresma, Pierluigi Graziani, Stefano M. Nicoletti
TL;DR
This work examines the problem of what properties enable automated reasoning systems to generate new and interesting geometric theorems rather than merely prove conjectures. It surveys four ATG paradigms—Inductive, Generative, Manipulative, and Deductive—and presents a common generation–filtering framework, emphasizing the role of run-time filters and metrics to identify interesting results. A key result is an undecidability proof via Rice's theorem, which implies that deterministic determination of theorem interestingness is not possible, motivating heuristic and empirical approaches. To address this, the authors propose empirical expert surveys to define and validate what constitutes interesting geometry theorems and outline a plan to integrate these findings into theorem-proving/finding systems, including existing implementations like JGEx and GeoGebra Discovery and the OGPCP-GDDM project.
Abstract
The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "wheat", new and interesting facts, is much harder, but is also being addressed by different authors using different approaches. In this paper we will focus on geometry. We present and discuss different approaches for the automatic discovery of geometric theorems (and properties), and different metrics to find the interesting theorems among all those that were generated. After this description we will introduce the first result of this article: an undecidability result proving that having an algorithmic procedure that decides for every possible Turing Machine that produces theorems, whether it is able to produce also interesting theorems, is an undecidable problem. Consequently, we will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task, at best a task to be addressed by program based in an algorithm guided by heuristics criteria. Therefore, as a human, to satisfy this task two things are necessary: an expert survey that sheds light on what a theorem prover/finder of interesting geometric theorems is, and - to enable this analysis - other surveys that clarify metrics and approaches related to the interestingness of geometric theorems. In the conclusion of this article we will introduce the structure of two of these surveys - the second result of this article - and we will discuss some future work.