Computer proof?

Discussions concerned with knowledge of measurement, properties, and relations quantities, theoretical or applied.

Computer proof?

Postby A_Seagull on June 5th, 2018, 1:29 am 

I am interested to know whether a computer is capable of producing a mathematical proof.

Has a computer ever provided a proof? And by 'proof' I don't just mean a demonstration of the exhaustion of possibilities as was done with the 4 colour problem. I mean something like proving that the square root of 2 is irrational or that the set of primes is infinite.

I suspect that a computer would be theoretically capable of doing so, but it would require some additional concepts such as a a logical interpretation of 'infinite' and 'irrational'.

As a corollary to this question: Is there any mathematical procedure or operation which a computer is incapable of carrying out?
User avatar
A_Seagull
Forum Neophyte
 
Posts: 31
Joined: 29 Apr 2017


Re: Computer proof?

Postby Dave_Oblad on June 6th, 2018, 6:13 pm 

Hi A_Seagull,

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

Yes. A computer cannot generate/create a true random number nor anything actually random. It can do pseudo-random functions via op-code or.. obtain a signal from a random noise generator. See.. Math cannot be used to generate true randomness.

Regards,
Dave :^)
User avatar
Dave_Oblad
Resident Member
 
Posts: 3229
Joined: 08 Sep 2010
Location: Tucson, Arizona
Blog: View Blog (2)


Re: Computer proof?

Postby mitchellmckain on June 6th, 2018, 6:27 pm 

Yes and not only can this be demonstrated for trivial examples. But computers now play important roles in a lot of mathematical proofs.
User avatar
mitchellmckain
Active Member
 
Posts: 1326
Joined: 27 Oct 2016


Re: Computer proof?

Postby A_Seagull on June 6th, 2018, 6:35 pm 

Dave_Oblad » June 7th, 2018, 10:13 am wrote:Hi A_Seagull,

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

Yes. A computer cannot generate/create a true random number nor anything actually random. It can do pseudo-random functions via op-code or.. obtain a signal from a random noise generator. See.. Math cannot be used to generate true randomness.

Regards,
Dave :^)


What does the generation of random numbers have to do with a proof?
User avatar
A_Seagull
Forum Neophyte
 
Posts: 31
Joined: 29 Apr 2017


Re: Computer proof?

Postby someguy1 on June 8th, 2018, 1:24 am 

A_Seagull » June 4th, 2018, 11:29 pm wrote:I am interested to know whether a computer is capable of producing a mathematical proof.

Has a computer ever provided a proof? And by 'proof' I don't just mean a demonstration of the exhaustion of possibilities as was done with the 4 colour problem. I mean something like proving that the square root of 2 is irrational or that the set of primes is infinite.



Automated proof systems of various types are making great strides these days as others have noted. One interesting one is Coq, which as Wiki says is not an automated theorem prover, but rather a proof assistant. It's designed to let the working mathematician formalize his or her proofs and then have them checked to make sure they are correct.

Coq came out of the observation that many published math proofs contain errors; and that these errors can go undiscovered in some cases for decades. So computer-assisted math, if you want to call it that, is addressing a genuine practical problem. It's not just an attempt to mechanize human creativity by AI-hypemeisters in other words. (Count me among the AI skeptics).

Now perhaps you are thinking or wondering about whether computers can emulate or even surpass human creativity. A proof checker doesn't "want" to find a proof, it's just flipping bits like the Chinese room. But you know how endless that discussion gets, I'm only pointing out that it's the same question. Does the Chinese room understand Chinese? Does an automated proof checker understand math? I say no and no, but plenty of people are ready to argue the opposite. I'm mentioning all this because I'm reading between the lines of your question. Do computers formulate great research programs and then carry them out, as a professional mathematician does? No, not yet. Will they ever? I don't think so, but I could be wrong.

The tl;dr on all that is to ask, what do you mean by "producing?" On its own initiative? No of course not. But the field's making great strides. Chess and Go computers make moves that baffle experts. How long will it be before the math computers start doing the same?





A_Seagull » June 4th, 2018, 11:29 pm wrote:I suspect that a computer would be theoretically capable of doing so, but it would require some additional concepts such as a a logical interpretation of 'infinite' and 'irrational'.


Just a technical point. Those logical definitions aren't difficult. A set is "infinite" just in case it fails to have a bijection with any of the natural numbers 0, 1, 2, 3, ... That's not hard to put into logical notation and feed to a program that can manipulate logical expressions in predicate calculus. That's all the automated theorem provers are doing. So we can tell a computer what an infinite set it. Likewise a real number is irrational if it's not the case that it's the quotient of two integers. We can code that up as a predicate expression. Those things are technical exercises, they're not conceptual challenges to computers doing math.


A_Seagull » June 4th, 2018, 11:29 pm wrote:As a corollary to this question: Is there any mathematical procedure or operation which a computer is incapable of carrying out?


Dave gave the example of generating a random number. You asked what that has to do with proofs, but I thought he was answering the question you asked.

There's another very interesting example of something a computer can't do, solving Diophantine equations. A Diophantine equation (after Diophantus of Alexandria, the father of algebra -- it was Diophantus's book whose margin Fermat found too small) is a polynomial equation in two or more variables whose coeeficients are integers. We may then ask, are there any integer solutions to the equation?

For example consider w3 + x3 = y3 + z3. The smallest integer solution (with distinct w, x, y, z) is 123 + 13 = 93 + 103. This is Ramanujan's famous taxicab number.

In 1900, the great German mathematician David Hilbert asked whether there might be an automatic procedure for determining whether an arbitary Diophantine equation has a solution. In 1970 it was proven that the answer is no. There is no automated procedure for determining if an arbitrary Diophantine equation has an integer solution.

This is a classic example of an easily stated mathematical problem that can not possibly be solved by a computer.

https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem
someguy1
Member
 
Posts: 733
Joined: 08 Nov 2013
Dave_ObladBraininvatmitchellmckain liked this post



Return to Mathematics

Who is online

Users browsing this forum: No registered users and 3 guests