Alonzo Church, one of the great logicians of the 20th century, published a proof to the Entscheidungsproblem, known as Church’s Theorem:
No single algorithm can determine whether a statement of number theory is a theorem or not.
The statement is fairly simple, I think. You can write a computer program, which, when fed a mathematical statement, would test it arbitrarily to see whether it held in random test cases and then proceeded to attempt to determine its theorem-hood through a variety of preprogrammed “strategies.” It might work in a lot of cases. However, you cannot write a computer program which follows the same procedure every time to determine whether something was a theorem or not, according to Alonzo Church. Read the rest of this entry »