Department Seminar

Tuesday, 21 April 2026, Sala Verde

10:30

Pierluigi Graziani (Università degli Studi di Urbino “Carlo Bo”)

Simplicity, Readability, and Interestingness: From Lemoine’s Geometrography to Wos’s 31st Problem

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.

Page on the University of Verona website
Link.