Auction Theory Toolbox (ATT)

This is an output of the ForMaRE research project. We particularly focus on

Both will be detailed below.

Proving theorems about static single-good auctions

Our formalisation is guided by Eric Maskin's 2004 review article “The unity of auction theory: Milgrom's master class” (Journal of Economic Literature 42.4, p. 1102–1115). As this article makes rather high-level statements, we have elaborated them to more detail on paper.

We have used different languages for the formalisation. The table below lists the current state of formalising the propositions given in Maskin's review article. For the research background and first results, please see our paper “A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory” (in: Conference on Intelligent Computer Mathematics, 2013).

Further contributions are highly welcome; this includes

  • formalisations of propositions not yet covered
  • re-formalisations in new languages
  • improvements to existing formalisations

For any questions, please contact us via formare-discuss@cs.bham.ac.uk. (You need to subscribe first.)

Downloadable files are linked below. If you would like to contribute to the latest developments, please have a look at our GitHub repository.

The table below shows the following information:

  • Proposition: the number of the respective Proposition in Maskin's review article and the original authors of the theorem
  • Elaboration: a link to the elaborated paper version
  • For each formalisation: its authors. The formalisations of all theorems can be accessed via the column header showing the name of the respective language.
Proposition (Maskin) Elaboration CASL Isabelle Mizar Theorema
1 (Vickrey) elaboration (Rowat/Kerber/Lange) Lange/Mossakowski Lange/Wenzel/Kerber Caminati Windsteiger
2 (Green/Laffont/Holmström/Maskin)
3 (Green/Laffont/Maskin)
4 (d'Aspremont/Gérard-Varet)
5 (Laffont/Maskin/Myerson/Satterthwaite)
6 (Vickrey/Myerson/Riley/Samuelson)
7 (Myerson/Riley/Samuelson)
8 (Vickrey)
9 (Vickrey/Riley/Samuelson/Myerson)
10 (Riley/Samuelson/Myerson)
11 (Holt/Maskin/Riley/Matthews)
12 (Maskin/Jehiel/Moldovanu)
13 (Milgrom/Weber)

Soundness of complex auctions; verified auction software

In this effort, we prove that auctions are soundly specified, i.e. assign a unique, well-defined outcome to each well-formed bid input. This is easier to prove than certain other properties of auctions studied above, but we deal with more complex auctions, at the moment with static combinatorial auctions. Once the soundness of an auction has been proved, we generate verified software code from the formalisation. For details and first results, please see our paper “Proving soundness of combinatorial Vickrey auctions and generating verified executable code” (2013).

Our work is guided by some of the chapters of the following book: Peter Cramton, Yoav Shoham, and Richard Steinberg (2006). Combinatorial Auctions. MIT Press. ISBN 0-262-03342-9. Here, we focus on Isabelle as a formalisation tool.

Topic (Chapter) Elaboration Isabelle
Vickrey auction (1) see section 4 (Rowat/Kerber/Lange) Lange/Caminati (in progress)

Unless otherwise stated, the sources of the Auction Theory Toolbox are dually licenced under the ISC License and the Creative Commons Attribution 3.0 License. With a dual licence for source code and creative works, we follow the model of the Mizar Mathematical Library, as suggested by Alama, Kohlhase, Naumowicz, Rudnicki, Urban and Mamane.

This page was last modified on 04 September 2013.