Auctions are more interesting than one may think: There is not always a single good, for which participants give increasing bids, and the highest bidder wins. There are more complex auctions out there; think of governments auctioning their radio frequency spectrum to mobile phone network operators. An operator may be interested in bidding for a low-frequency spectrum as well as a high-frequency one, as they complement each other like a left shoe and a right shoe. Such auctions are called combinatorial auctions.
Goals of an auction designer include:
But how can you tell, with absolute certainty, that a certain auction mechanism generally has certain properties?
Our approach is to describe auctions mathematically, to state theorems about them, and prove them – using computer support (interactive/automated theorem provers).
In a second price auction, each participant makes one bid without knowing the others' bids. The highest bidder wins, but only pays the price of the second highest bid. This is a simplification of what eBay does.
In such an auction, the best strategy for every individual participant is to simply bid his or her valuation; e.g. if I believe the painting being auctioned is worth £1,000 this is my bid. There is no need for tactic over- or under-bidding. This is Vickrey's Theorem, established on paper in 1961, but only machine-verified in 2012.
This project is suitable for BSc students interested in logics, as well as for MSc students.
This research takes place in the context of the project "Formalised Mathematical Reasoning in Economics" (ForMaRE). At the University of Birmingham, this also involves Dr Manfred Kerber from computer science, who is offering related projects, and Dr Colin Rowat from economics. More concretely, this research takes place within our plan to build an Auction Theory Toolbox (description) in close contact with people who design real million-$ in-the-field auctions tailored to the things to be auctioned, such as internet domains (who will get the .book domain: Google or Amazon?), treasure bill yields, etc.
Manfred Kerber offers a related project on matching problems. If you are interested in different problems in economics, we may also provide guidance. Please study our slides “An economist's guide to mechanized reasoning or My computer just proved 84 impossibility theorems” (invited lecture at the 2012 Initiative for Computational Economics summer school).
Please contact Christoph Lange if interested; see my homepage for contact information.