G?delís Theorem (1931): Whatever finite sets of axioms and inference
rules we choose, there will remain true mathematical statements that
cannot be proven (derived from those axioms by those inference rules).
This is true even for such a limited part of mathematics as the arithmetic
of positive integers, where the only operations we consider are + and ?.
So, forget any dreams about constructing a universal ďTruth MachineĒ
- a machine (program) that would find all the true mathematical