Are theorems in a mathematical theory effectively checkable? I wonder whether it is possible to effectively check whether some theorem of a mathematical theory (for example group theory) is provable from axioms of that theory. I know that in propositional logic and for example Hilbert's axiomatic system, it is possible to effectively check whether a theorem follows from it's premises/axioms. I also know that in 20th century there were efforts in mathematics to formalize mathematics (maybe so that it would be possible to effectively check whether a theorem follows from axioms of the theory?). Let's say I want to check by a computer whether a theorem follows from axioms of the group theory. Is it possible to check it by a computer? If so, how is it done?
 A: The answer depends crucially on what objects you are trying to study. First, we fix a theory, say that of Abelian Groups, Graphs, ZFC, etc. Then we can ask if there is a program meeting the following specification:

Given a sentence $\varphi$ in the theory of interest, output either
  
  
*
  
*a proof of $\varphi$ from the axioms, which tells us that every model satisfies $\varphi$
  
*a model $\mathfrak{M}$ which satisfies $\lnot \varphi$, showing that there is no proof of $\varphi$.

This problem is called the Decision Problem for $T$, since it decides if a formula is provable or not. We say that a program which does the above decides $T$. If such a program exists, then we say $T$ is decidable, and if no such program exists, then $T$ is undecidable.
As I said, trying to determine if a theory is decidable or not is a fairly delicate field of study. One thing you should know before starting is that efficient algorithms are fairly hard to come by. A lot of decision procedures, when they exist, are doubly exponential in runtime.

For convenience, here is a quick selection of some results in this area:


*

*The theory of Groups is undecidable

*The theory of Abelian Groups is decidable

*The theory of $(\mathbb{Q}, <)$ is decidable


*

*More generally, any theory admitting Quantifier Elimination is decidable


*The theory of $(\mathbb{N}, +)$ is decidable

*The theory of $(\mathbb{N}, \times)$ is decidable

*The theory of $(\mathbb{N}, +, \times)$ is undecidable


*

*More generally, any theory powerful enough to "do logic" inside of it is undecidable. This is basically the first incompleteness theorem


*The theory of Graphs is undecidable

*The theory of Graphs is decidable if we restrict attention to $\forall^*\exists^*$ formulas



Some useful references might be this wikipdedia page, as well as


*

*Rabin's "Decidable theories"

*Tarski, Mostowski, and Robinson's "Undecidable theories"

*Ferrante and Rackoff's "The computational complexity of logical theories"



I hope this helps ^_^
