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.