An Introduction to Mechanized Reasoning

TL;DR

This paper introduces mechanized reasoning to economists, explaining its techniques, applications in social choice and auction theory, and demonstrating its practical use through a proof of Vickrey's theorem.

Contribution

It provides the first comprehensive presentation of mechanized reasoning techniques and their application to economic problems for an economics audience.

Findings

Mechanized reasoning techniques are effective in verifying economic theorems.

Applied to social choice and auction theory, demonstrating practical utility.

A detailed proof of Vickrey's theorem showcases the approach's effectiveness.

Abstract

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.