Formalizing a Key Theorem from Auction Theory using the Theorema System
In this talk we present a complete formalization of a key result in auction
theory, namely Vickrey's Theorem on second-price auctions. In a second-price
auction, one of the bidders with the highest bid wins, but instead of having to
pay his/her own bid he/she must pay the maximum of all remaining bids, which
is essentially how also eBay determines the winner's price to pay. Vickrey's
theorem states that in a second-price auction it is a weakly dominant strategy
to bid exactly as much as one values the good, i.e. it does not make sense
to bid higher or lower than the actual valuation no matter what the others
do.
After defining the required concepts from theoretical economics (bids,
valuations, winning strategy, weak dominance, etc.) we give a full formal proof
of the theorem. The emphasis in this presentation lies on the demonstration of
Theorema's capabilities as a mathematical assistant system, we want to stress
the following aspects in particular:
o) The power of the Theorema language to formulate mathematical content in
a concise manner still preserving the elegance of mathematical notation that
one is used from standard mathematical documents written in e.g. LaTeX.
o) The capabilities to structure bigger blocks of mathematics into smaller
theories and subtheories with the possibility of easy re-use through
theory import.
o) The power of the automated proving methods implemented in the Theorema
system, in particular of specialized inference rules for built-in language
constructs of the Theorema language, e.g. the maximum-construct.
o) The attractivity of the resulting formalization for the working
mathematician. The formalization document as well as the automatically
generated proofs are delivered in a form that resembles the way how
mathematicians are used to read and write their documents.
This talk is a follow-up to a paper presented at the CICM'2013 conference,
where several proof assistants were compared and assessed based on the
formalization of Vickrey's theorem. Although Theorema 2.0 was part of
this comparison, the system was not able to give any of the proofs due to the
incomplete implementation at that time. The assessment was given based on the
formalization input in version 2.0 in combination with proof experience in a
similar formalization carried out in a predecessor version. In this
presentation, the entire formalization including the proofs is done in the
Theorema 2.0 system.