The structure of mathematical proof trees

Abstract:  With the computerization of formal mathematics, it has become possible to automatically prove theorems by systemically applying all inference rules to all axioms. However, most mathematical theorems today are proven through the use of human intuition. Can we characterize the heuristic that human theorem provers use to search through the space of possible proofs to reach the desired theorem? Given a formal system, there may be a massive number of different proof structures that prove a given theorem. By analyzing the particular proof structures that people have used and formalized into the theorem proving language Coq, we may be able to generate insight into the subclass of possible proof trees that humans tend to explore. Our goal is to use insights of the structure of human-generated proofs to better direct automatic proof search.