This paper reports on an exploration of variants of Boolos' curious inference, using higher-order automated theorem provers (ATPs). Surprisingly, only a single shorthand notation had to be provided by hand. All higher-order lemmas required for obtaining short proof are automatically discovered by the ATPs. 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.

翻译：本文报告了对Boolos好奇推理的变体的探索,使用了较高顺序自动定理验证(ATPs) 。 令人惊讶的是,只需要手手写一个短手标记即可。 ATPs自动发现了获得短证据所需的所有较高顺序的 Lemmas。 鉴于本文件的意见和建议,Boolos关于加快证明长度的完整证明自动化示例和相关实例,现在似乎可以用于更高顺序的ATPs。