Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

This question already has an answer here:

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?

share|cite|improve this question

marked as duplicate by Jack M, Will Jagy, M Turgeon, studiosus, Hakim Jun 1 '14 at 20:55

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

Presumably because it takes too long. Also, it wouldn't be any fun. Proving theorems is pointless if nobody understands the proofs. – Qiaochu Yuan Jun 1 '14 at 18:24
You mean why computers don't solve theorems or why people don't just solve theorems automatically – kingW3 Jun 1 '14 at 18:30
You have to know what you're looking for in order to have automatic theorem solvers do the work for you.. – Cameron Williams Jun 1 '14 at 18:30
This is really a different question from the linked "duplicate". – Nick Alger Jun 1 '14 at 22:55
"Either mathematics is too big for the human mind or the human mind is more than a machine." -- Kurt Gödel – Asaf Karagila Jun 2 '14 at 2:42

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.

share|cite|improve this answer
" informality of mathematical language and thinking is such that we can operate much faster ": so, there is an advantage sometimes in not being rigorous? – Quora Feans Jun 2 '14 at 12:06
"the informality of mathematical language and thinking is such that we can operate much faster than and see much farther" so, there is an advantage for the human mind since it's being informal sometimes? And, this non-rigorous thinking can be emulated by machines? – Quora Feans Jun 2 '14 at 12:26
"Computers aren't guided by creativity, intuition, metaphor like people are. ". this is true in 2015, not for ever. human intelligence has nothing magical and is nothing more than an algorithm that computers can simulate. It's obvious that mathematicians, not understanding that computers can be smart if the code has been written by smart people, are retarded. artificial intelligence is a math subject, and automatic theorem proving and discovering is one of the main artificial intelligence problem, as well as one of the main math problem. – reuns Jun 27 '15 at 21:17

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.
share|cite|improve this answer
I'm no expert, but are you using polynomial time legitimately? As your method doesn't terminate if a proof doesn't exist (i.e. it's not an algorithm), I don't think you can meaningfully say it's polynomial. – akroy Jun 1 '14 at 19:18
Notice the assumption: "If there is a finite proof (...)". – Marcin Łoś Jun 1 '14 at 20:36

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.

share|cite|improve this answer

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 :)

share|cite|improve this answer
For those of us who aren't going to read the linked paper, could you explain the gist of it? – blue Jun 1 '14 at 20:07
Cook's paper mainly discusses two things: the first is that the Boolean satisfiability problem is NP-complete. Hence it cannot be solved efficiently unles $\mathbf{P=NP}$. The second part is a method of measuring the complexity of proof procedures for the predicate calculus. @seaturtles Cook's paper is worth reading. – Jika Jun 1 '14 at 20:21

Not the answer you're looking for? Browse other questions tagged or ask your own question.