arXiv · 1412.0542
Budget Imbalance Criteria for Auctions: A Formalized Theorem
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.
Explore related subjects
Keep this discovery
Marco B. Caminati, Manfred Kerber, Colin Rowat. 2014-11-07. Budget Imbalance Criteria for Auctions: A Formalized Theorem. https://arxiv.org/abs/1412.0542
Cite the original work for its findings. Save a collection to share your selection of sources.