21122002 not mine but quotation

Yet, in principle, computers cannot be asked to discover proofs, except in very restricted areas of mathematics–such as elementary Euclidean geometry–where the set of theorems happens to be recursive, as was proved by Tarski.

… the prime number theorem was first suggested as the result of extensive hand calculations on the prime numbers up to 3,000,000 by the Swiss mathematician Leonhard Euler (1707-83), a process that would have been greatly facilitated by the availability of a modern computer.

Thus Godel was able to assert that the set of theorems of mathematics is recursively enumerable, and, more recently, the American linguist Noam Chomsky (b. 1928) could say that the set of grammatical sentences of a natural language, such as English, is recursively enumerable.

Godel’s incompleteness theorem is that the consistency of mathematics can be proved only in a language which is stronger than the language of mathematics itself. Yet, formalism is not dead- …

— Encyclopædia Britannica

.

.

2022.10.13 Thursday ACHK