Computer proof?

[A_Seagull]

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?

[Dave_Oblad]

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

[mitchellmckain]

Yes and not only can this be demonstrated for trivial examples. But computers now play important roles in a lot of mathematical proofs.

[A_Seagull]

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?

[someguy1]

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?

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.

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 w³ + x³ = y³ + z³. The smallest integer solution (with distinct w, x, y, z) is 12³ + 1³ = 9³ + 10³. 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