[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
for the code). This has been done as part of our ForMaRE project (Formal
Mathematical Reasoning in Economics); see
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.
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
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and