Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Will computers be able to do math proofs?

  1. Dec 27, 2006 #1
    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 possess the ingenuity to do math proofs? Is that technology being worked on right now?
     
    Last edited: Dec 27, 2006
  2. jcsd
  3. Dec 27, 2006 #2

    -Job-

    User Avatar
    Science Advisor

    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.
     
  4. Dec 27, 2006 #3
    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.
     
    Last edited: Dec 27, 2006
  5. Dec 27, 2006 #4

    D H

    User Avatar
    Staff Emeritus
    Science Advisor

    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.
     
  6. Dec 27, 2006 #5
    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.
     
    Last edited: Dec 27, 2006
  7. Dec 27, 2006 #6

    -Job-

    User Avatar
    Science Advisor

    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.
     
  8. Dec 27, 2006 #7

    D H

    User Avatar
    Staff Emeritus
    Science Advisor

    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 number of combinations in Go 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.
     
  9. Dec 28, 2006 #8
    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.
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?



Similar Discussions: Will computers be able to do math proofs?
Loading...