Budget imbalance criteria for auctions: A formalized theorem

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

Colleges, School and Institutes


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.

Bibliographic note

ISBN 978-83-62582-58-7


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