Idea
Hilbert’s Entsheidungsproblem is a decision problem posed by Hilbert in 1928 for the provability of statements first-order logic. It was shown by Church and Turing to be undecidable.
Problem statement
Is there an algorithm which when fed any statement in the formal language of first-order arithmetic, decides whether or not the statement is provable from Peano’s axioms for arithmetic, using the usual rules of first-order logic?
Remarks
“Entsheidungsproblem” is German for “decision problem”.