Budget imbalance criteria for auctions: A formalized theorem

Marco B. Caminati, Manfred Kerber, Colin Rowat

Research output: Contribution to conference (unpublished)Paperpeer-review


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 reproduced here
in common mathematical language, and are accompanied by an informal
discussion about the underlying ideas.
Original languageEnglish
Number of pages10
Publication statusPublished - 1 Jul 2014
EventTrends in Contemporary Computer Science - http://katmat.pb.bialystok.pl/pcm14/programy/program_detailed_v2.pdf, Białystok, Poland
Duration: 1 Jul 20144 Jul 2014


ConferenceTrends in Contemporary Computer Science

Bibliographical note

ISBN 978-83-62582-58-7


Dive into the research topics of 'Budget imbalance criteria for auctions: A formalized theorem'. Together they form a unique fingerprint.

Cite this