An introduction to mechanized reasoning

Manfred Kerber, Christoph Lange-Bever, Colin Rowat

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)
210 Downloads (Pure)


Mechanized reasoning uses computers to verify proofs and to help discover new theorems. Computer scientists have applied mechanized reasoning to economic problems but–to date–this work has not yet been properly presented in economics journals. We introduce mechanized reasoning to economists in three ways. First, we introduce mechanized reasoning in general, describing both the techniques and their successful applications. Second, we explain how mechanized reasoning has been applied to economic problems, concentrating on the two domains that have attracted the most attention: social choice theory and auction theory. Finally, we present a detailed example of mechanized reasoning in practice by means of a proof of Vickrey’s familiar theorem on second-price auctions.
Original languageEnglish
Pages (from-to)26-39
Number of pages14
JournalJournal of Mathematical Economics
Early online date18 Jul 2016
Publication statusPublished - Oct 2016


  • mechanized reasoning
  • formal methods
  • social choice theory
  • auction theory


Dive into the research topics of 'An introduction to mechanized reasoning'. Together they form a unique fingerprint.

Cite this