A formal proof of Vickrey's theorem by blast, simp, and rule

Manfred Kerber, Christoph Lange, Colin Rowat

Research output: Working paper/PreprintDiscussion paper


Formal methods use computers to verify proofs or even discover new theorems. Interest in applying formal methods to problems in economics has increased in the past decade, but - to date - none of this work has been published in economics journals. This paper applies formal methods to a familiar environment - Vickrey's theorem on second-price auctions - and provides, as background, an introduction to formal methods.
Original languageEnglish
PublisherUniversity of Birmingham
Number of pages13
Publication statusPublished - 5 Jan 2014

Publication series

NameUniversity of Birmingham, Department of Economics Working Paper Series


  • formal proof
  • mechanized reasoning
  • auction theory


Dive into the research topics of 'A formal proof of Vickrey's theorem by blast, simp, and rule'. Together they form a unique fingerprint.

Cite this