Does there exist an algorithm for deciding whether or not a specific mathematical assertion does or does not have a proof? The decision
problem is also known as the Entscheidungsproblem (which, not so coincidentally,
is German for "decision problem").
Using the concept of the Turing machine, Turing showed the answer to be negative for elementary number
theory. J. Robinson and Tarski showed the decision problem is undecidable
for arbitrary fields.
Church, A. "A Note on the Entscheidungsproblem." J. Symb. Logic1, 1936.Wolfram, S. A
New Kind of Science. Champaign, IL: Wolfram Media, pp. 1100
and 1136, 2002.