@techreport{0c62b648c3894ac48359f085b129fdb7,
title = "A formal proof of Vickrey's theorem by blast, simp, and rule",
abstract = "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.",
keywords = "formal proof, mechanized reasoning, auction theory",
author = "Manfred Kerber and Christoph Lange and Colin Rowat",
year = "2014",
month = jan,
day = "5",
doi = "10.2139/ssrn.2376205",
language = "English",
series = "University of Birmingham, Department of Economics Working Paper Series",
publisher = "University of Birmingham",
number = "14-01 ",
pages = "1--13",
address = "United Kingdom",
type = "WorkingPaper",
institution = "University of Birmingham",
}