Forgot your password?
typodupeerror
Math

Software Is Starting To Aid Mathematical Proofs 90

Posted by kdawson
from the sequencing-the-mathematical-genome dept.
An anonymous reader writes "Mathematical proofs are supposed to establish absolute certainty, since each statement is a pure deduction from fundamental axioms. But the reality is that mathematicians make mistakes. Proof-validation software can do what mathematicians never do: spell out every last step, making sure everything is right. Such software has been around for 20 years, but mathematicians and computer scientists now say they are nearing the point where every mathematician will routinely use the software before submitting a new result to a journal, producing a fully correct, formal, axiomatized mathematics."
This discussion has been archived. No new comments can be posted.

Software Is Starting To Aid Mathematical Proofs

Comments Filter:
  • Starting? (Score:1, Redundant)

    by narcberry (1328009)

    Maybe we've not run proof validation extensively, but software has been "aiding mathematical proofs" for a long time.

    • Yep. I guess the AC who submitted the story didn't quite RTFA, since TFA mentions the 1976 proof of the four color theorem. TFA doesn't say that proof checking software is new, just that it is gaining in popularity.

      • Re: (Score:3, Informative)

        by Anonymous Coward

        No. The 1976 proof of the four-color theorem has nothing to do with "proof checking". This is the process of writing your paper as formal logic, not as prose (which nobody does becomes its absurdly impractical for hard results), then using a computer to test that your formal logic is error-free. The four-color theorem proof was completely different. That was using math to say the theorem is equivalent to some simple property being true on a large database of special cases, and this property was tested by co

        • Yes, because translating problems from English to Programming languages is a really small part of solving problems with computers. Lady Lovelace [wikipedia.org] wasted a good deal of time on something like that. Too bad she didn't realize what a waste of time it is.
    • Dear slashdot mod: How the heck could the first post be redundant?
  • Let's see it prove I am not a chair ;-)

    • Re: (Score:3, Insightful)

      by ceoyoyo (59147)

      Assume: A: Chairs do not post on Slashdot.
      B: Tablizer posted on Slashdot.

      Therefore, Tablizer is not a chair.

      • What if I write a comment posting program called SlashBot, then sit on the computer running it?
      • Re: (Score:3, Funny)

        by WK2 (1072560)

        Assume: A: Chairs do not post on Slashdot.

        Why would I assume that? In fact, chairs posting on Slashdot is my hypothesis to explain why the posts seem as intelligent as they are, and why so many Slashdotters are afraid of Steve Ballmer.

        • If a chair would post on slashdot, it wouldn't be a chair, but a computer in the shape of a chair, or a human disguised as a chair. Therefore, chairs can't post on slashdot.
          • If a chair would post on slashdot, it wouldn't be a chair, but a computer in the shape of a chair, or a human disguised as a chair.

            And what if the computer in the shape of a chair was for sitting on? That would make it a bona-fide chair, with an embedded CPU.

      • by Daimanta (1140543)

        Assume: A: Ballmer posts on Slashdhot
        Therefore, chairs do not post on Slashdot
        B: Tablizer posted on Slashdot
        Therefore, Tablizer is not a chair.

      • Assume: A: Chairs do not post on Slashdot.

        [checks for the existence of a user with username chairs, finds no such user] Your assumption A holds ... for right now.

    • by rtaylor (70602)

      First we would need to determine the kind of chairs.

      Many an emperor has used their slaves as a seat.

      You may be in charge of a meeting at some point or an organization.

      There is a chance you have musical talent and could be in an orchestra.

      I think you should prove you are not a chair first because I'm pretty damn certain is someone offered you a substantial amount of money to act as a seat for a day, you would.

      Proving you are not a 4 legged wooden bar chair is fairly straight forward.

  • if the proof-verifying-algorithm is polynomially verifiable.

  • one proof engine (Score:4, Informative)

    by emeraldemon (1167599) on Sunday November 16, 2008 @12:23AM (#25774643)
    For what it's worth, I've had good experiences with coq: http://coq.inria.fr/ [inria.fr] Although I've never used it for anything large, it has the nice ability to make proofs about code, and export the code to haskell, scheme, or ML. I had a fun time proving that the min function always returns the lesser of the two values.
    • by richkh (534205)
      So you've been spending a lot of time playing with co... nevermind.
      • by JamesP (688957)

        No, you see, coq is french for rooster

        So he actually spent lots of time playing with a rooster.

        Oh wait...

    • For what it's worth, I've had good experiences with coq

      Don't forget to pay your $699 licensing fee, you coq-smoking teabagger!

    • by jd (1658)
      HOL [sourceforge.net] is said to be usable, but doesn't have the same opportunities for name abuse, though 2001 fans could come up with a whole bunch of new ideas. Isabelle [in.tum.de], however, would provide such opportunities, if you were to combine it with the package that started this thread. ACL2 [utexas.edu] is the least abusable name of all, so is quite useless.
  • So now that we have software that can extensively check proofs, what's next? I don't think it's too far-fetched to someday expect programs that can construct a proof from a given statement. I imagine some sort of approach where axioms are manipulated to reach a desired conclusion either through blind or guided permutations, or even the beginnings of coded innovation. Considering how logical and orderly mathematics is, could discoveries be left to computers while humans are forced to specialize in adaptin
    • Right so eliptic curves being intimately related to modular forms, which in turn can be used to prove Fermat's last theorem would be easy to do with a computer. Plus any program for finding proofs would be so complicated that there would be bugs in the code, leading to problems with the proofs it generated. That and mathematicians would not generally accept the results until they have been checked by peer review.

      An awful lot of proofs actually go in non logical directions and incorporate very different a
  • by Secret Rabbit (914973) on Sunday November 16, 2008 @04:45AM (#25775901) Journal

    To address the title first:

    There is experimental Mathematics that uses programs to search problems for "interesting features." Then one can take pencil to paper to look into that specific area of the "problem." You know, to actually prove something. Software can also be used to search for counter-examples to conjectures or look for evidence that a conjecture is true or not. So, in that way, software does aid Maths. As in, software can be used to search for "things" or to be used as a "microscope." It's been like this for some time.

    But, most people don't actually understand what Mathematics actually is. Hell, even in Applied Mathematics, one must actually prove something. But, that proof, and here is where the misunderstanding comes in, is not an exhaustive search nor similar. That is a "show." Proving something is very different. Proving something not only gets you to a conclusion, but you learn something a long the way. The proof always points to "other things." A "show" doesn't provide this.

    Now to answer what was written in the post:

    These "proof checkers" are, to put it politely, a misnomer. I find it sad that people actually think that they will work as advertised. First off, if anyone would actually look at the "code" that is needed to be entered in (at least) many of these "proof checkers" they'd realise just how problematic data entry will be. Not to mention the... numerous bugs that WILL be in the compiler and checker itself. Not to mention the impossible requirement for a zero defect environment. I could go on.

    But, there are also many other concerns that make this a practical fools errand. Namely, how do you translate something like, "A sufficiently well behaved function" (no that's not ad hoc, it quite rigorous within context), or "We take (37) and proceed by parts which results in:", etc, etc, etc. To accommodate this, the proof checker will either need someone to manually code every last detail expanding details as needed, something that is intractable, or AI that is, more than likely, more than a century more advanced than what we have today.

    I'll also point out that we already have a formal, axiomatized, correct Mathematics. The only problems with correctness that come up are recent results and those are typically found quickly. It's called a retraction and it happens regularly. As in, the Mathematics community already has facilities to accommodate for incorrectness in published solutions. Lets not blow everything out of proportion because some clowns with nothing better to do with there time think otherwise.

    In all honesty, how many of these fallacious stories are going to be published here? Because, this has been a repeated topic over the past couple weeks. Or does /. have the same technique as FOX "News"; say it enough times and it /becomes/ true?

    • Re: (Score:1, Informative)

      by Anonymous Coward

      You raise some interesting points, but I gather from the tone of your post that you haven't actually used a production quality proof assistant before (e.g., coq, isabelle, etc.)

      You say that these proof assistants will not work as advertised. I'm curious about why you think this is the case. Many of these proof assistants are not ad hoc pieces of software that some average hacker wrote, expecting it to do their mathematics homework for them. Several of the more prominent proof assistants, such as Coq and

      • I only read the first couple paragraphs before I stopped reading as you clearly only skimmed mine. As in, the answers are already there.

    • by thecod (1162567)

      These "proof checkers" are, to put it politely, a misnomer. I find it sad that people actually think that they will work as advertised. First off, if anyone would actually look at the "code" that is needed to be entered in (at least) many of these "proof checkers" they'd realise just how problematic data entry will be.

      This is completely wrong, on several points:

      firstly a proof checker actually does check proofs in a very precise sense: a proof is a rigorously defined, implementable object and a proof checker verifies that this object does indeed consist of a proof of a given proposition. This is (non trivially) decidable; i.e. there exists an algorithm that carries out this task, it forms the basis of any given proof checking software called the kernel. The rest of the software is just an environment to help the user co

      • 1) You didn't read what I wrote in what you first quoted of mine. Please actually read before replying to someone.

        2) I'll paraphrase from the Tao: Though a program be but 3 lines long. Some day, someone will have to maintain it. Similarly, no matter how small a program is, it will contain bugs.

        3) Having to go in a check the checker defeats the purpose of the checker.

        4) It isn't my job to check the checker. Nor is it any Mathematicians job to check the checker.

        5) Re: well defined "A sufficiently well beh

        • by thecod (1162567)

          2) I'll paraphrase from the Tao: Though a program be but 3 lines long. Some day, someone will have to maintain it. Similarly, no matter how small a program is, it will contain bugs.

          In the world of software development that the Tao refers to I have no doubt that this is true. But I have a dream... that someday my programms will not be juged by the number of their bugs but by the usefulness of their content...that someday the sons of a former logician and the sons of a former software engineer will be able to sit down together at the shell prompts of brotherhood... Also, it seems that the software that controls, say, a driverless subway system can not really afford to wait around for u

    • by khallow (566160)

      These "proof checkers" are, to put it politely, a misnomer. I find it sad that people actually think that they will work as advertised. First off, if anyone would actually look at the "code" that is needed to be entered in (at least) many of these "proof checkers" they'd realise just how problematic data entry will be. Not to mention the... numerous bugs that WILL be in the compiler and checker itself. Not to mention the impossible requirement for a zero defect environment. I could go on.

      I believe you're wrong for a very simple reason. The error in a proof checker is strictly decreasing. One can construct increasingly elaborate test cases as the proof checker is developed and vet each change (including new platforms) against this growing body of test cases. In comparison, each new math paper as it stands has a similar chance of evading error. But once these papers are converted to the language of the proof checker, then they too are subject to the asymptotically improving reliability of the

      • You're assuming that bug fixes won't introduce new errors. Are you sure that's a good assumption? Because, I've used computers before, and I know that it isn't.

        • by khallow (566160)
          The new errors have to get past the tests. And if they can, then the errors might as well have been there in the first place.
          • The number of potential errors/bugs is infinite if you want to be able to check proofs of arbitrary length. Merely claiming a monotonically decreasing number of bugs does not imply you will ever get to zero.

            The other thing you ignore is the fact that there are external bugs in the operating system and hardware (eg the infamous intel division bug), which can falsify the conclusion that a particular tests was actually passed. Thus it is not actually true that, even with a monotonically increasing number of

  • When a computer can put together some reasonable proofs in algebraic topology or geometry then we might have something.

    Not everything is mathematics is a clean series of algebraic steps. Sure you might be able to get a computer to prove the Snake Lemma, but what about a real theorem?

  • Holy crap! COMPUTErs used to COMPUTE stuff?! Unbelievable! Who thought up this off the base out of the box idea?!

  • I work as an assistant professor in mathematics. This sort of program really won't address the needs of the vast majority of publications for any highly regarded professional math journals because math publications are typically very concise and rarely fill in very many of the details. It is not too uncommon for steps in proofs well beyond most talented undergraduates to be taken as "obvious". If they don't want to bother entering all the steps into a paper, you can be sure they don't want to be bothered to
    • A question is, is this a problem? Are those "obvious" steps in proofs ever wrong? Given that, as you say, they are "well beyond most talented undergraduates", aren't there lots of slip-ups?

  • "fully correct, formal, axiomatized mathematics" (facepalm)

We have a equal opportunity Calculus class -- it's fully integrated.

Working...