Budget Imbalance Criteria for Auctions: A Formalized Theorem
This is a theoretical contribution to auction theory, but it is incremental as it formalizes known results.
The paper presents a theorem specifying conditions under which the sum of bidder payments in auctions is not constant, with a formal proof in Isabelle/HOL. It applies to Vickrey auctions and provides a novel proof for a basic result.
We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.