I don't know if there exist computer programs working on its own, trying to find and prove theorems, delivering proofs and go on searching for new theorems. But if (when) there are such programs, efficient or not, would it be a milestone in the development of mathematics? Or would lack of intuition and heuristic create nothing more than lists of random theorems, not much more important than lists of random numbers?

Isn't mathematics more than pseudo random started recursive processes? How important is human desire for the development of important and realistic mathematics?


closed as unclear what you're asking by user64687, Eric Stucky, Namaste, Emily, drhab Jan 19 '15 at 14:51

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ This question is most likely going to be closed. I asked a similar one about artificial intelligence proving crazy math. I was told "there is a difference between a paint sprayer and an artist". Link: math.stackexchange.com/questions/978764/… $\endgroup$ – layman Jan 19 '15 at 13:31
  • $\begingroup$ I think it would be interesting if it had success, even if we couldn't figure out the actual math behind the proof. In the extreme case, you might imagine a brute force program finding an inconsistency of Peano arithmetic, ZFC or related systems. However, I doubt such a search would be successful in our lifetime, since I'd expect formalized proofs of nontrivial theorems to be extremely long - however, I have never seen particular estimates in this direction (does anyone else?) $\endgroup$ – Hanno Jan 19 '15 at 13:44
  • $\begingroup$ @Hanno: I think computer aided proving is important already and will become more important in the future, but my question is about the "form" of real mathematics. Is it mathematics at all, if it isn't formed by humans? Or at least get feedback from human desire... $\endgroup$ – Lehs Jan 20 '15 at 7:39
  • $\begingroup$ You might read about automated theorem proving on Wikipedia and you might also find some interesting pointers in that article. $\endgroup$ – Martin Sleziak Jan 20 '15 at 11:47
  • $\begingroup$ I also found this fact interesting: In 1959, Wang wrote on an IBM704 computer a program that in only 9 minutes mechanically proved several hundred mathematical logic theorems in Whitehead and Russell's Principia Mathematica. Source: en.wikipedia.org/wiki/Hao_Wang_%28academic%29 $\endgroup$ – Martin Sleziak Jan 20 '15 at 11:52

The fact that such a program exists is actually an important concept, in fields such as foundations of mathematics, computability theory and complexity theory.

Foundations: When you want to reason about mathematics in general, you can either fix an axiomatic system, such as ZF (or a variant like ZFC), or take a general one. However, when you consider a general axiomatic system, you usually require that this system is recursively enumerable, which means precisely that there exists a program that enumerates all proofs and theorems in your given system. This is for instance required in Gödel's incompleteness theorems. In particular it is true in the case of ZF(C), which is the system most commonly used by mathematicians.

Computability: When studying Turing machines, you might be interested in proving termination. The fact that there is a particular Turing machine that enumerates proofs in your system (like ZFC) shows that you will not be able to always find a proof that tells you if your algorithm terminates. For instance if you take an machine that looks for a contradiction in ZFC, and if ZFC is coherent, your machine won't terminate but you cannot prove it in ZFC (as showed by Gödel in his second incompleteness theorem). So the fact that your system is recursively enumerable implies a limit on what you can prove about Turing Machines: there is a particular explicit Turing Machine that runs forever but you cannot prove that fact.

Complexity: Finally, it is argued that the question of P=NP is linked with automated proving. Indeed, looking for a proof is a priori a lot harder than checking the validity of a proof. But if P=NP, verifying becomes "as hard" as finding, and so it would become "easy" to find proofs automatically, when they exist and are not too long. However, even if P=NP, the algorithm could still be impractical because of huge constant or exponent, but in spirit mathematicians could be replaced by algorithms.


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