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

Great stuff, look forward to more of this.

A small random point: the definition

definition in_range ::
  "nat \<Rightarrow> nat \<Rightarrow> bool" where
  "in_range n i \<equiv> 1 \<le> i \<and> i \<le> n"

excludes 0. Unless you have some very good reason for starting at 1, I would
start at 0, which typically makes things smoother. For a start, you can just
write "i<n" instead of "in_range n i".


Am 31/10/2012 19:28, schrieb Christoph LANGE:
> 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 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.
> We began our formalisation by rewriting Maskin's proof in a more
> machine-friendly format
> (
>  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).
> 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.
> 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

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