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.

Halting Problem

There’s no algorithm that can decide, in general, whether any given program will halt.
Equivalently, there’s no algorithm that decides the truth of all arithmetic statements. If you tried to “implement all of classical math” as a total, always-terminating program that answers every question, you’d run into a contradiction or non-termination.

Link to original