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

TL;DR

This paper investigates Boolos' Curious Inference using higher-order automated theorem provers, demonstrating that ATPs can automatically discover necessary lemmas and find short proofs with minimal manual notation, advancing proof automation.

Contribution

It shows that higher-order ATPs can automatically discover lemmas and produce short proofs for Boolos' Curious Inference, reducing manual effort and enhancing proof automation capabilities.

Findings

ATP automatically discovers higher-order lemmas.

Short proofs are found with minimal manual notation.

Full proof automation appears achievable for similar problems.

Abstract

This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs.