## 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 reproduced here

in common mathematical language, and are accompanied by an informal

discussion about the underlying ideas.

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 language | English |
---|---|

Pages | 35-44 |

Number of pages | 10 |

Publication status | Published - 1 Jul 2014 |

Event | Trends in Contemporary Computer Science - http://katmat.pb.bialystok.pl/pcm14/programy/program_detailed_v2.pdf, Białystok, Poland Duration: 1 Jul 2014 → 4 Jul 2014 |

### Conference

Conference | Trends in Contemporary Computer Science |
---|---|

Country/Territory | Poland |

City | Białystok |

Period | 1/07/14 → 4/07/14 |