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.

为了发现并判断几何定理的有趣性，本文针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。