Would it be possible to automate the job of a mathematician by

ya

>>8074921
Sure. Now do it.

Oh wait, what's that? You can't?

I guess mathematicians will be keeping their jobs, topkek.

File: compressed.jpg (7KB, 236x330px) Image search: [Google]

7KB, 236x330px

>>8074921
>Could we just hook this technique up to some super computers and map out all of mathematics in finite time?
No. It would take forever to do that.

File: nothing found.png (5KB, 244x74px) Image search: [Google]

5KB, 244x74px

>>8074921
It's called ATP.

https://en.wikipedia.org/wiki/Automated_theorem_proving

>Could we just hook this technique up to some super computers and map out all of mathematics in finite time?

lol no. It becomes intractable. The hard part is trying to figure out how to combine axioms intelligently.

>>8075005
I'm interested in human-directed ATP but I'm a shitty mathematician lolol.

>>8074921
No, you couldn't. That's kind of the beauty of real mathematics.

>>8075043
And part of the reason that you can't is that the number of objects and connections between objects defined by a finite number of axioms is infinite and there is no reasonable heuristic for sorting through it.

Someone hasn't read his Turing

>>8075047
How do you know it's unbounded, though? Have you considered that there might be topological loops in the space of possible mathematics, where where one field relates to and transitions into the other?

File: 1455319635551.png (287KB, 836x1065px) Image search: [Google]

287KB, 836x1065px

>>8075069
This has nothing to do with the halting problem.

>>8075085
I didn't say it was unbounded.
I said it was infinite. The space of real numbers between 0 and 1, for example, is bounded and infinite.

We know it is infinite because we can put it in 1-to-1 correspondence with the real numbers.

Short of designing a computer as complex as the human brain with the capacity to learn these things for itself, i.e. a thinking AI, there is no way to check every possibility of axiomatic implications as a means of solving theorems.

Brute forcing this with a computer is not only difficult, it is impossible.

For example, even something as simple as determining the next prime after 2^74207281 - 1 has never been done before.

>>8075102
>The space of real numbers between 0 and 1, for example, is bounded and infinite
But proofs are discrete. This is a combinatorics problem and hence finite.

>>8075095
It's related to the Entscheidungsproblem

>>8075107
Look. We know that 2^10000000000000000 or whatever, some really large number, plus 1, is 2^10000000000000000 + 1. But writing it out in that notation, we know that because we've defined "plus 1" as + 1. But if I wrote it out without the exponent, we would only know how to add the 1 by means of an algorithm we all know intuitively for adding 1 to a number, regardless of the size of the number.

What you're suggesting is that a computer should be able to prove theorems on its own. To do that, it must rely on such algorithms as this. However, that leaves us with 2 options. The first is that we program all the algorithms in ourselves, which themselves rely on loads of theorems and proofs and is the same as feeding the computer all the information already. We already have that. It's Wolfram, or even Proofwiki or any math encyclopedia. So disregarding that option, what you're asking for is a computer that knows how to add 1 to a number infinitely large without an algorithm for quickly adding numbers. This is impossible, since the computation size of adding 1 to an arbitrarily large number would make it more feasible for the computer to simply combine all letters in English in every possible order into sentences, determine which ones form reasonable mathematical definitions for things (2 and 3, for example, would be different definitions, so an infinite number of definitions to sort through is yet another problem), and then consider the body of knowledge of every other academic discipline ever created and actively determine which of these definitions are reasonably useful at all, then draw an inference between 2 definitions, creating a new object that has to be defined in conjunction with every other definition and repeat this process an infinite number of times to prove even the simplest theorem.

To learn algorithms as it goes is impossible because the distinction between what is useful, and significant in mathematics is artificial and arbitrary.

>>8075095
The halting problem is a weaken version of the incompleteness theorem.

CS majors are still tards tho