1 Formulation of the Problem Checking Identities Is Computationally Intractable (NP-Hard), So Human Provers Will Be Always Needed

A recent article in the American Mathematical Monthly has shown that most combinatorial identities of the type described in Monthly problems can be solved by known identity checking algorithms. A natural question arises: are these algorithms always feasible, or the number of computational steps can be so big that application of these algorithms is sometimes not physically feasible? We prove that the problem of checking identities is NP-hard, and thus (unless NP=P), for every algorithm that solves it, there are cases in which this algorithm would require exponentially long running time and will thus be not feasible. This means that no matter how successful computers are in checking identities, human mathematicians will always be needed to check some of them. Keywords: computational complexity, NP-hard, checking identitie