Who Finds the Short Proof? An Exploration of variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers

We report on an exploration of variants of Boolos' curious inference using higher-order automated theorem provers (ATPs). Surprisingly, only a single shorthand notation still had to be provided by hand. All higher-order lemmas required for obtaining short proof are automatically discovered by the computer. Given the observations and suggestions in this paper, full proof automation of Boolos' example on the speedup of proof lengths, and related examples, now seems to be within reach for higher-order ATPs.