# [isabelle] Started auction theory toolbox; announcement, next steps, and questions

Dear Isabelle community,

`We are pleased to announce our first step towards building an auction
``theory toolbox: a complete formalisation of William Vickrey's 1961
``theorem on second price auctions (see
``http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/Vickrey.thy
``for the code). This has been done as part of our ForMaRE project (Formal
``Mathematical Reasoning in Economics); see
``http://cs.bham.ac.uk/research/projects/formare/.
`

`This mail outlines our result and our next steps. We'd also like to ask
``you for some Isabelle-specific advice on our next steps, and to share
``and discuss the experiences we've had.
`
AUCTION THEORY

`In second price (or Vickrey) auctions, bidders submit sealed bids; the
``highest bidder wins, and pays the highest bid of the _remaining_ bids;
``the losers pay nothing. (See
``http://en.wikipedia.org/wiki/Vickrey_auction for more information,
``including a discussion of variants used by eBay, Google and Yahoo!.)
``Vickrey proved that 'truth-telling' (i.e. submitting a bid equal to
``one's actual valuation of the good) was a weakly dominant strategy. This
``means that no bidder could do strictly better by bidding above or below
``its valuation _whatever_ the other bidders did. Thus, the auction is
``also efficient, awarding the item to the bidder with the highest valuation.
`

`Vickrey was awarded Economics' Nobel prize in 1996 for his work. High
``level versions of his theorem, and 12 others, were collected in Eric
``Maskin's 2004 review of Paul Milgrom's influential book on auction
``theory ("The unity of auction theory: Milgrom’s master class", Journal
``of Economic Literature, 42(4), pp. 1102–1115). Maskin himself won the
``Nobel in 2007.
`
OUR RESULT AND PLANS

`We began our formalisation by rewriting Maskin's proof in a more
``machine-friendly format
``(http://cs.bham.ac.uk/research/projects/formare/code/auction-theory/vickrey-paper.pdf).
`` As the proof is case based, this allowed a simple translation to Isabelle.
`

`We plan to formalise the other theorems in Maskin's paper, adding them
``to an auction theory toolbox, with the eventual goal of proving new
``theorems about old and new types of auctions.
`

`This will require both re-arrangements of our current formalisation into
``multiple theories, and generalisations. For example, we now model
``bidders as an integer range 1,…,n, and their bids as an n-vector of real
``numbers (actually, as a function from 1,…,n to reals). However,
``Vickrey's theorem does not assume any _order_ among the participants. It
``is thus sufficient to treat them as a set, but it must be possible to
``remove elements from such a set (which we currently do by skipping
``components of a vector).
`
QUESTIONS FOR ISABELLE COMMUNITY

`We would like to contribute our formalisation to the AFP, but are unsure
``about the procedure: once accepted and published, can we submit updates?
``We could imagine submitting this formalisation soon (as it is
``self-contained and covers a relevant field), but still we are planning
``to evolve and improve it.
`

`As this was our first major Isabelle formalisation, we may have got a
``lot of things wrong. We would be grateful if any of you were able to
``look into the source and tell us of any "anti-patterns" we shouldn't
``use. I will also follow up on this mail with a number of mails asking
``specific questions on how certain things in Isabelle work, and with some
``jEdit bug reports.
`
COMMENTS ON ISABELLE EXPERIENCE

`Overall, we have been quite satisfied with how Isabelle works so far,
``but we are also trying to take the perspective of our end users
``(economists with little computer science background), who may find it
``harder to use. Here are some preliminary notes (some of which may be
``based on wrong assumptions):
`
* jEdit gives good feedback about syntax errors and certain semantic errors.

`* When developing the structure of a proof, "show ?thesis sorry"
``placeholders proved useful.
`* sledgehammer is very useful for finding justifications for proof steps.
* Local renamings with "let" proved useful in complex proofs.

`* It would be nice to be able to introduce proper types (not just
``type_synonyms) for things such as non-negative real vectors.
``* In statements such as "!x. p x --> q x" it is tedious (and always the
``same) to break their structure down to a level where the actually
``interesting work starts.
`
Cheers, and thanks in advance for your feedback,
Christoph & Colin & Manfred
--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
2–5 April 2013, Exeter, UK. Deadlines 10 Dec (stage 1), 14 Jan (st. 2)
http://cs.bham.ac.uk/research/projects/formare/events/aisb2013/

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*