Abstract:
Automated Theorem Proving (ATP) and Automated Theorem Finding (ATF) are well-established areas of mathematical research, rich in methods, results, and open problems. Among the questions that remain especially significant today are how to measure the simplicity of a proof, how to assess its readability, and how to evaluate the interestingness of a theorem. Each of these questions matters in its own right. In this talk, however, I will consider them specifically in relation to automated theorem proving and theorem finding in geometry. I will suggest that these three questions can be viewed as closely connected, and that, when approached from this perspective, they offer a fruitful way of understanding both the process and the products of automated reasoning in geometry.
---
