Slashdot Mirror

← Back to Stories (view on slashdot.org)

The End of Mathematical Proofs by Humans?

Posted by timothy on from the somehow-I-doubt-it dept.

vivin writes "I recall how I did a bunch of Mathematical Proofs when I was in high school. In fact, proofs were an important part of Math according to the CBSE curriculum in Indian Schools. We were taught how to analyze complex problems and then break them down into simple (atomic) steps. It is similar to the derivation of a Physics formula. Proofs form a significant part of what Mathematicians do. However, according to this article from the Economist, it seems that the use of computers to generate proofs is causing mathematicians to 're-examine the foundations of their discipline.' However, critics of computer-aided proofs say that the proofs are hard to verify due to the large number of steps and hence, may be inherently flawed. Defenders of the same point out that there are non computer-aided proofs that are also rather large and unverifiable, like the Classification of Simple Finite Groups. Computer-aided proofs have been instrumental in solving some vexing problems like the Four Color Theorem."

4 of 549 comments (clear)

  1. Re:Godel/Turing/Cohen... by ivano · · Score: 0, Troll
    >> There's absolutely no evidence that human minds have magical access to truths which formal systems don't

    What has Penrose have to do with it? His little "quantum computers in our brain" has nothing to do with what I said. I gave you my sources: Cohen, Turning and Godel. That's it. Ask a logician if you don't believe me. All of these guys showed the limitations of formal systems (my bit about humans is irrelevant - and not very funny to begin with).

    Ciao

  2. Yesterday's news? by nextdoornerd · · Score: 0, Troll
    Ahemm.

    First, the story has been already discussed on technocrat.net day's ago (well, with 5 comments or so not really "discussed" as such :))

    Second, I have to run to have lunch now and then boys... I'm eager to wrestle over my master's subject with the whole /. crowde... Oh, the sanity :)

    Anyway, more to the point: it's not really AI, man. (At least nowadays.) Just some wonderfully pure math represented in (the most cases) painfully obfuscated, say, ML code >:\ (oh functionals, how I love thee... let me count the ways... uhm... zero? Ahemm.)

  3. Re:unverifiable by roju · · Score: 0, Troll

    Good idea. You write us a verifying program that can tell us if any given program will halt, and then we'll use it to test our theorem generator.

  4. Re:Critics Reaction... by nine-times · · Score: 0, Troll

    If it's so simple, go ahead and come up with a proof now. Or has your understanding diminished since the 1st grade?