Developing an Auction Theory Toolbox

Auctions allocate trillions of dollars in goods and services every year. Auction design can have significant consequences, but its practice outstrips theory. We aim at advancing auction theory with help from mechanised reasoning. To that end we are developing a toolbox of formalised representations of key facts of auction theory, which will allow auction designers to have relevant properties of their auctions machine-checked. In the starting phase of this effort, we are investigating the suitability of different mechanised reasoning systems (Isabelle, Theorema, and TPTP) for reproducing a key result of auction theory: Vickrey's celebrated 1961 theorem on the properties of second price auctions – the foundational result in modern auction theory. Based on our formalisation experience, we give tentative recommendations on what system to use for what purpose in auction theory, and outline further steps towards a complete auction theory toolbox.