Will computers be able to do math proofs?

[andytoh]

I'm a math graduate student, but also have great interest in computer capabilities.

Chess players once thought that a machine cannot beat the world's best chess players because they cannot plan like humans despite their calculational power. Nowadays, computers are consistently beating the world's best human chess players with their developed strategic power.

So, will computers also one day possesses the ingenuity to do math proofs? Is that technology being worked on right now?

 

[-Job-]

This question is mostly concerned with the field of Logic, but i think it's possible. For example, we could use a brute force approach to iterate through all possible proofs until we find one that works, although that isn't really feasible for most problems.
I think i remember coming across something that related this question to the P vs NP problem. In fact it was in a letter by some famous Mathematician/Logician, something to the effect that a polynomial time solution to an NP-Complete problem would make this feasible. I think i saw it on Clay Institute's site.

 

[andytoh]

we could use a brute force approach to iterate through all possible proofs until we find one that works, although that isn't really feasible for most problems.

With sufficient computing speed, it could possibly work. After all, when we solve a math problem, we do precisely that: using our current knowledge of definitions and theorems and then applying them in a correct sequence that leads to the desired conclusion. All math proofs use a finite number of definitions and a finite number of theorems, and they are simply applied in a logical sequence, like a path from node to node. We humans simply obtain the correct sequence with fewer trials (perhaps just one trial) avoiding the sequences that make no sense.

Computers may not be able to find the correct sequence in as few trials as us, but with sufficient computing speed can go through all the many permutations and hit a correct one with little time, much like a computer finds winning combinations in chess with many trials along the tree of move sequences and then getting it right in a short time.

 

[D H]

Computers are not ingenious chess players. They appear to be ingenious because chess is amenable to brute force search techniques. Go is a much harder game in terms of combinatorics. Computer Go games remain horrendous amateurs.

You can see the state of the art in symbolic manipulation in programs like Mathematica and Maple. They do the brute force, plug-and-chug stuff quite nicely and without errors (usually). However, they do a lousy job of simplifying equations. I can usually tell when someone has implemented a Maple solution to a differential equation in some algorithm because a single equation can span an entire page. I remain duly unimpressed.

 

[andytoh]

Computers are not ingenious chess players.

That is probably correct a few years ago, but nowadays I'm quite impressed. For example, in the last game of the Man (World's #1 player) vs Machine match a few weeks ago (where the computer won overall), Fritz 10 found a plan consisting of a long sequence of moves that baffled all the commentators. Only much later did the GMs watching appreciate the ingenuity of the plan, which none of the humans could have thought of. It was a winning plan that defeated the world's number 1. The ingenuity of computers is getting there.

Going back to math proofs, I believe machines can provide proofs so long as they have the database of definitions and established theorems. Once that stage is reached, the next step will be for them to discover new theorems with the current knowledge. But let's take it one step at a time.

 

[-Job-]

If you think about it humans also use a brute force approach through learning.
In the brain the unsuccessful connections have their relevance minimized. So it's a brute force process in the sense that as many combinations as possible are attempted, the useful ones being prioritized.

 

[D H]

If you think about it humans also use a brute force approach through learning.
In the brain the unsuccessful connections have their relevance minimized. So it's a brute force process in the sense that as many combinations as possible are attempted, the useful ones being prioritized.

I disagree. Computers are much better at brute force than we can ever hope to accomplish. Where we excel is in pattern recognition. The ability to recognize patterns is partially built-in through evolution. Our imagination builds on top of those built-in capabilties.

We learn by extending existing patterns. We start life with a small set of built-in patterns. For us, extending patterns is a much more fruitful approach than is blind brute force. The number of combinations of the kinds of things we deal on a day-to-day basis vastly overwhelm the number of neural connections in a human brain.

Go is a good example. There is no way to apply brute force to Go. With captures, the http://senseis.xmp.net/?ComplexityOfGo" makes the number of protons in the universe a very tiny number: [tex]10^{(7.49\cdot 10^{48})}\text{\ versus\ } 10^{90}[/itex], a tiny number.[/tex]

 

[waht]

There is a computer program capable of checking advaced proofs from topology and higher.

The mizar project

http://en.wikipedia.org/wiki/Mizar_system


However, proving a new proof usually requires inventing new notations, new math, new spaces, new rules and etc.

I don't think computers can do that, because our pattern recognition algorithms are very primitive, basically.