Theorem discovery, with the help of computer, presents at least two steps of challenges. The first concerns how to come up with reasonable conjectures automatically. This raises further challenges, such as how to represent these conjectures within the computers, what is the yardstick for reasonableness, etc. The second concerns how to prove or negate the conjectures automatically. However theorem proving, even for the best of human beings, is still an intelligence-demanding endeavor and sometimes even a nightmare....[ Read more ]

Theorem discovery, with the help of computer, presents at least two steps of challenges. The first concerns how to come up with reasonable conjectures automatically. This raises further challenges, such as how to represent these conjectures within the computers, what is the yardstick for reasonableness, etc. The second concerns how to prove or negate the conjectures automatically. However theorem proving, even for the best of human beings, is still an intelligence-demanding endeavor and sometimes even a nightmare.

Our starting point however, is a basic form of proof, namely proof by induction. The heuristic behind is extremely straightforward: We first formulate the problem domain in a proper language, say logic or other formal languages. We then enumerate the sentences (within certain length limit) in the underlying language that describe propositions in the domain. After that, we use a computer program to verify through these sentences to find those true in base cases, that is, where the problem size is small. The remaining sentences serves as conjectures, which can be extended, one way or other, to inductive cases.

It turns out that this methodology has been quite effective since we adopted it in economic theory. In particular, some of our programs on game theory have returned theorems that shed lights on the understanding of basic game forms such as zero-sum game, potential game and super-modular game. Some of them have helped us prove some Nobel Prize winning theorems such as Arrow's impossibility theorem and Sen’s theorem on voting functions and discover new theorems that better characterize key concepts in social choice theory. Others also have helped us prove Nobel Prize winning theorems such as Maskin's theorem on Nash implementation as well as Gibbard-Satterthwaite theorem on dominant strategy implementation. These proofs themselves also provide insights on discovering similar theorems.

This thesis reports all attempts that we have conducted in the past few years, in support of the general methodology of theorem discovery.