Why isn't math completely solved by expert systems?

Question

Everything in math can be perfectly defined or formalized. And we could derive logical conclusions from that. However, mathematicians still use human natural language to solve their theorems.

Why isn't automatic proof checking or automated theorem solving the kernel of math?

Answer 1

Here, from wikipedia (I'm just a layman here, but I recall this from a lecture)

Gödel's incompleteness theorems are two theorems of mathematical logic that establish inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic.

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency.

Answer 2

Computers aren't guided by creativity, intuition, metaphor like people are. Humans wouldn't even bother to search through much of the boring uninteresting gobbledygook that exists in the space of all symbolic statements - most of this space is noise and nonsense that we efficiently ignore. Indeed, the informality of mathematical language and thinking is such that we can operate much faster than and see much farther than pure logical brute force searching can. Imagine solving a maze algorithmically, as opposed to being able to jump up and see over the labyrinth walls, or even climb over the walls when lucky. See also: Application of computers in higher mathematics.

Answer 3

My answer is in two parts:

• First part is a quote by Prof. Scott Aaronson: If P = NP, then the world would be a profoundly different place than we usually assume it to be. There would be no special value in "creative leaps," no fundamental gap between solving a problem and recognizing the solution once it's found. — Scott Aaronson, MIT

• Second part is the famous and well known paper by Stephen Cook: The Complexity of Theorem-Proving Procedues

I hope my answers helps you :)

Answer 4

Determining whether there exists a length-$k$ proof of a statement is a problem in the complexity class $NP$. So if there is a constructive proof that $P=NP$, that would also provide a polynomial time algorithm for proving theorems.

First you would try to find a proof of length $1$ in polynomial time, then try to find a proof of length $2$ in polynomial time, then length $3$, and so forth. If there is a finite proof then you will find it in polynomial time.

In case the statement is false, one should also be using the algorithm to try to prove the statement false simultaneously.

A few issues with this are

• Most mathematicians think $P \neq NP$,
• A future proof that $P=NP$ might be indirect based on contradiction, and not provide an actual algorithm,
• Even polynomial time algorithms can be prohibitively expensive - eg., an algorithm with running time $O(k^{100000})$ would be "polynomial time", but still completely intractible from a practical persective.
• There is an implicit dependence on the length of the shortest proof, which though fixed for any particular theorem, is still unbounded for theorems in general.
• In the extreme, if you try to prove a statement (or it's negation) that is undecidable your algorithm will keep running forever,
• Even if algorithms can prove or disprove statements, that still doesn't help in deciding what statements are "interesting". Humans will be needed to decide what statements to run the algorithm on.