Entscheidungsproblem

Is there a program which can tell if a theorem is true or false?

This question was posed by David Hilbert in 1928, and addressed by three pioneers of computer science:

Alonzo Church (1936):

Invented lambda calculus
Created functional programming paradigm
Proved the Entscheidungsproblem has no solution using $\lambda$-calculus

Alan Turing (1936):
Invented the Turing machine
Also proved the Entscheidungsproblem has no solution

Kurt Gödel (1931):
Created general recursive functions
Proved the incompleteness theorems
Showed that any consistent formal system containing arithmetic has undecidable statements

→ All three showed (in different ways) that there is no universal algorithm that can decide the truth of all mathematical statements.