An introduction to mechanized reasoning
向经济学家介绍机械化推理（用计算机验证证明和发现新定理），重点阐述其在社会选择理论和拍卖理论中的应用，并以Vickrey第二价格拍卖定理的证明为例展示实践。
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.