A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

TL;DR

This paper compares four theorem provers to determine their effectiveness in formalizing a fundamental auction theory result, aiding the development of reliable, machine-checked proofs for auction design properties.

Contribution

It provides a qualitative comparison of Isabelle, Theorema, Mizar, and Hets/CASL/TPTP for formalizing auction theory, with practical recommendations for auction designers.

Findings

Isabelle and Mizar are most suitable for formalizing auction properties.

Formalization experience highlights strengths and limitations of each prover.

Recommendations guide future development of a comprehensive auction theory toolbox.

Abstract

Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.