Budget Imbalance Criteria for Auctions: A Formalized Theorem

TL;DR

This paper introduces a formalized theorem in auction theory that identifies conditions where the total payments in an auction are not constant, providing a new proof for the second-price Vickrey auction and formal verification in Isabelle/HOL.

Contribution

It presents a novel theorem on payment sums in auctions, with a formal proof in Isabelle/HOL and a simplified proof for the second-price Vickrey auction.

Findings

The sum of payments is not necessarily zero or constant under certain conditions.

A minimal set of bids where the sum varies is explicitly constructed.

The theorem is formalized and verified in Isabelle/HOL.

Abstract

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.